Some explanations

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

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos3.opb
MD5SUMaa121475b5e53120a1d24de3f0361b26
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 155
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 10737418235
Number of bits of the sum of numbers in the objective function 34
Biggest number in a constraint 2454208150643933184000
Number of bits of the biggest number in a constraint 72
Biggest sum of numbers in a constraint 289272765430218954375168
Number of bits of the biggest sum of numbers78
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables42220
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 constraint4780

Trace number 5900

Launcher Data

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        878800 kB
Buffers:         33948 kB
Cached:          90224 kB
SwapCached:        676 kB
Active:          27752 kB
Inactive:        98872 kB
HighTotal:      131008 kB
HighFree:        41524 kB
LowTotal:       903652 kB
LowFree:        837276 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5664 kB
Slab:            23560 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:05:33 (client local time) WITH STATUS 0 IN 1204.51 SECONDS
stats: 3073 7 1204.51 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/4023/stat): 4023 (minisat+_script) R 4022 4023 19818 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854669029 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/4023/statm): 174 3 169 147 0 27 0
[pid=4023] 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=4024
New process pid=4025
New process pid=4026
execve syscall for /bin/sed executable
One traced child (pid=4025) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=4026) exited with status: 0
One traced child (pid=4024) exited with status: 0
New process pid=4027
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-neos3.opb
One traced child (pid=4027) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=4028
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-neos3.opb

