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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos3.opb
MD5SUM640a68756f6bc046860dd4d0fa3890ca
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 105
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 10485755
Number of bits of the sum of numbers in the objective function 24
Biggest number in a constraint 2396687647113216000
Number of bits of the biggest number in a constraint 62
Biggest sum of numbers in a constraint 282492798299765243904
Number of bits of the biggest sum of numbers68
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables28623
Total number of constraints2841
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)1377
Number of constraints which are nor clauses,nor cardinality constraints1464
Minimum length of a constraint1
Maximum length of a constraint3188

Trace number 6299

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        878016 kB
Buffers:         25432 kB
Cached:         102424 kB
SwapCached:        868 kB
Active:          44980 kB
Inactive:        85500 kB
HighTotal:      131008 kB
HighFree:        26264 kB
LowTotal:       903652 kB
LowFree:        851752 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5712 kB
Slab:            20408 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:39:36 (client local time) WITH STATUS 0 IN 1206.87 SECONDS
stats: 3458 7 1206.87 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 4155] 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/17669/stat): 17669 (minisat+_script) R 17668 17669 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855974989 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/17669/statm): 174 3 169 147 0 27 0
[pid=17669] 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=17670
New process pid=17671
New process pid=17672
execve syscall for /bin/sed executable
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
One traced child (pid=17671) exited with status: 0
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=17672) exited with status: 0
One traced child (pid=17670) exited with status: 0
New process pid=17673
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-neos3.opb
One traced child (pid=17673) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=17674
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-neos3.opb

[startup+10.0036 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 3396 0 0 0 948 21 0 0 25 0 1 0 1855974999 13291520 3084 4294967295 134512640 135167914 3221224448 3221223264 134522195 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17674/statm): 3245 3084 162 162 0 3083 0
[pid=17674] vsize: 12980
Current children cumulated CPU time (s) 9.75
Current children cumulated vsize (Kb) 15108

[startup+20.0053 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 3396 0 0 0 1948 22 0 0 25 0 1 0 1855974999 13291520 3084 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17674/statm): 3245 3084 162 162 0 3083 0
[pid=17674] vsize: 12980
Current children cumulated CPU time (s) 19.76
Current children cumulated vsize (Kb) 15108

[startup+30.006 s]
Raw data (loadavg): 1.00 0.97 0.96 1/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) T 17669 17669 16528 0 -1 0 8530 0 0 0 2902 45 0 0 25 0 1 0 1855974999 31170560 7430 4294967295 134512640 135167914 3221224448 3221091292 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/17674/statm): 7610 7430 162 162 0 7448 0
[pid=17674] vsize: 30440
Current children cumulated CPU time (s) 29.53
Current children cumulated vsize (Kb) 32568

[startup+40.0056 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 17076 0 0 0 3840 76 0 0 25 0 1 0 1855974999 58003456 13999 4294967295 134512640 135167914 3221224448 3221093024 134845890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 14161 13999 162 162 0 13999 0
[pid=17674] vsize: 56644
Current children cumulated CPU time (s) 39.22
Current children cumulated vsize (Kb) 58772

[startup+50.0063 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 22565 0 0 0 4776 104 0 0 25 0 1 0 1855974999 80637952 19488 4294967295 134512640 135167914 3221224448 3221091632 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17674/statm): 19687 19488 162 162 0 19525 0
[pid=17674] vsize: 78748
Current children cumulated CPU time (s) 48.86
Current children cumulated vsize (Kb) 80876

[startup+60.007 s]
Raw data (loadavg): 1.00 0.97 0.96 1/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) T 17669 17669 16528 0 -1 0 32113 0 0 0 5716 137 0 0 25 0 1 0 1855974999 108748800 26357 4294967295 134512640 135167914 3221224448 3221091132 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17674/statm): 26550 26357 162 162 0 26388 0
[pid=17674] vsize: 106200
Current children cumulated CPU time (s) 58.59
Current children cumulated vsize (Kb) 108328

