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

Namesubmitted/manquinho/primes-dimacs-cnf/normalized-par32-2-c.opb
MD5SUM40e47c460002545cc2670ca84fd53082
Bench Categoryoptimization, small integers (OPTSMALLINT)
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 2606
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 2606
Number of bits of the sum of numbers in the objective function 12
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 2606
Number of bits of the biggest sum of numbers12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2606
Total number of constraints6509
Number of constraints which are clauses6509
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint3

Trace number 2194

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        927964 kB
Buffers:         31232 kB
Cached:          48140 kB
SwapCached:        732 kB
Active:          41868 kB
Inactive:        40056 kB
HighTotal:      131008 kB
HighFree:        81032 kB
LowTotal:       903652 kB
LowFree:        846932 kB
SwapTotal:     2097136 kB
SwapFree:      2095856 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            19016 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:25:36 (client local time) WITH STATUS 0 IN 1200.15 SECONDS
stats: 2572 7 1200.15 0

Solver Data

c Parsing PB file...
c Converting 6509 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6509    17852 |    2169       0        0     nan |  0.000 % |
c |       101 |    6509    17852 |    2385     101     2462    24.4 |  0.004 % |
c |       254 |    6509    17852 |    2624     254     6700    26.4 |  0.000 % |
c |       479 |    6509    17852 |    2886     479     9646    20.1 |  0.000 % |
c |       818 |    6509    17852 |    3175     818    18135    22.2 |  0.000 % |
c |      1324 |    6509    17852 |    3493    1324    25947    19.6 |  0.000 % |
c |      2083 |    6509    17852 |    3842    2083    49373    23.7 |  0.000 % |
c |      3223 |    6509    17852 |    4226    3223    66840    20.7 |  0.000 % |
c |      4935 |    6509    17852 |    4649    4935   113629    23.0 |  0.000 % |
c |      7497 |    6509    17852 |    5114    2609    59930    23.0 |  0.000 % |
c |     11341 |    6509    17852 |    5625    3849   103222    26.8 |  0.000 % |
c |     17107 |    6502    17836 |    6188    3798    98704    26.0 |  0.077 % |
c |     25756 |    6502    17836 |    6807    6122   147878    24.2 |  0.077 % |
c |     38730 |    6502    17836 |    7487    5300   120700    22.8 |  0.077 % |
c |     58191 |    6502    17836 |    8236    5807   133966    23.1 |  0.077 % |
c |     87384 |    6502    17836 |    9060    5797   134404    23.2 |  0.077 % |
c |    131173 |    6502    17836 |    9966    8389   195763    23.3 |  0.077 % |
c |    196859 |    6502    17836 |   10963    8687   237112    27.3 |  0.077 % |
c |    295385 |    6502    17836 |   12059    7459   201642    27.0 |  0.077 % |
c |    443174 |    6502    17836 |   13265    9518   210422    22.1 |  0.077 % |
c |    664857 |    6502    17836 |   14591   10972   229363    20.9 |  0.077 % |

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/16129/stat): 16129 (minisat+_script) R 16128 16129 9854 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1785048163 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/16129/statm): 174 3 169 147 0 27 0
[pid=16129] 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=16130
New process pid=16131
New process pid=16132
execve syscall for /bin/sed executable
One traced child (pid=16131) 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=16132) exited with status: 0
One traced child (pid=16130) exited with status: 0
New process pid=16133
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-par32-2-c.opb

[startup+10.0047 s]
Raw data (loadavg): 1.00 1.05 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 725 0 0 0 990 3 0 0 25 0 1 0 1785048168 3280896 712 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 801 712 145 145 0 656 0
[pid=16133] vsize: 3204
Current children cumulated CPU time (s) 9.93
Current children cumulated vsize (Kb) 5328

[startup+20.0055 s]
Raw data (loadavg): 1.00 1.05 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 725 0 0 0 1989 3 0 0 25 0 1 0 1785048168 3280896 712 4294967295 134512640 135094434 3221224448 3221223040 134551469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 801 712 145 145 0 656 0
[pid=16133] vsize: 3204
Current children cumulated CPU time (s) 19.92
Current children cumulated vsize (Kb) 5328

[startup+30.0072 s]
Raw data (loadavg): 1.00 1.05 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 725 0 0 0 2989 4 0 0 25 0 1 0 1785048168 3280896 712 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 801 712 145 145 0 656 0
[pid=16133] vsize: 3204
Current children cumulated CPU time (s) 29.93
Current children cumulated vsize (Kb) 5328

[startup+40.008 s]
Raw data (loadavg): 1.00 1.05 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 725 0 0 0 3989 4 0 0 25 0 1 0 1785048168 3280896 712 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 801 712 145 145 0 656 0
[pid=16133] vsize: 3204
Current children cumulated CPU time (s) 39.93
Current children cumulated vsize (Kb) 5328

[startup+50.0098 s]
Raw data (loadavg): 1.00 1.04 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 732 0 0 0 4988 5 0 0 25 0 1 0 1785048168 3317760 719 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 810 719 145 145 0 665 0
[pid=16133] vsize: 3240
Current children cumulated CPU time (s) 49.93
Current children cumulated vsize (Kb) 5364