[startup+10.004 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 4414 0 0 0 947 21 0 0 25 0 1 0 1854669040 14471168 3088 4294967295 134512640 135167914 3221224448 3221222784 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 3533 3088 162 162 0 3371 0
[pid=4028] vsize: 14132
Current children cumulated CPU time (s) 9.74
Current children cumulated vsize (Kb) 16260

[startup+20.0058 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 6978 0 0 0 1919 34 0 0 25 0 1 0 1854669040 20332544 4524 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 4964 4524 162 162 0 4802 0
[pid=4028] vsize: 19856
Current children cumulated CPU time (s) 19.59
Current children cumulated vsize (Kb) 21984

[startup+30.0066 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 6978 0 0 0 2918 35 0 0 25 0 1 0 1854669040 20332544 4524 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 4964 4524 162 162 0 4802 0
[pid=4028] vsize: 19856
Current children cumulated CPU time (s) 29.59
Current children cumulated vsize (Kb) 21984

[startup+40.0074 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 6978 0 0 0 3919 35 0 0 25 0 1 0 1854669040 20332544 4524 4294967295 134512640 135167914 3221224448 3221223296 134594248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 4964 4524 162 162 0 4802 0
[pid=4028] vsize: 19856
Current children cumulated CPU time (s) 39.6
Current children cumulated vsize (Kb) 21984

[startup+50.0081 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) T 4023 4023 19818 0 -1 0 11834 0 0 0 4876 58 0 0 25 0 1 0 1854669040 36900864 8554 4294967295 134512640 135167914 3221224448 3221036924 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/4028/statm): 9009 8554 162 162 0 8847 0
[pid=4028] vsize: 36036
Current children cumulated CPU time (s) 49.4
Current children cumulated vsize (Kb) 38164

[startup+60.0089 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 20307 0 0 0 5814 90 0 0 25 0 1 0 1854669040 63455232 15050 4294967295 134512640 135167914 3221224448 3221038852 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 15492 15050 162 162 0 15330 0
[pid=4028] vsize: 61968
Current children cumulated CPU time (s) 59.1
Current children cumulated vsize (Kb) 64096

[startup+70.0097 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) T 4023 4023 19818 0 -1 0 25811 0 0 0 6755 114 0 0 25 0 1 0 1854669040 86155264 20554 4294967295 134512640 135167914 3221224448 3221038492 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/4028/statm): 21034 20554 162 162 0 20872 0
[pid=4028] vsize: 84136
Current children cumulated CPU time (s) 68.75
Current children cumulated vsize (Kb) 86264

[startup+80.0115 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 35341 0 0 0 7698 144 0 0 25 0 1 0 1854669040 114184192 27405 4294967295 134512640 135167914 3221224448 3221036892 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 27877 27405 162 162 0 27715 0
[pid=4028] vsize: 111508
Current children cumulated CPU time (s) 78.48
Current children cumulated vsize (Kb) 113636

[startup+90.0123 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 40909 0 0 0 8637 171 0 0 25 0 1 0 1854669040 136953856 32973 4294967295 134512640 135167914 3221224448 3221037084 134722542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 33436 32973 162 162 0 33274 0
[pid=4028] vsize: 133744
Current children cumulated CPU time (s) 88.14
Current children cumulated vsize (Kb) 135872

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 46382 0 0 0 9578 195 0 0 25 0 1 0 1854669040 159350784 38446 4294967295 134512640 135167914 3221224448 3221037456 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 38904 38446 162 162 0 38742 0
[pid=4028] vsize: 155616
Current children cumulated CPU time (s) 97.79
Current children cumulated vsize (Kb) 157744

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 59876 0 0 0 10523 232 0 0 25 0 1 0 1854669040 214597632 51940 4294967295 134512640 135167914 3221224448 3221038192 134516662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 52392 51940 162 162 0 52230 0
[pid=4028] vsize: 209568
Current children cumulated CPU time (s) 107.61
Current children cumulated vsize (Kb) 211696

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) T 4023 4023 19818 0 -1 0 65326 0 0 0 11463 258 0 0 25 0 1 0 1854669040 215302144 52117 4294967295 134512640 135167914 3221224448 3221036924 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/4028/statm): 52564 52117 162 162 0 52402 0
[pid=4028] vsize: 210256
Current children cumulated CPU time (s) 117.27
Current children cumulated vsize (Kb) 212384

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 70902 0 0 0 12404 284 0 0 25 0 1 0 1854669040 238120960 57693 4294967295 134512640 135167914 3221224448 3221038188 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 58135 57693 162 162 0 57973 0
[pid=4028] vsize: 232540
Current children cumulated CPU time (s) 126.94
Current children cumulated vsize (Kb) 234668

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) T 4023 4023 19818 0 -1 0 76368 0 0 0 13343 308 0 0 25 0 1 0 1854669040 260886528 63159 4294967295 134512640 135167914 3221224448 3221036924 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/4028/statm): 63693 63159 162 162 0 63531 0
[pid=4028] vsize: 254772
Current children cumulated CPU time (s) 136.57
Current children cumulated vsize (Kb) 256900

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 81795 0 0 0 14285 333 0 0 25 0 1 0 1854669040 283070464 68586 4294967295 134512640 135167914 3221224448 3221039936 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 69109 68586 162 162 0 68947 0
[pid=4028] vsize: 276436
Current children cumulated CPU time (s) 146.24
Current children cumulated vsize (Kb) 278564

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 87208 0 0 0 15227 358 0 0 25 0 1 0 1854669040 305225728 73999 4294967295 134512640 135167914 3221224448 3221037716 134697371 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 74518 73999 162 162 0 74356 0
[pid=4028] vsize: 298072
Current children cumulated CPU time (s) 155.91
Current children cumulated vsize (Kb) 300200

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 112849 0 0 0 16134 424 0 0 25 0 1 0 1854669040 410238976 99640 4294967295 134512640 135167914 3221224448 3221037344 134625423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 100156 99640 162 162 0 99994 0
[pid=4028] vsize: 400624
Current children cumulated CPU time (s) 165.64
Current children cumulated vsize (Kb) 402752

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 113953 0 0 0 17118 433 0 0 25 0 1 0 1854669040 371560448 90198 4294967295 134512640 135167914 3221224448 3221037340 134694368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90713 90198 162 162 0 90551 0
[pid=4028] vsize: 362852
Current children cumulated CPU time (s) 175.57
Current children cumulated vsize (Kb) 364980

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 119565 0 0 0 18056 460 0 0 25 0 1 0 1854669040 394534912 95810 4294967295 134512640 135167914 3221224448 3221037984 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 96322 95810 162 162 0 96160 0
[pid=4028] vsize: 385288
Current children cumulated CPU time (s) 185.22
Current children cumulated vsize (Kb) 387416

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) T 4023 4023 19818 0 -1 0 125096 0 0 0 18995 485 0 0 25 0 1 0 1854669040 417177600 101341 4294967295 134512640 135167914 3221224448 3221036876 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/4028/statm): 101850 101341 162 162 0 101688 0
[pid=4028] vsize: 407400
Current children cumulated CPU time (s) 194.86
Current children cumulated vsize (Kb) 409528

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) T 4023 4023 19818 0 -1 0 130743 0 0 0 19932 513 0 0 25 0 1 0 1854669040 439959552 106905 4294967295 134512640 135167914 3221224448 3221037852 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/4028/statm): 107412 106905 162 162 0 107250 0
[pid=4028] vsize: 429648
Current children cumulated CPU time (s) 204.51
Current children cumulated vsize (Kb) 431776

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135242 0 0 0 20883 533 0 0 25 0 1 0 1854669040 458346496 111404 4294967295 134512640 135167914 3221224448 3221223232 134623592 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 111901 111404 162 162 0 111739 0
[pid=4028] vsize: 447604
Current children cumulated CPU time (s) 214.22
Current children cumulated vsize (Kb) 449732

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 21878 537 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221222984 134846907 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 224.21
Current children cumulated vsize (Kb) 365368

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 22878 537 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215584 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 234.21
Current children cumulated vsize (Kb) 365368

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 23878 538 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215612 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 244.22
Current children cumulated vsize (Kb) 365368

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 24878 538 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215664 134629143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 254.22
Current children cumulated vsize (Kb) 365368

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 25878 538 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216272 134696658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 264.22
Current children cumulated vsize (Kb) 365368

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 26878 538 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216240 134844866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 274.22
Current children cumulated vsize (Kb) 365368