[startup+70.0077 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 37628 0 0 0 6653 163 0 0 25 0 1 0 1855974999 131305472 31872 4294967295 134512640 135167914 3221224448 3221093984 134694419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17674/statm): 32057 31872 162 162 0 31895 0
[pid=17674] vsize: 128228
Current children cumulated CPU time (s) 68.22
Current children cumulated vsize (Kb) 130356

[startup+80.0084 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 43081 0 0 0 7591 188 0 0 25 0 1 0 1855974999 153616384 37325 4294967295 134512640 135167914 3221224448 3221091776 134620666 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17674/statm): 37504 37325 162 162 0 37342 0
[pid=17674] vsize: 150016
Current children cumulated CPU time (s) 77.85
Current children cumulated vsize (Kb) 152144

[startup+90.0081 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 56413 0 0 0 8539 223 0 0 25 0 1 0 1855974999 208211968 50657 4294967295 134512640 135167914 3221224448 3221091776 134625512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 50833 50657 162 162 0 50671 0
[pid=17674] vsize: 203332
Current children cumulated CPU time (s) 87.68
Current children cumulated vsize (Kb) 205460

[startup+100.009 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 61955 0 0 0 9477 250 0 0 25 0 1 0 1855974999 209293312 50926 4294967295 134512640 135167914 3221224448 3221091888 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17674/statm): 51097 50926 162 162 0 50935 0
[pid=17674] vsize: 204388
Current children cumulated CPU time (s) 97.33
Current children cumulated vsize (Kb) 206516

[startup+110.009 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 67484 0 0 0 10417 276 0 0 25 0 1 0 1855974999 231919616 56455 4294967295 134512640 135167914 3221224448 3221091684 134624225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17674/statm): 56621 56455 162 162 0 56459 0
[pid=17674] vsize: 226484
Current children cumulated CPU time (s) 106.99
Current children cumulated vsize (Kb) 228612

[startup+120.011 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) T 17669 17669 16528 0 -1 0 72962 0 0 0 11355 300 0 0 25 0 1 0 1855974999 254337024 61933 4294967295 134512640 135167914 3221224448 3221091196 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/17674/statm): 62094 61933 162 162 0 61932 0
[pid=17674] vsize: 248376
Current children cumulated CPU time (s) 116.61
Current children cumulated vsize (Kb) 250504