[startup+60.0106 s]
Raw data (loadavg): 1.00 1.04 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 739 0 0 0 5988 5 0 0 25 0 1 0 1785048168 3350528 726 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 818 726 145 145 0 673 0
[pid=16133] vsize: 3272
Current children cumulated CPU time (s) 59.93
Current children cumulated vsize (Kb) 5396

[startup+70.0114 s]
Raw data (loadavg): 1.00 1.04 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 772 0 0 0 6987 6 0 0 25 0 1 0 1785048168 3510272 759 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 857 759 145 145 0 712 0
[pid=16133] vsize: 3428
Current children cumulated CPU time (s) 69.93
Current children cumulated vsize (Kb) 5552

[startup+80.0132 s]
Raw data (loadavg): 1.00 1.04 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 779 0 0 0 7987 6 0 0 25 0 1 0 1785048168 3543040 766 4294967295 134512640 135094434 3221224448 3221223060 134563137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 865 766 145 145 0 720 0
[pid=16133] vsize: 3460
Current children cumulated CPU time (s) 79.93
Current children cumulated vsize (Kb) 5584

[startup+90.014 s]
Raw data (loadavg): 1.00 1.04 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 779 0 0 0 8986 7 0 0 25 0 1 0 1785048168 3543040 766 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 865 766 145 145 0 720 0
[pid=16133] vsize: 3460
Current children cumulated CPU time (s) 89.93
Current children cumulated vsize (Kb) 5584

[startup+100.016 s]
Raw data (loadavg): 1.00 1.03 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 815 0 0 0 9985 8 0 0 25 0 1 0 1785048168 3686400 802 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 900 802 145 145 0 755 0
[pid=16133] vsize: 3600
Current children cumulated CPU time (s) 99.93
Current children cumulated vsize (Kb) 5724

[startup+110.018 s]
Raw data (loadavg): 1.00 1.03 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 820 0 0 0 10985 8 0 0 25 0 1 0 1785048168 3710976 807 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 906 807 145 145 0 761 0
[pid=16133] vsize: 3624
Current children cumulated CPU time (s) 109.93
Current children cumulated vsize (Kb) 5748

[startup+120.02 s]
Raw data (loadavg): 1.00 1.03 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 821 0 0 0 11984 9 0 0 25 0 1 0 1785048168 3710976 808 4294967295 134512640 135094434 3221224448 3221223072 134562078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 906 808 145 145 0 761 0
[pid=16133] vsize: 3624
Current children cumulated CPU time (s) 119.93
Current children cumulated vsize (Kb) 5748

[startup+130.022 s]
Raw data (loadavg): 1.00 1.03 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 829 0 0 0 12984 9 0 0 25 0 1 0 1785048168 3743744 816 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 914 816 145 145 0 769 0
[pid=16133] vsize: 3656
Current children cumulated CPU time (s) 129.93
Current children cumulated vsize (Kb) 5780

[startup+140.023 s]
Raw data (loadavg): 1.00 1.03 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 848 0 0 0 13983 10 0 0 25 0 1 0 1785048168 3833856 835 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 936 835 145 145 0 791 0
[pid=16133] vsize: 3744
Current children cumulated CPU time (s) 139.93
Current children cumulated vsize (Kb) 5868

[startup+150.025 s]
Raw data (loadavg): 1.00 1.03 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 893 0 0 0 14983 10 0 0 25 0 1 0 1785048168 4014080 880 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 980 880 145 145 0 835 0
[pid=16133] vsize: 3920
Current children cumulated CPU time (s) 149.93
Current children cumulated vsize (Kb) 6044

[startup+160.025 s]
Raw data (loadavg): 1.00 1.03 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 907 0 0 0 15982 10 0 0 25 0 1 0 1785048168 4071424 894 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 994 894 145 145 0 849 0
[pid=16133] vsize: 3976
Current children cumulated CPU time (s) 159.92
Current children cumulated vsize (Kb) 6100