[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 27878 538 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216272 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 284.22
Current children cumulated vsize (Kb) 365368

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 28878 539 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215808 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 294.23
Current children cumulated vsize (Kb) 365368

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 29878 539 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216096 134844720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 304.23
Current children cumulated vsize (Kb) 365368

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 30878 539 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216304 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 314.23
Current children cumulated vsize (Kb) 365368

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 31878 539 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216544 134630818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 324.23
Current children cumulated vsize (Kb) 365368

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 32878 539 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216364 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 334.23
Current children cumulated vsize (Kb) 365368

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 33878 539 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215968 134522839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 344.23
Current children cumulated vsize (Kb) 365368

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 34877 540 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216336 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 354.23
Current children cumulated vsize (Kb) 365368

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 35878 540 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215824 134522227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 364.24
Current children cumulated vsize (Kb) 365368

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 36878 540 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216480 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 374.24
Current children cumulated vsize (Kb) 365368

[startup+390.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 37878 540 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216364 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 384.24
Current children cumulated vsize (Kb) 365368

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 38877 540 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216800 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 394.23
Current children cumulated vsize (Kb) 365368

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 39877 540 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216848 134522834 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 404.23
Current children cumulated vsize (Kb) 365368

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 40877 541 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216544 134629275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 414.24
Current children cumulated vsize (Kb) 365368

[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 41877 541 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216512 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 424.24
Current children cumulated vsize (Kb) 365368

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 42877 541 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216880 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 434.24
Current children cumulated vsize (Kb) 365368

[startup+450.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 43877 541 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216000 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 444.24
Current children cumulated vsize (Kb) 365368

[startup+460.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 44877 541 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216096 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 454.24
Current children cumulated vsize (Kb) 365368

[startup+470.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 45877 542 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216320 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 464.25
Current children cumulated vsize (Kb) 365368

[startup+480.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 46877 542 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215856 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 474.25
Current children cumulated vsize (Kb) 365368

[startup+490.043 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 47877 542 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216272 134696733 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 484.25
Current children cumulated vsize (Kb) 365368

[startup+500.043 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 48876 543 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216524 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 494.25
Current children cumulated vsize (Kb) 365368

[startup+510.044 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 49876 543 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215980 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 504.25
Current children cumulated vsize (Kb) 365368

[startup+520.045 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 50876 543 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216508 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 514.25
Current children cumulated vsize (Kb) 365368

[startup+530.047 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 51876 543 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216716 134696410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 524.25
Current children cumulated vsize (Kb) 365368

[startup+540.048 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 52876 544 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216096 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 534.26
Current children cumulated vsize (Kb) 365368

[startup+550.047 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 53876 544 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216112 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 544.26
Current children cumulated vsize (Kb) 365368

[startup+560.049 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 54875 544 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216164 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 554.25
Current children cumulated vsize (Kb) 365368

[startup+570.05 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 55875 544 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221217024 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 564.25
Current children cumulated vsize (Kb) 365368

[startup+580.051 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 56875 545 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221217064 134693744 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 574.26
Current children cumulated vsize (Kb) 365368

[startup+590.051 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 57875 545 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216124 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 584.26
Current children cumulated vsize (Kb) 365368

[startup+600.052 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 58875 546 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216668 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 594.27
Current children cumulated vsize (Kb) 365368

[startup+610.053 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 59874 546 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216176 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 604.26
Current children cumulated vsize (Kb) 365368

[startup+620.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 60874 546 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216540 134693585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 614.26
Current children cumulated vsize (Kb) 365368

[startup+630.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 61874 546 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216284 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 624.26
Current children cumulated vsize (Kb) 365368

[startup+640.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 62874 547 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216400 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 634.27
Current children cumulated vsize (Kb) 365368

[startup+650.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 63874 547 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216684 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 644.27
Current children cumulated vsize (Kb) 365368

[startup+660.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 64874 547 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216360 134849087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 654.27
Current children cumulated vsize (Kb) 365368

[startup+670.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 65874 547 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221217040 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 664.27
Current children cumulated vsize (Kb) 365368

[startup+680.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 66874 547 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215756 134723267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 674.27
Current children cumulated vsize (Kb) 365368

[startup+690.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 67874 547 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215920 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 684.27
Current children cumulated vsize (Kb) 365368

[startup+700.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 68873 547 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215968 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 694.26
Current children cumulated vsize (Kb) 365368

[startup+710.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 69874 547 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216336 134694504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 704.27
Current children cumulated vsize (Kb) 365368

[startup+720.063 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 70874 547 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216480 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 714.27
Current children cumulated vsize (Kb) 365368

[startup+730.063 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 71874 548 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216688 134843064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 724.28
Current children cumulated vsize (Kb) 365368

[startup+740.065 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 72874 548 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216032 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 734.28
Current children cumulated vsize (Kb) 365368

[startup+750.065 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 73874 548 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216096 134844731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 744.28
Current children cumulated vsize (Kb) 365368

[startup+760.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 74874 548 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216344 134722513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 754.28
Current children cumulated vsize (Kb) 365368

[startup+770.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 75874 548 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216368 134629049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 764.28
Current children cumulated vsize (Kb) 365368

[startup+780.067 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 76874 548 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216704 134694364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 774.28
Current children cumulated vsize (Kb) 365368

[startup+790.068 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 77875 548 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221217056 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 784.29
Current children cumulated vsize (Kb) 365368

[startup+800.069 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 78875 548 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216992 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 794.29
Current children cumulated vsize (Kb) 365368

[startup+810.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 79875 549 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216560 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 804.3
Current children cumulated vsize (Kb) 365368

[startup+820.069 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 80875 549 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216464 134843402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 814.3
Current children cumulated vsize (Kb) 365368

[startup+830.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 81875 549 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216652 134693600 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 824.3
Current children cumulated vsize (Kb) 365368

[startup+840.071 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 82875 549 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215920 134844682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 834.3
Current children cumulated vsize (Kb) 365368

[startup+850.071 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 83875 549 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216196 134629364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 844.3
Current children cumulated vsize (Kb) 365368

[startup+860.072 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 84876 549 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216068 134844636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 854.31
Current children cumulated vsize (Kb) 365368

[startup+870.072 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 85876 549 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216512 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 864.31
Current children cumulated vsize (Kb) 365368

[startup+880.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 86876 549 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216272 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 874.31
Current children cumulated vsize (Kb) 365368

[startup+890.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 87876 549 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216500 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 884.31
Current children cumulated vsize (Kb) 365368

[startup+900.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 88876 549 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216560 134629457 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 894.31
Current children cumulated vsize (Kb) 365368

[startup+910.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 89876 549 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216512 134843402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 904.31
Current children cumulated vsize (Kb) 365368

[startup+920.075 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 90876 549 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216552 134629360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 914.31
Current children cumulated vsize (Kb) 365368

[startup+930.076 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 91877 550 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216816 134696578 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 924.33
Current children cumulated vsize (Kb) 365368

[startup+940.077 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 92877 550 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216896 134629275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 934.33
Current children cumulated vsize (Kb) 365368

[startup+950.078 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 93877 550 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216872 134722513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 944.33
Current children cumulated vsize (Kb) 365368

[startup+960.078 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 94877 550 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216656 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 954.33
Current children cumulated vsize (Kb) 365368

[startup+970.079 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 95877 550 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216656 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 964.33
Current children cumulated vsize (Kb) 365368

[startup+980.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 96877 550 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216512 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 974.33
Current children cumulated vsize (Kb) 365368

[startup+990.082 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 97878 550 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216624 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 984.34
Current children cumulated vsize (Kb) 365368

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 98876 551 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216528 134849068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 994.33
Current children cumulated vsize (Kb) 365368

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 99876 552 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216480 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1004.34
Current children cumulated vsize (Kb) 365368

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 100876 552 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221217216 134849148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1014.34
Current children cumulated vsize (Kb) 365368

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 101876 553 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216108 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1024.35
Current children cumulated vsize (Kb) 365368

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 102875 553 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216804 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1034.34
Current children cumulated vsize (Kb) 365368

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 103876 553 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216352 134849066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1044.35
Current children cumulated vsize (Kb) 365368

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 104876 554 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216528 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1054.36
Current children cumulated vsize (Kb) 365368

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 105876 554 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216816 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1064.36
Current children cumulated vsize (Kb) 365368

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 106875 554 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216716 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1074.35
Current children cumulated vsize (Kb) 365368

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 107876 554 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216624 134696342 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1084.36
Current children cumulated vsize (Kb) 365368

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 108876 554 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216284 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1094.36
Current children cumulated vsize (Kb) 365368

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 109876 555 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221217052 134722660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1104.37
Current children cumulated vsize (Kb) 365368

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 110876 555 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216624 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1114.37
Current children cumulated vsize (Kb) 365368

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 111876 555 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216812 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1124.37
Current children cumulated vsize (Kb) 365368

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 112876 555 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216976 134844691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1134.37
Current children cumulated vsize (Kb) 365368

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 113876 555 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216000 134694345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1144.37
Current children cumulated vsize (Kb) 365368

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 114876 555 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215756 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1154.37
Current children cumulated vsize (Kb) 365368

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 115877 555 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216384 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1164.38
Current children cumulated vsize (Kb) 365368

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 116876 556 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216476 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1174.38
Current children cumulated vsize (Kb) 365368

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 117877 556 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221215920 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1184.39
Current children cumulated vsize (Kb) 365368

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 118877 556 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216528 134843001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1194.39
Current children cumulated vsize (Kb) 365368

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 119877 556 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216096 134844647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1204.39
Current children cumulated vsize (Kb) 365368



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 4028
Raw data (/proc/4023/stat): 4023 (minisat+_script) S 4022 4023 19818 0 -1 0 314 395 0 0 0 1 3 2 20 0 1 0 1854669029 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4023/statm): 532 234 485 147 0 385 0
[pid=4023] vsize: 2128
Raw data (/proc/4028/stat): 4028 (minisat+_bignum) R 4023 4023 19818 0 -1 0 135243 0 0 0 119877 556 0 0 25 0 1 0 1854669040 371957760 90314 4294967295 134512640 135167914 3221224448 3221216208 134844668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4028/statm): 90810 90314 162 162 0 90648 0
[pid=4028] vsize: 363240
Current children cumulated CPU time (s) 1204.39
Current children cumulated vsize (Kb) 365368

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

Child status: 0
Real time (s): 1210.27
CPU time (s): 1204.51
CPU user time (s): 1198.78
CPU system time (s): 5.72813
CPU usage (%): 99.5239
Max. virtual memory (cumulated for all children) (Kb): 449732

Verifier Data

ERROR: no interpretation found !