[startup+130.012 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 12346 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216272 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 126.57
Current children cumulated vsize (Kb) 210852

[startup+140.012 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 13346 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216864 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 136.57
Current children cumulated vsize (Kb) 210852

[startup+150.014 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 14346 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216976 134844668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 146.57
Current children cumulated vsize (Kb) 210852

[startup+160.014 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 15346 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216528 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 156.57
Current children cumulated vsize (Kb) 210852

[startup+170.015 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 16347 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216976 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 166.58
Current children cumulated vsize (Kb) 210852

[startup+180.015 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 17347 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216800 134696738 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 176.58
Current children cumulated vsize (Kb) 210852

[startup+190.016 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 18347 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216432 134845890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 186.58
Current children cumulated vsize (Kb) 210852

[startup+200.017 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 19347 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216852 134849147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 196.58
Current children cumulated vsize (Kb) 210852

[startup+210.016 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 20347 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216624 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 206.58
Current children cumulated vsize (Kb) 210852

[startup+220.018 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 21348 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217328 134844653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 216.59
Current children cumulated vsize (Kb) 210852

[startup+230.019 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 22348 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217044 134849147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 226.59
Current children cumulated vsize (Kb) 210852

[startup+240.018 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 23348 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217024 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 236.59
Current children cumulated vsize (Kb) 210852

[startup+250.019 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 24348 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216656 134718203 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 246.59
Current children cumulated vsize (Kb) 210852

[startup+260.02 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 25348 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216496 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 256.59
Current children cumulated vsize (Kb) 210852

[startup+270.02 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 26349 305 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216652 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 266.6
Current children cumulated vsize (Kb) 210852

[startup+280.021 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 27349 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216652 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 276.61
Current children cumulated vsize (Kb) 210852

[startup+290.022 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 28349 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216560 134844736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 286.61
Current children cumulated vsize (Kb) 210852

[startup+300.022 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 29349 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217216 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 296.61
Current children cumulated vsize (Kb) 210852

[startup+310.023 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 30349 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216800 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 306.61
Current children cumulated vsize (Kb) 210852

[startup+320.024 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 31350 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216480 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 316.62
Current children cumulated vsize (Kb) 210852

[startup+330.024 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 32350 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216688 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 326.62
Current children cumulated vsize (Kb) 210852

[startup+340.025 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 33350 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216800 134696726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 336.62
Current children cumulated vsize (Kb) 210852

[startup+350.026 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 34350 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216820 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 346.62
Current children cumulated vsize (Kb) 210852

[startup+360.027 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 35350 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217232 134694329 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 356.62
Current children cumulated vsize (Kb) 210852

[startup+370.028 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 36350 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217216 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 366.62
Current children cumulated vsize (Kb) 210852

[startup+380.029 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 37351 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216688 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 376.63
Current children cumulated vsize (Kb) 210852

[startup+390.029 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 38351 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216880 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 386.63
Current children cumulated vsize (Kb) 210852

[startup+400.03 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 39351 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217024 134522816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 396.63
Current children cumulated vsize (Kb) 210852

[startup+410.031 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 40351 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216844 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 406.63
Current children cumulated vsize (Kb) 210852

[startup+420.032 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 41352 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217248 134629069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 416.64
Current children cumulated vsize (Kb) 210852

[startup+430.033 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 42352 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217088 134844647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 426.64
Current children cumulated vsize (Kb) 210852

[startup+440.033 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 43352 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216836 134844636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 436.64
Current children cumulated vsize (Kb) 210852

[startup+450.034 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 44352 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216336 134843015 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 446.64
Current children cumulated vsize (Kb) 210852

[startup+460.034 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 45352 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217152 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 456.64
Current children cumulated vsize (Kb) 210852

[startup+470.035 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 46353 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216496 134845937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 466.65
Current children cumulated vsize (Kb) 210852

[startup+480.036 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 47353 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216792 134718177 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 476.65
Current children cumulated vsize (Kb) 210852

[startup+490.036 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 48353 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216508 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 486.65
Current children cumulated vsize (Kb) 210852

[startup+500.037 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 49353 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216640 134696653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 496.65
Current children cumulated vsize (Kb) 210852

[startup+510.038 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 50354 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216464 134843426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 506.66
Current children cumulated vsize (Kb) 210852

[startup+520.039 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 51354 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216816 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 516.66
Current children cumulated vsize (Kb) 210852

[startup+530.039 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 52354 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216484 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 526.66
Current children cumulated vsize (Kb) 210852

[startup+540.039 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 53354 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216864 134694524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 536.66
Current children cumulated vsize (Kb) 210852

[startup+550.041 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 54355 306 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217072 134629143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 546.67
Current children cumulated vsize (Kb) 210852

[startup+560.041 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 55355 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216688 134694517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 556.68
Current children cumulated vsize (Kb) 210852

[startup+570.042 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 56355 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217064 134693734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 566.68
Current children cumulated vsize (Kb) 210852

[startup+580.043 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 57355 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216812 134723236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 576.68
Current children cumulated vsize (Kb) 210852

[startup+590.042 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 58355 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217440 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 586.68
Current children cumulated vsize (Kb) 210852

[startup+600.043 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 59356 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217056 134694345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 596.69
Current children cumulated vsize (Kb) 210852

[startup+610.044 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 60356 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216884 134696786 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 606.69
Current children cumulated vsize (Kb) 210852

[startup+620.044 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 61356 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217392 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 616.69
Current children cumulated vsize (Kb) 210852

[startup+630.045 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 62356 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217328 134843402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 626.69
Current children cumulated vsize (Kb) 210852

[startup+640.046 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 63356 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217248 134630795 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 636.69
Current children cumulated vsize (Kb) 210852

[startup+650.046 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 64357 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216540 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 646.7
Current children cumulated vsize (Kb) 210852

[startup+660.047 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 65357 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216528 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 656.7
Current children cumulated vsize (Kb) 210852

[startup+670.049 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 66357 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216032 134844647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 666.7
Current children cumulated vsize (Kb) 210852

[startup+680.049 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 67357 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216472 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 676.7
Current children cumulated vsize (Kb) 210852

[startup+690.049 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 68357 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216688 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 686.7
Current children cumulated vsize (Kb) 210852

[startup+700.051 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 69358 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217004 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 696.71
Current children cumulated vsize (Kb) 210852

[startup+710.052 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 70358 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216624 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 706.71
Current children cumulated vsize (Kb) 210852

[startup+720.052 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 71358 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216736 134844715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 716.71
Current children cumulated vsize (Kb) 210852

[startup+730.054 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 72358 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216692 134849147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 726.71
Current children cumulated vsize (Kb) 210852

[startup+740.054 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 73358 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216988 134723267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 736.71
Current children cumulated vsize (Kb) 210852

[startup+750.054 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 74359 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216892 134522235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 746.72
Current children cumulated vsize (Kb) 210852

[startup+760.055 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 75359 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216624 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 756.72
Current children cumulated vsize (Kb) 210852

[startup+770.057 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 76359 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217152 134845194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 766.72
Current children cumulated vsize (Kb) 210852

[startup+780.057 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 77360 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217040 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 776.73
Current children cumulated vsize (Kb) 210852

[startup+790.058 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 78360 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216448 134844715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 786.73
Current children cumulated vsize (Kb) 210852

[startup+800.059 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 79360 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216208 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 796.73
Current children cumulated vsize (Kb) 210852

[startup+810.059 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 80360 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217408 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 806.73
Current children cumulated vsize (Kb) 210852

[startup+820.06 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 81360 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216672 134522839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 816.73
Current children cumulated vsize (Kb) 210852

[startup+830.061 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 82361 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217016 134844674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 826.74
Current children cumulated vsize (Kb) 210852

[startup+840.061 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 83361 307 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216528 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 836.74
Current children cumulated vsize (Kb) 210852

[startup+850.062 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 84361 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217392 134843402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 846.75
Current children cumulated vsize (Kb) 210852

[startup+860.063 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 85361 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217200 134522492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 856.75
Current children cumulated vsize (Kb) 210852

[startup+870.064 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 86361 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216864 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 866.75
Current children cumulated vsize (Kb) 210852

[startup+880.065 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 87362 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217064 134694366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 876.76
Current children cumulated vsize (Kb) 210852

[startup+890.065 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 88362 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217596 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 886.76
Current children cumulated vsize (Kb) 210852

[startup+900.066 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 89362 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216992 134843074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 896.76
Current children cumulated vsize (Kb) 210852

[startup+910.066 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 90362 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216888 134693744 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 906.76
Current children cumulated vsize (Kb) 210852

[startup+920.067 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 91362 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217056 134849102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 916.76
Current children cumulated vsize (Kb) 210852

[startup+930.068 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 92363 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217200 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 926.77
Current children cumulated vsize (Kb) 210852

[startup+940.068 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 93363 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217264 134630786 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 936.77
Current children cumulated vsize (Kb) 210852

[startup+950.069 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 94363 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217232 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 946.77
Current children cumulated vsize (Kb) 210852

[startup+960.07 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 95363 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216800 134843404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 956.77
Current children cumulated vsize (Kb) 210852

[startup+970.07 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 96363 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217200 134845937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 966.77
Current children cumulated vsize (Kb) 210852

[startup+980.071 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 97363 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216752 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 976.77
Current children cumulated vsize (Kb) 210852

[startup+990.071 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 98364 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216736 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 986.78
Current children cumulated vsize (Kb) 210852

[startup+1000.07 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 99364 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217532 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 996.78
Current children cumulated vsize (Kb) 210852

[startup+1010.07 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 100364 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216640 134696248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1006.78
Current children cumulated vsize (Kb) 210852

[startup+1020.07 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 101364 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217072 134630795 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1016.78
Current children cumulated vsize (Kb) 210852

[startup+1030.07 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 102364 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217200 134722539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1026.78
Current children cumulated vsize (Kb) 210852

[startup+1040.07 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 103365 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217312 134845913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1036.79
Current children cumulated vsize (Kb) 210852

[startup+1050.07 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 104365 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216400 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1046.79
Current children cumulated vsize (Kb) 210852

[startup+1060.07 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 105365 308 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216976 134844718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1056.79
Current children cumulated vsize (Kb) 210852

[startup+1070.07 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 106365 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216532 134696786 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1066.8
Current children cumulated vsize (Kb) 210852

[startup+1080.07 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 107365 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217056 134694364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1076.8
Current children cumulated vsize (Kb) 210852

[startup+1090.07 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 108365 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217256 134628675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1086.8
Current children cumulated vsize (Kb) 210852

[startup+1100.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 109366 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216512 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1096.81
Current children cumulated vsize (Kb) 210852

[startup+1110.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 110366 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216784 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1106.81
Current children cumulated vsize (Kb) 210852

[startup+1120.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 111366 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217056 134849122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1116.81
Current children cumulated vsize (Kb) 210852

[startup+1130.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 112366 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217344 134843404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1126.81
Current children cumulated vsize (Kb) 210852

[startup+1140.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 113366 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216864 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1136.81
Current children cumulated vsize (Kb) 210852

[startup+1150.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 114367 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216712 134849087 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1146.82
Current children cumulated vsize (Kb) 210852

[startup+1160.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 115367 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217088 134629451 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1156.82
Current children cumulated vsize (Kb) 210852

[startup+1170.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 116367 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217248 134630940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1166.82
Current children cumulated vsize (Kb) 210852

[startup+1180.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 117367 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216844 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1176.82
Current children cumulated vsize (Kb) 210852

[startup+1190.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 118367 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216836 134844636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1186.82
Current children cumulated vsize (Kb) 210852

[startup+1200.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 119368 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221217088 134629454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1196.83
Current children cumulated vsize (Kb) 210852

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 120368 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216800 134845921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1206.83
Current children cumulated vsize (Kb) 210852



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 17674
Raw data (/proc/17669/stat): 17669 (minisat+_script) S 17668 17669 16528 0 -1 0 314 392 0 0 0 1 3 2 20 0 1 0 1855974989 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17669/statm): 532 234 485 147 0 385 0
[pid=17669] vsize: 2128
Raw data (/proc/17674/stat): 17674 (minisat+_bignum) R 17669 17669 16528 0 -1 0 73596 0 0 0 120368 309 0 0 25 0 1 0 1855974999 213733376 52021 4294967295 134512640 135167914 3221224448 3221216812 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17674/statm): 52181 52021 162 162 0 52019 0
[pid=17674] vsize: 208724
Current children cumulated CPU time (s) 1206.83
Current children cumulated vsize (Kb) 210852

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

Child status: 0
Real time (s): 1210.18
CPU time (s): 1206.87
CPU user time (s): 1203.69
CPU system time (s): 3.18851
CPU usage (%): 99.7268
Max. virtual memory (cumulated for all children) (Kb): 250504

Verifier Data

ERROR: no interpretation found !