[startup+170.025 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 910 0 0 0 16982 11 0 0 25 0 1 0 1785048168 4083712 897 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 997 897 145 145 0 852 0
[pid=16133] vsize: 3988
Current children cumulated CPU time (s) 169.93
Current children cumulated vsize (Kb) 6112

[startup+180.026 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 910 0 0 0 17983 11 0 0 25 0 1 0 1785048168 4083712 897 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 997 897 145 145 0 852 0
[pid=16133] vsize: 3988
Current children cumulated CPU time (s) 179.94
Current children cumulated vsize (Kb) 6112

[startup+190.027 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 910 0 0 0 18983 11 0 0 25 0 1 0 1785048168 4083712 897 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 997 897 145 145 0 852 0
[pid=16133] vsize: 3988
Current children cumulated CPU time (s) 189.94
Current children cumulated vsize (Kb) 6112

[startup+200.028 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 910 0 0 0 19983 11 0 0 25 0 1 0 1785048168 4083712 897 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 997 897 145 145 0 852 0
[pid=16133] vsize: 3988
Current children cumulated CPU time (s) 199.94
Current children cumulated vsize (Kb) 6112

[startup+210.028 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 910 0 0 0 20983 11 0 0 25 0 1 0 1785048168 4083712 897 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 997 897 145 145 0 852 0
[pid=16133] vsize: 3988
Current children cumulated CPU time (s) 209.94
Current children cumulated vsize (Kb) 6112

[startup+220.029 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 947 0 0 0 21982 11 0 0 25 0 1 0 1785048168 4227072 934 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1032 934 145 145 0 887 0
[pid=16133] vsize: 4128
Current children cumulated CPU time (s) 219.93
Current children cumulated vsize (Kb) 6252

[startup+230.03 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 952 0 0 0 22982 11 0 0 25 0 1 0 1785048168 4259840 939 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1040 939 145 145 0 895 0
[pid=16133] vsize: 4160
Current children cumulated CPU time (s) 229.93
Current children cumulated vsize (Kb) 6284

[startup+240.031 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 952 0 0 0 23982 11 0 0 25 0 1 0 1785048168 4259840 939 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1040 939 145 145 0 895 0
[pid=16133] vsize: 4160
Current children cumulated CPU time (s) 239.93
Current children cumulated vsize (Kb) 6284

[startup+250.033 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 957 0 0 0 24983 11 0 0 25 0 1 0 1785048168 4280320 944 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1045 944 145 145 0 900 0
[pid=16133] vsize: 4180
Current children cumulated CPU time (s) 249.94
Current children cumulated vsize (Kb) 6304

[startup+260.033 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 961 0 0 0 25983 12 0 0 25 0 1 0 1785048168 4300800 948 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1050 948 145 145 0 905 0
[pid=16133] vsize: 4200
Current children cumulated CPU time (s) 259.95
Current children cumulated vsize (Kb) 6324

[startup+270.034 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 968 0 0 0 26983 12 0 0 25 0 1 0 1785048168 4329472 955 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1057 955 145 145 0 912 0
[pid=16133] vsize: 4228
Current children cumulated CPU time (s) 269.95
Current children cumulated vsize (Kb) 6352

[startup+280.036 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 977 0 0 0 27983 12 0 0 25 0 1 0 1785048168 4374528 964 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1068 964 145 145 0 923 0
[pid=16133] vsize: 4272
Current children cumulated CPU time (s) 279.95
Current children cumulated vsize (Kb) 6396

[startup+290.036 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 977 0 0 0 28983 12 0 0 25 0 1 0 1785048168 4374528 964 4294967295 134512640 135094434 3221224448 3221223072 134557711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1068 964 145 145 0 923 0
[pid=16133] vsize: 4272
Current children cumulated CPU time (s) 289.95
Current children cumulated vsize (Kb) 6396

[startup+300.036 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 985 0 0 0 29983 12 0 0 25 0 1 0 1785048168 4407296 972 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1076 972 145 145 0 931 0
[pid=16133] vsize: 4304
Current children cumulated CPU time (s) 299.95
Current children cumulated vsize (Kb) 6428

[startup+310.038 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 985 0 0 0 30983 12 0 0 25 0 1 0 1785048168 4407296 972 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1076 972 145 145 0 931 0
[pid=16133] vsize: 4304
Current children cumulated CPU time (s) 309.95
Current children cumulated vsize (Kb) 6428

[startup+320.038 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 985 0 0 0 31984 12 0 0 25 0 1 0 1785048168 4407296 972 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1076 972 145 145 0 931 0
[pid=16133] vsize: 4304
Current children cumulated CPU time (s) 319.96
Current children cumulated vsize (Kb) 6428

[startup+330.039 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 988 0 0 0 32984 12 0 0 25 0 1 0 1785048168 4423680 975 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1080 975 145 145 0 935 0
[pid=16133] vsize: 4320
Current children cumulated CPU time (s) 329.96
Current children cumulated vsize (Kb) 6444

[startup+340.04 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 988 0 0 0 33984 12 0 0 25 0 1 0 1785048168 4423680 975 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1080 975 145 145 0 935 0
[pid=16133] vsize: 4320
Current children cumulated CPU time (s) 339.96
Current children cumulated vsize (Kb) 6444

[startup+350.04 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1010 0 0 0 34983 12 0 0 25 0 1 0 1785048168 4509696 997 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1101 997 145 145 0 956 0
[pid=16133] vsize: 4404
Current children cumulated CPU time (s) 349.95
Current children cumulated vsize (Kb) 6528

[startup+360.041 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1017 0 0 0 35983 12 0 0 25 0 1 0 1785048168 4558848 1004 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1113 1004 145 145 0 968 0
[pid=16133] vsize: 4452
Current children cumulated CPU time (s) 359.95
Current children cumulated vsize (Kb) 6576

[startup+370.042 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1019 0 0 0 36984 12 0 0 25 0 1 0 1785048168 4558848 1006 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1113 1006 145 145 0 968 0
[pid=16133] vsize: 4452
Current children cumulated CPU time (s) 369.96
Current children cumulated vsize (Kb) 6576

[startup+380.043 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1026 0 0 0 37984 12 0 0 25 0 1 0 1785048168 4591616 1013 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1121 1013 145 145 0 976 0
[pid=16133] vsize: 4484
Current children cumulated CPU time (s) 379.96
Current children cumulated vsize (Kb) 6608

[startup+390.044 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1026 0 0 0 38984 13 0 0 25 0 1 0 1785048168 4591616 1013 4294967295 134512640 135094434 3221224448 3221223040 134557352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1121 1013 145 145 0 976 0
[pid=16133] vsize: 4484
Current children cumulated CPU time (s) 389.97
Current children cumulated vsize (Kb) 6608

[startup+400.045 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1026 0 0 0 39984 13 0 0 25 0 1 0 1785048168 4591616 1013 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1121 1013 145 145 0 976 0
[pid=16133] vsize: 4484
Current children cumulated CPU time (s) 399.97
Current children cumulated vsize (Kb) 6608

[startup+410.046 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1032 0 0 0 40984 13 0 0 25 0 1 0 1785048168 4624384 1019 4294967295 134512640 135094434 3221224448 3221223040 134551463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1129 1019 145 145 0 984 0
[pid=16133] vsize: 4516
Current children cumulated CPU time (s) 409.97
Current children cumulated vsize (Kb) 6640

[startup+420.046 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1038 0 0 0 41985 13 0 0 25 0 1 0 1785048168 4657152 1025 4294967295 134512640 135094434 3221224448 3221223120 134555957 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1137 1025 145 145 0 992 0
[pid=16133] vsize: 4548
Current children cumulated CPU time (s) 419.98
Current children cumulated vsize (Kb) 6672

[startup+430.047 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1044 0 0 0 42985 13 0 0 25 0 1 0 1785048168 4689920 1031 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1145 1031 145 145 0 1000 0
[pid=16133] vsize: 4580
Current children cumulated CPU time (s) 429.98
Current children cumulated vsize (Kb) 6704

[startup+440.048 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1056 0 0 0 43985 13 0 0 25 0 1 0 1785048168 4755456 1043 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 1161 1043 145 145 0 1016 0
[pid=16133] vsize: 4644
Current children cumulated CPU time (s) 439.98
Current children cumulated vsize (Kb) 6768

[startup+450.049 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1056 0 0 0 44984 13 0 0 25 0 1 0 1785048168 4755456 1043 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1161 1043 145 145 0 1016 0
[pid=16133] vsize: 4644
Current children cumulated CPU time (s) 449.97
Current children cumulated vsize (Kb) 6768

[startup+460.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1058 0 0 0 45985 13 0 0 25 0 1 0 1785048168 4755456 1045 4294967295 134512640 135094434 3221224448 3221223104 134557832 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1161 1045 145 145 0 1016 0
[pid=16133] vsize: 4644
Current children cumulated CPU time (s) 459.98
Current children cumulated vsize (Kb) 6768

[startup+470.051 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1059 0 0 0 46985 13 0 0 25 0 1 0 1785048168 4755456 1046 4294967295 134512640 135094434 3221224448 3221223136 134554728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1161 1046 145 145 0 1016 0
[pid=16133] vsize: 4644
Current children cumulated CPU time (s) 469.98
Current children cumulated vsize (Kb) 6768

[startup+480.052 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1059 0 0 0 47985 13 0 0 25 0 1 0 1785048168 4755456 1046 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1161 1046 145 145 0 1016 0
[pid=16133] vsize: 4644
Current children cumulated CPU time (s) 479.98
Current children cumulated vsize (Kb) 6768

[startup+490.052 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1069 0 0 0 48985 13 0 0 25 0 1 0 1785048168 4820992 1056 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1177 1056 145 145 0 1032 0
[pid=16133] vsize: 4708
Current children cumulated CPU time (s) 489.98
Current children cumulated vsize (Kb) 6832

[startup+500.053 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1069 0 0 0 49986 13 0 0 25 0 1 0 1785048168 4820992 1056 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1177 1056 145 145 0 1032 0
[pid=16133] vsize: 4708
Current children cumulated CPU time (s) 499.99
Current children cumulated vsize (Kb) 6832

[startup+510.054 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1069 0 0 0 50986 13 0 0 25 0 1 0 1785048168 4820992 1056 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1177 1056 145 145 0 1032 0
[pid=16133] vsize: 4708
Current children cumulated CPU time (s) 509.99
Current children cumulated vsize (Kb) 6832

[startup+520.055 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1069 0 0 0 51986 14 0 0 25 0 1 0 1785048168 4820992 1056 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1177 1056 145 145 0 1032 0
[pid=16133] vsize: 4708
Current children cumulated CPU time (s) 520
Current children cumulated vsize (Kb) 6832

[startup+530.056 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1087 0 0 0 52985 14 0 0 25 0 1 0 1785048168 4911104 1074 4294967295 134512640 135094434 3221224448 3221223072 134562051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 1199 1074 145 145 0 1054 0
[pid=16133] vsize: 4796
Current children cumulated CPU time (s) 529.99
Current children cumulated vsize (Kb) 6920

[startup+540.056 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1091 0 0 0 53984 14 0 0 25 0 1 0 1785048168 4931584 1078 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1204 1078 145 145 0 1059 0
[pid=16133] vsize: 4816
Current children cumulated CPU time (s) 539.98
Current children cumulated vsize (Kb) 6940

[startup+550.058 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1095 0 0 0 54985 14 0 0 25 0 1 0 1785048168 4947968 1082 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1208 1082 145 145 0 1063 0
[pid=16133] vsize: 4832
Current children cumulated CPU time (s) 549.99
Current children cumulated vsize (Kb) 6956

[startup+560.059 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1095 0 0 0 55985 14 0 0 25 0 1 0 1785048168 4947968 1082 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1208 1082 145 145 0 1063 0
[pid=16133] vsize: 4832
Current children cumulated CPU time (s) 559.99
Current children cumulated vsize (Kb) 6956

[startup+570.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1095 0 0 0 56985 14 0 0 25 0 1 0 1785048168 4947968 1082 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1208 1082 145 145 0 1063 0
[pid=16133] vsize: 4832
Current children cumulated CPU time (s) 569.99
Current children cumulated vsize (Kb) 6956

[startup+580.061 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1101 0 0 0 57985 14 0 0 25 0 1 0 1785048168 4980736 1088 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1216 1088 145 145 0 1071 0
[pid=16133] vsize: 4864
Current children cumulated CPU time (s) 579.99
Current children cumulated vsize (Kb) 6988

[startup+590.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1107 0 0 0 58986 14 0 0 25 0 1 0 1785048168 5013504 1094 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1224 1094 145 145 0 1079 0
[pid=16133] vsize: 4896
Current children cumulated CPU time (s) 590
Current children cumulated vsize (Kb) 7020

[startup+600.061 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1107 0 0 0 59985 14 0 0 25 0 1 0 1785048168 5013504 1094 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1224 1094 145 145 0 1079 0
[pid=16133] vsize: 4896
Current children cumulated CPU time (s) 599.99
Current children cumulated vsize (Kb) 7020

[startup+610.062 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1107 0 0 0 60986 14 0 0 25 0 1 0 1785048168 5013504 1094 4294967295 134512640 135094434 3221224448 3221223120 134555687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1224 1094 145 145 0 1079 0
[pid=16133] vsize: 4896
Current children cumulated CPU time (s) 610
Current children cumulated vsize (Kb) 7020

[startup+620.062 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1107 0 0 0 61986 14 0 0 25 0 1 0 1785048168 5013504 1094 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1224 1094 145 145 0 1079 0
[pid=16133] vsize: 4896
Current children cumulated CPU time (s) 620
Current children cumulated vsize (Kb) 7020

[startup+630.062 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1113 0 0 0 62986 14 0 0 25 0 1 0 1785048168 5046272 1100 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1232 1100 145 145 0 1087 0
[pid=16133] vsize: 4928
Current children cumulated CPU time (s) 630
Current children cumulated vsize (Kb) 7052

[startup+640.063 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1120 0 0 0 63986 14 0 0 25 0 1 0 1785048168 5079040 1107 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1240 1107 145 145 0 1095 0
[pid=16133] vsize: 4960
Current children cumulated CPU time (s) 640
Current children cumulated vsize (Kb) 7084

[startup+650.064 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1120 0 0 0 64987 14 0 0 25 0 1 0 1785048168 5079040 1107 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1240 1107 145 145 0 1095 0
[pid=16133] vsize: 4960
Current children cumulated CPU time (s) 650.01
Current children cumulated vsize (Kb) 7084

[startup+660.065 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1127 0 0 0 65987 14 0 0 25 0 1 0 1785048168 5111808 1114 4294967295 134512640 135094434 3221224448 3221223120 134555252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1248 1114 145 145 0 1103 0
[pid=16133] vsize: 4992
Current children cumulated CPU time (s) 660.01
Current children cumulated vsize (Kb) 7116

[startup+670.066 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1127 0 0 0 66987 14 0 0 25 0 1 0 1785048168 5111808 1114 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1248 1114 145 145 0 1103 0
[pid=16133] vsize: 4992
Current children cumulated CPU time (s) 670.01
Current children cumulated vsize (Kb) 7116

[startup+680.066 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1127 0 0 0 67987 15 0 0 25 0 1 0 1785048168 5111808 1114 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1248 1114 145 145 0 1103 0
[pid=16133] vsize: 4992
Current children cumulated CPU time (s) 680.02
Current children cumulated vsize (Kb) 7116

[startup+690.067 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1128 0 0 0 68987 15 0 0 25 0 1 0 1785048168 5111808 1115 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1248 1115 145 145 0 1103 0
[pid=16133] vsize: 4992
Current children cumulated CPU time (s) 690.02
Current children cumulated vsize (Kb) 7116

[startup+700.068 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1135 0 0 0 69987 15 0 0 25 0 1 0 1785048168 5144576 1122 4294967295 134512640 135094434 3221224448 3221223072 134562110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1256 1122 145 145 0 1111 0
[pid=16133] vsize: 5024
Current children cumulated CPU time (s) 700.02
Current children cumulated vsize (Kb) 7148

[startup+710.069 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1135 0 0 0 70987 16 0 0 25 0 1 0 1785048168 5144576 1122 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1256 1122 145 145 0 1111 0
[pid=16133] vsize: 5024
Current children cumulated CPU time (s) 710.03
Current children cumulated vsize (Kb) 7148

[startup+720.072 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1141 0 0 0 71986 16 0 0 25 0 1 0 1785048168 5177344 1128 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1264 1128 145 145 0 1119 0
[pid=16133] vsize: 5056
Current children cumulated CPU time (s) 720.02
Current children cumulated vsize (Kb) 7180

[startup+730.072 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1146 0 0 0 72986 17 0 0 25 0 1 0 1785048168 5210112 1133 4294967295 134512640 135094434 3221224448 3221223120 134555802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1272 1133 145 145 0 1127 0
[pid=16133] vsize: 5088
Current children cumulated CPU time (s) 730.03
Current children cumulated vsize (Kb) 7212

[startup+740.072 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1146 0 0 0 73986 17 0 0 25 0 1 0 1785048168 5210112 1133 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1272 1133 145 145 0 1127 0
[pid=16133] vsize: 5088
Current children cumulated CPU time (s) 740.03
Current children cumulated vsize (Kb) 7212

[startup+750.074 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1146 0 0 0 74987 17 0 0 25 0 1 0 1785048168 5210112 1133 4294967295 134512640 135094434 3221224448 3221223104 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1272 1133 145 145 0 1127 0
[pid=16133] vsize: 5088
Current children cumulated CPU time (s) 750.04
Current children cumulated vsize (Kb) 7212

[startup+760.075 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1146 0 0 0 75986 17 0 0 25 0 1 0 1785048168 5210112 1133 4294967295 134512640 135094434 3221224448 3221223060 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1272 1133 145 145 0 1127 0
[pid=16133] vsize: 5088
Current children cumulated CPU time (s) 760.03
Current children cumulated vsize (Kb) 7212

[startup+770.074 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1146 0 0 0 76986 18 0 0 25 0 1 0 1785048168 5210112 1133 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1272 1133 145 145 0 1127 0
[pid=16133] vsize: 5088
Current children cumulated CPU time (s) 770.04
Current children cumulated vsize (Kb) 7212

[startup+780.075 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1149 0 0 0 77986 18 0 0 25 0 1 0 1785048168 5210112 1136 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1272 1136 145 145 0 1127 0
[pid=16133] vsize: 5088
Current children cumulated CPU time (s) 780.04
Current children cumulated vsize (Kb) 7212

[startup+790.076 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1150 0 0 0 78987 18 0 0 25 0 1 0 1785048168 5210112 1137 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1272 1137 145 145 0 1127 0
[pid=16133] vsize: 5088
Current children cumulated CPU time (s) 790.05
Current children cumulated vsize (Kb) 7212

[startup+800.077 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1151 0 0 0 79986 19 0 0 25 0 1 0 1785048168 5210112 1138 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16133/statm): 1272 1138 145 145 0 1127 0
[pid=16133] vsize: 5088
Current children cumulated CPU time (s) 800.05
Current children cumulated vsize (Kb) 7212

[startup+810.078 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1179 0 0 0 80985 19 0 0 25 0 1 0 1785048168 5320704 1166 4294967295 134512640 135094434 3221224448 3221223060 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1299 1166 145 145 0 1154 0
[pid=16133] vsize: 5196
Current children cumulated CPU time (s) 810.04
Current children cumulated vsize (Kb) 7320

[startup+820.078 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1199 0 0 0 81984 20 0 0 25 0 1 0 1785048168 5419008 1186 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1323 1186 145 145 0 1178 0
[pid=16133] vsize: 5292
Current children cumulated CPU time (s) 820.04
Current children cumulated vsize (Kb) 7416

[startup+830.079 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1209 0 0 0 82985 20 0 0 25 0 1 0 1785048168 5468160 1196 4294967295 134512640 135094434 3221224448 3221223040 134557423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1335 1196 145 145 0 1190 0
[pid=16133] vsize: 5340
Current children cumulated CPU time (s) 830.05
Current children cumulated vsize (Kb) 7464

[startup+840.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1209 0 0 0 83985 20 0 0 25 0 1 0 1785048168 5468160 1196 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1335 1196 145 145 0 1190 0
[pid=16133] vsize: 5340
Current children cumulated CPU time (s) 840.05
Current children cumulated vsize (Kb) 7464

[startup+850.082 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1216 0 0 0 84985 20 0 0 25 0 1 0 1785048168 5500928 1203 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1343 1203 145 145 0 1198 0
[pid=16133] vsize: 5372
Current children cumulated CPU time (s) 850.05
Current children cumulated vsize (Kb) 7496

[startup+860.083 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1223 0 0 0 85985 20 0 0 25 0 1 0 1785048168 5533696 1210 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1351 1210 145 145 0 1206 0
[pid=16133] vsize: 5404
Current children cumulated CPU time (s) 860.05
Current children cumulated vsize (Kb) 7528

[startup+870.083 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1235 0 0 0 86985 20 0 0 25 0 1 0 1785048168 5599232 1222 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1367 1222 145 145 0 1222 0
[pid=16133] vsize: 5468
Current children cumulated CPU time (s) 870.05
Current children cumulated vsize (Kb) 7592

[startup+880.084 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1242 0 0 0 87985 20 0 0 25 0 1 0 1785048168 5632000 1229 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1375 1229 145 145 0 1230 0
[pid=16133] vsize: 5500
Current children cumulated CPU time (s) 880.05
Current children cumulated vsize (Kb) 7624

[startup+890.085 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1243 0 0 0 88986 20 0 0 25 0 1 0 1785048168 5632000 1230 4294967295 134512640 135094434 3221224448 3221223104 134557856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1375 1230 145 145 0 1230 0
[pid=16133] vsize: 5500
Current children cumulated CPU time (s) 890.06
Current children cumulated vsize (Kb) 7624

[startup+900.086 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1249 0 0 0 89986 21 0 0 25 0 1 0 1785048168 5664768 1236 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1383 1236 145 145 0 1238 0
[pid=16133] vsize: 5532
Current children cumulated CPU time (s) 900.07
Current children cumulated vsize (Kb) 7656

[startup+910.087 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1249 0 0 0 90986 21 0 0 25 0 1 0 1785048168 5664768 1236 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1383 1236 145 145 0 1238 0
[pid=16133] vsize: 5532
Current children cumulated CPU time (s) 910.07
Current children cumulated vsize (Kb) 7656

[startup+920.086 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1250 0 0 0 91986 21 0 0 25 0 1 0 1785048168 5664768 1237 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1383 1237 145 145 0 1238 0
[pid=16133] vsize: 5532
Current children cumulated CPU time (s) 920.07
Current children cumulated vsize (Kb) 7656

[startup+930.088 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1256 0 0 0 92986 21 0 0 25 0 1 0 1785048168 5697536 1243 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1391 1243 145 145 0 1246 0
[pid=16133] vsize: 5564
Current children cumulated CPU time (s) 930.07
Current children cumulated vsize (Kb) 7688

[startup+940.089 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1257 0 0 0 93986 21 0 0 25 0 1 0 1785048168 5697536 1244 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1391 1244 145 145 0 1246 0
[pid=16133] vsize: 5564
Current children cumulated CPU time (s) 940.07
Current children cumulated vsize (Kb) 7688

[startup+950.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1257 0 0 0 94986 21 0 0 25 0 1 0 1785048168 5697536 1244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1391 1244 145 145 0 1246 0
[pid=16133] vsize: 5564
Current children cumulated CPU time (s) 950.07
Current children cumulated vsize (Kb) 7688

[startup+960.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1257 0 0 0 95987 21 0 0 25 0 1 0 1785048168 5697536 1244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1391 1244 145 145 0 1246 0
[pid=16133] vsize: 5564
Current children cumulated CPU time (s) 960.08
Current children cumulated vsize (Kb) 7688

[startup+970.091 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1259 0 0 0 96987 21 0 0 25 0 1 0 1785048168 5697536 1246 4294967295 134512640 135094434 3221224448 3221223104 134561750 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1391 1246 145 145 0 1246 0
[pid=16133] vsize: 5564
Current children cumulated CPU time (s) 970.08
Current children cumulated vsize (Kb) 7688

[startup+980.092 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1267 0 0 0 97987 21 0 0 25 0 1 0 1785048168 5730304 1254 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1399 1254 145 145 0 1254 0
[pid=16133] vsize: 5596
Current children cumulated CPU time (s) 980.08
Current children cumulated vsize (Kb) 7720

[startup+990.093 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1268 0 0 0 98987 21 0 0 25 0 1 0 1785048168 5730304 1255 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1399 1255 145 145 0 1254 0
[pid=16133] vsize: 5596
Current children cumulated CPU time (s) 990.08
Current children cumulated vsize (Kb) 7720

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1268 0 0 0 99987 21 0 0 25 0 1 0 1785048168 5730304 1255 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1399 1255 145 145 0 1254 0
[pid=16133] vsize: 5596
Current children cumulated CPU time (s) 1000.08
Current children cumulated vsize (Kb) 7720

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1268 0 0 0 100987 21 0 0 25 0 1 0 1785048168 5730304 1255 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1399 1255 145 145 0 1254 0
[pid=16133] vsize: 5596
Current children cumulated CPU time (s) 1010.08
Current children cumulated vsize (Kb) 7720

[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1268 0 0 0 101988 21 0 0 25 0 1 0 1785048168 5730304 1255 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1399 1255 145 145 0 1254 0
[pid=16133] vsize: 5596
Current children cumulated CPU time (s) 1020.09
Current children cumulated vsize (Kb) 7720

[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1268 0 0 0 102988 21 0 0 25 0 1 0 1785048168 5730304 1255 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1399 1255 145 145 0 1254 0
[pid=16133] vsize: 5596
Current children cumulated CPU time (s) 1030.09
Current children cumulated vsize (Kb) 7720

[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1268 0 0 0 103988 21 0 0 25 0 1 0 1785048168 5730304 1255 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1399 1255 145 145 0 1254 0
[pid=16133] vsize: 5596
Current children cumulated CPU time (s) 1040.09
Current children cumulated vsize (Kb) 7720

[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1270 0 0 0 104988 22 0 0 25 0 1 0 1785048168 5730304 1257 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1399 1257 145 145 0 1254 0
[pid=16133] vsize: 5596
Current children cumulated CPU time (s) 1050.1
Current children cumulated vsize (Kb) 7720

[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1271 0 0 0 105988 22 0 0 25 0 1 0 1785048168 5730304 1258 4294967295 134512640 135094434 3221224448 3221223120 134556111 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1399 1258 145 145 0 1254 0
[pid=16133] vsize: 5596
Current children cumulated CPU time (s) 1060.1
Current children cumulated vsize (Kb) 7720

[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1279 0 0 0 106988 22 0 0 25 0 1 0 1785048168 5791744 1266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1414 1266 145 145 0 1269 0
[pid=16133] vsize: 5656
Current children cumulated CPU time (s) 1070.1
Current children cumulated vsize (Kb) 7780

[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1279 0 0 0 107989 22 0 0 25 0 1 0 1785048168 5791744 1266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1414 1266 145 145 0 1269 0
[pid=16133] vsize: 5656
Current children cumulated CPU time (s) 1080.11
Current children cumulated vsize (Kb) 7780

[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1280 0 0 0 108989 22 0 0 25 0 1 0 1785048168 5791744 1267 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1414 1267 145 145 0 1269 0
[pid=16133] vsize: 5656
Current children cumulated CPU time (s) 1090.11
Current children cumulated vsize (Kb) 7780

[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1281 0 0 0 109989 22 0 0 25 0 1 0 1785048168 5791744 1268 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1414 1268 145 145 0 1269 0
[pid=16133] vsize: 5656
Current children cumulated CPU time (s) 1100.11
Current children cumulated vsize (Kb) 7780

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1286 0 0 0 110989 22 0 0 25 0 1 0 1785048168 5824512 1273 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1422 1273 145 145 0 1277 0
[pid=16133] vsize: 5688
Current children cumulated CPU time (s) 1110.11
Current children cumulated vsize (Kb) 7812

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1287 0 0 0 111989 22 0 0 25 0 1 0 1785048168 5824512 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1422 1274 145 145 0 1277 0
[pid=16133] vsize: 5688
Current children cumulated CPU time (s) 1120.11
Current children cumulated vsize (Kb) 7812

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1287 0 0 0 112989 22 0 0 25 0 1 0 1785048168 5824512 1274 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1422 1274 145 145 0 1277 0
[pid=16133] vsize: 5688
Current children cumulated CPU time (s) 1130.11
Current children cumulated vsize (Kb) 7812

[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1287 0 0 0 113990 22 0 0 25 0 1 0 1785048168 5824512 1274 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1422 1274 145 145 0 1277 0
[pid=16133] vsize: 5688
Current children cumulated CPU time (s) 1140.12
Current children cumulated vsize (Kb) 7812

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1287 0 0 0 114990 22 0 0 25 0 1 0 1785048168 5824512 1274 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1422 1274 145 145 0 1277 0
[pid=16133] vsize: 5688
Current children cumulated CPU time (s) 1150.12
Current children cumulated vsize (Kb) 7812

[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1287 0 0 0 115990 22 0 0 25 0 1 0 1785048168 5824512 1274 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1422 1274 145 145 0 1277 0
[pid=16133] vsize: 5688
Current children cumulated CPU time (s) 1160.12
Current children cumulated vsize (Kb) 7812

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1287 0 0 0 116991 22 0 0 25 0 1 0 1785048168 5824512 1274 4294967295 134512640 135094434 3221224448 3221223072 134557724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1422 1274 145 145 0 1277 0
[pid=16133] vsize: 5688
Current children cumulated CPU time (s) 1170.13
Current children cumulated vsize (Kb) 7812

[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1287 0 0 0 117991 22 0 0 25 0 1 0 1785048168 5824512 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1422 1274 145 145 0 1277 0
[pid=16133] vsize: 5688
Current children cumulated CPU time (s) 1180.13
Current children cumulated vsize (Kb) 7812

[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1287 0 0 0 118991 22 0 0 25 0 1 0 1785048168 5824512 1274 4294967295 134512640 135094434 3221224448 3221223104 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1422 1274 145 145 0 1277 0
[pid=16133] vsize: 5688
Current children cumulated CPU time (s) 1190.13
Current children cumulated vsize (Kb) 7812

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1287 0 0 0 119991 22 0 0 25 0 1 0 1785048168 5824512 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1422 1274 145 145 0 1277 0
[pid=16133] vsize: 5688
Current children cumulated CPU time (s) 1200.13
Current children cumulated vsize (Kb) 7812



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16133
Raw data (/proc/16129/stat): 16129 (minisat+_script) S 16128 16129 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1785048163 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16129/statm): 531 226 485 147 0 384 0
[pid=16129] vsize: 2124
Raw data (/proc/16133/stat): 16133 (minisat+_64-bit) R 16129 16129 9854 0 -1 0 1287 0 0 0 119991 22 0 0 25 0 1 0 1785048168 5824512 1274 4294967295 134512640 135094434 3221224448 3221223172 134555088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16133/statm): 1422 1274 145 145 0 1277 0
[pid=16133] vsize: 5688
Current children cumulated CPU time (s) 1200.13
Current children cumulated vsize (Kb) 7812

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

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.15
CPU user time (s): 1199.92
CPU system time (s): 0.232964
CPU usage (%): 100.003
Max. virtual memory (cumulated for all children) (Kb): 7812

Verifier Data

ERROR: no interpretation found !