Some explanations

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

General information on the benchmark

Namemps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-sc50b.opb
MD5SUMf10dfcccbc5d23245c6e708690ee08ea
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -60000
Optimality of the best value was proved NO
Number of terms in the objective function 30
Biggest coefficient in the objective function 536870912
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 1073741823
Number of bits of the sum of numbers in the objective function 30
Biggest number in a constraint 5905580032
Number of bits of the biggest number in a constraint 33
Biggest sum of numbers in a constraint 22548578283
Number of bits of the biggest sum of numbers35
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.38
Number of variables1440
Total number of constraints48
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints48
Minimum length of a constraint60
Maximum length of a constraint120

Trace number 2666

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        902672 kB
Buffers:         35584 kB
Cached:          69464 kB
SwapCached:        896 kB
Active:          70148 kB
Inactive:        37528 kB
HighTotal:      131008 kB
HighFree:        60172 kB
LowTotal:       903652 kB
LowFree:        842500 kB
SwapTotal:     2097892 kB
SwapFree:      2096496 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            18724 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:50:41 (client local time) WITH STATUS 10 IN 1208.77 SECONDS
stats: 2800 7 1208.77 10

Solver Data

c Parsing PB file...
c Converting 68 PB-constraints to clauses...
c   -- Unit propagations: ppppppp
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[  67]---> Sorter-cost:  364     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> BDD-cost:   52
c ---[  63]---> BDD-cost:   49
c ---[  61]---> BDD-cost:   49
c ---[  59]---> BDD-cost:   49
c ---[  58]---> BDD-cost:   49
c ---[  57]---> BDD-cost:   49
c ---[  56]---> BDD-cost:   49
c ---[  55]---> Sorter-cost: 1585     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[  54]---> Sorter-cost:  375     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[  51]---> Sorter-cost:  977     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  49]---> BDD-cost:  164
c ---[  47]---> BDD-cost:  155
c ---[  45]---> BDD-cost:  155
c ---[  43]---> BDD-cost:  155
c ---[  42]---> BDD-cost:   55
c ---[  41]---> BDD-cost:   55
c ---[  40]---> BDD-cost:   55
c ---[  39]---> Sorter-cost: 1776     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[  38]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[  35]---> Sorter-cost: 1041     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  33]---> BDD-cost:  177
c ---[  31]---> BDD-cost:  168
c ---[  29]---> BDD-cost:  168
c ---[  27]---> BDD-cost:  168
c ---[  26]---> BDD-cost:   58
c ---[  25]---> BDD-cost:   58
c ---[  24]---> BDD-cost:   58
c ---[  23]---> Sorter-cost: 1841     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[  22]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  775     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[  19]---> Sorter-cost: 1105     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  17]---> BDD-cost:  186
c ---[  15]---> BDD-cost:  173
c ---[  13]---> BDD-cost:  173
c ---[  11]---> BDD-cost:  173
c ---[  10]---> BDD-cost:   61
c ---[   9]---> BDD-cost:   61
c ---[   8]---> BDD-cost:   61
c ---[   7]---> Sorter-cost: 1951     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[   6]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  814     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[   3]---> Sorter-cost: 1166     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[   2]---> Sorter-cost: 1785     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[   1]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  775     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   54002   128500 |   18000       0        0     nan |  0.000 % |
c |       100 |   53990   128473 |   19800      96      994    10.4 |  4.908 % |
c |       250 |   53990   128473 |   21780     246     2835    11.5 |  4.908 % |
c |       475 |   53888   128241 |   23958     466     8025    17.2 |  5.026 % |
c |       813 |   53840   128134 |   26353     801    15304    19.1 |  5.093 % |
c |      1319 |   53838   128130 |   28989    1306    24435    18.7 |  5.097 % |
c |      2079 |   53838   128130 |   31888    2066    34611    16.8 |  5.097 % |
c |      3218 |   53668   127750 |   35076    3160    52130    16.5 |  5.339 % |
c |      4928 |   53642   127698 |   38584    4856    80042    16.5 |  5.400 % |
c |      7491 |   52982   126198 |   42443    7363   112577    15.3 |  6.412 % |
c ==============================================================================
c Found solution: 0
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8656 |   52983   126212 |   17661    8528   138481    16.2 |  6.412 % |
c |      8756 |   52956   126154 |   19427    8622   139763    16.2 |  6.459 % |
c |      8907 |   52956   126154 |   21369    8773   142202    16.2 |  6.459 % |
c |      9132 |   52956   126154 |   23506    8998   146306    16.3 |  6.459 % |
c |      9469 |   52956   126154 |   25857    9335   150772    16.2 |  6.459 % |
c |      9975 |   52956   126154 |   28443    9841   159424    16.2 |  6.459 % |
c |     10734 |   52932   126102 |   31287   10596   170984    16.1 |  6.497 % |
c |     11873 |   52912   126061 |   34416   11725   192917    16.5 |  6.539 % |
c |     13581 |   52065   124063 |   37857   12978   214968    16.6 |  7.684 % |
c ==============================================================================
c Found solution: -30000
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15637 |   52075   124088 |   17358   15033   265477    17.7 |  7.684 % |
c |     15737 |   52075   124088 |   19093   15133   267118    17.7 |  7.690 % |
c |     15887 |   52075   124088 |   21003   15283   272259    17.8 |  7.690 % |
c |     16112 |   52054   124041 |   23103   15507   276466    17.8 |  7.719 % |
c |     16449 |   52032   123992 |   25413   15843   285028    18.0 |  7.752 % |
c |     16956 |   52032   123992 |   27955   16350   296518    18.1 |  7.752 % |
c |     17715 |   52030   123988 |   30750   17108   310980    18.2 |  7.757 % |
c |     18854 |   52026   123980 |   33825   18244   330875    18.1 |  7.766 % |
c ==============================================================================
c Found solution: -50000
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19376 |   52037   124008 |   17345   18766   339167    18.1 |  7.766 % |
c |     19476 |   52037   124008 |   19079   18866   340216    18.0 |  7.769 % |
c |     19627 |   52037   124008 |   20987   19017   342688    18.0 |  7.769 % |
c |     19852 |   52037   124008 |   23086   19242   348402    18.1 |  7.769 % |
c |     20189 |   51774   123409 |   25394   19532   352536    18.0 |  8.166 % |
c |     20697 |   51705   123245 |   27934   20037   363238    18.1 |  8.303 % |
c |     21456 |   51508   122779 |   30727   20682   376383    18.2 |  8.619 % |
c |     22595 |   51408   122541 |   33800   21808   402624    18.5 |  8.822 % |
c ==============================================================================
c Found solution: -60000
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22735 |   51383   122483 |   17127   21640   397595    18.4 |  8.822 % |
c |     22835 |   51383   122483 |   18839   10920   167739    15.4 |  8.824 % |
c |     22987 |   51376   122468 |   20723   11071   169187    15.3 |  8.833 % |
c |     23212 |   51376   122468 |   22796   11296   171562    15.2 |  8.833 % |
c |     23552 |   51376   122468 |   25075   11636   181634    15.6 |  8.833 % |
c |     24058 |   51278   122237 |   27583   12071   198172    16.4 |  8.999 % |
c |     24817 |   51151   121930 |   30341   12756   233513    18.3 |  9.192 % |
c |     25958 |   51144   121915 |   33375   13895   270608    19.5 |  9.202 % |
c |     27668 |   51056   121705 |   36713   15564   364382    23.4 |  9.391 % |
c |     30230 |   51056   121705 |   40384   18126   454277    25.1 |  9.391 % |
c |     34074 |   51013   121609 |   44423   21784   661037    30.3 |  9.448 % |
c |     39840 |   50905   121361 |   48865   27427  1030725    37.6 |  9.617 % |
c |     48490 |   49715   118579 |   53751   34568  1531234    44.3 | 11.308 % |
c |     61464 |   49553   118205 |   59127   47449  2188975    46.1 | 11.540 % |
c |     80925 |   49553   118205 |   65039   66910  3006402    44.9 | 11.540 % |
c |    110119 |   49553   118205 |   71543   38940  3121225    80.2 | 11.541 % |
c |    153908 |   49496   118079 |   78698   19529  1721062    88.1 | 11.630 % |
c |    219593 |   49251   117508 |   86567   85205  8444929    99.1 | 12.009 % |
c |    318121 |   49249   117504 |   95224   30743  2877854    93.6 | 12.012 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -COL00004_bit_10 -COL00004_bit_9 -COL00004_bit_8 -COL00004_bit_7 -COL00004_bit_6 COL00004_bit_5 COL00004_bit_4 -COL00004_bit_3 -COL00004_bit_2 COL00004_bit_1 -COL00004_bit0 COL00004_bit1 -COL00004_bit2 COL00004_bit3 COL00004_bit4 COL00004_bit5 -COL00004_bit6 -COL00004_bit7 -COL00004_bit8 -COL00004_bit9 -COL00004_bit10 -COL00004_bit11 -COL00004_bit12 -COL00004_bit13 -COL00004_bit14 -COL00004_bit15 -COL00004_bit16 -COL00004_bit17 -COL00004_bit18 -COL00004_bit19 -COL00001_bit_10 -COL00001_bit_9 -COL00001_bit_8 -COL00001_bit_7 -COL00001_bit_6 -COL00001_bit_5 -COL00001_bit_4 -COL00001_bit_3 -COL00001_bit_2 -COL00001_bit_1 -COL00001_bit0 -COL00001_bit1 -COL00001_bit2 -COL00001_bit3 -COL00001_bit4 -COL00001_bit5 -COL00001_bit6 -COL00001_bit7 -COL00001_bit8 -COL00001_bit9 -COL00001_bit10 -COL00001_bit11 -COL00001_bit12 -COL00001_bit13 -COL00001_bit14 -COL00001_bit15 -COL00001_bit16 -COL00001_bit17 -COL00001_bit18 -COL00001_bit19 -COL00002_bit_10 -COL00002_bit_9 -COL00002_bit_8 -COL00002_bit_7 -COL00002_bit_6 -COL00002_bit_5 -COL00002_bit_4 -COL00002_bit_3 -COL00002_bit_2 -COL00002_bit_1 -COL00002_bit0 -COL00002_bit1 -COL00002_bit2 COL00002_bit3 COL00002_bit4 -COL00002_bit5 -COL00002_bit6 -COL00002_bit7 -COL00002_bit8 -COL00002_bit9 -COL00002_bit10 -COL00002_bit11 -COL00002_bit12 -COL00002_bit13 -COL00002_bit14 -COL00002_bit15 -COL00002_bit16 -COL00002_bit17 -COL00002_bit18 -COL00002_bit19 -COL00003_bit_10 -COL00003_bit_9 -COL00003_bit_8 -COL00003_bit_7 -COL00003_bit_6 -COL00003_bit_5 -COL00003_bit_4 -COL00003_bit_3 -COL00003_bit_2 -COL00003_bit_1 -COL00003_bit0 -COL00003_bit1 COL00003_bit2 COL00003_bit3 -COL00003_bit4 -COL00003_bit5 COL00003_bit6 -COL00003_bit7 -COL00003_bit8 -COL00003_bit9 -COL00003_bit10 -COL00003_bit11 -COL00003_bit12 -COL00003_bit13 -COL00003_bit14 -COL00003_bit15 -COL00003_bit16 -COL00003_bit17 -COL00003_bit18 -COL00003_bit19 -COL00005_bit_10 -COL00005_bit_9 -COL00005_bit_8 -COL00005_bit_7 -COL00005_bit_6 COL00005_bit_5 COL00005_bit_4 -COL00005_bit_3 -COL00005_bit_2 COL00005_bit_1 -COL00005_bit0 COL00005_bit1 -COL00005_bit2 COL00005_bit3 COL00005_bit4 COL00005_bit5 -COL00005_bit6 -COL00005_bit7 -COL00005_bit8 -COL00005_bit9 -COL00005_bit10 -COL00005_bit11 -COL00005_bit12 -COL00005_bit13 -COL00005_bit14 -COL00005_bit15 -COL00005_bit16 -COL00005_bit17 -COL00005_bit18 -COL00005_bit19 -COL00006_bit_10 -COL00006_bit_9 -COL00006_bit_8 -COL00006_bit_7 -COL00006_bit_6 -COL00006_bit_5 -COL00006_bit_4 -COL00006_bit_3 -COL00006_bit_2 -COL00006_bit_1 -COL00006_bit0 -COL00006_bit1 -COL00006_bit2 -COL00006_bit3 -COL00006_bit4 -COL00006_bit5 -COL00006_bit6 -COL00006_bit7 -COL00006_bit8 -COL00006_bit9 -COL00006_bit10 -COL00006_bit11 -COL00006_bit12 -COL00006_bit13 -COL00006_bit14 -COL00006_bit15 -COL00006_bit16 -COL00006_bit17 -COL00006_bit18 -COL00006_bit19 -COL00007_bit_10 -COL00007_bit_9 -COL00007_bit_8 -COL00007_bit_7 -COL00007_bit_6 -COL00007_bit_5 -COL00007_bit_4 -COL00007_bit_3 -COL00007_bit_2 -COL00007_bit_1 -COL00007_bit0 -COL00007_bit1 -COL00007_bit2 COL00007_bit3 COL00007_bit4 -COL00007_bit5 -COL00007_bit6 -COL00007_bit7 -COL00007_bit8 -COL00007_bit9 -COL00007_bit10 -COL00007_bit11 -COL00007_bit12 -COL00007_bit13 -COL00007_bit14 -COL00007_bit15 -COL00007_bit16 -COL00007_bit17 -COL00007_bit18 -COL00007_bit19 -COL00008_bit_10 -COL00008_bit_9 -COL00008_bit_8 -COL00008_bit_7 -COL00008_bit_6 -COL00008_bit_5 -COL00008_bit_4 -COL00008_bit_3 -COL00008_bit_2 -COL00008_bit_1 -COL00008_bit0 -COL00008_bit1 COL00008_bit2 COL00008_bit3 -COL00008_bit4 -COL00008_bit5 COL00008_bit6 -COL00008_bit7 -COL00008_bit8 -COL00008_bit9 -COL00008_bit10 -COL00008_bit11 -COL00008_bit12 -COL00008_bit13 -COL00008_bit14 -COL00008_bit15 -COL00008_bit16 -COL00008_bit17 -COL00008_bit18 -COL00008_bit19 -COL00009_bit_10 -COL00009_bit_9 -COL00009_bit_8 -COL00009_bit_7 -COL00009_bit_6 -COL00009_bit_5 -COL00009_bit_4 -COL00009_bit_3 -COL00009_bit_2 -COL00009_bit_1 -COL00009_bit0 -COL00009_bit1 -COL00009_bit2 -COL00009_bit3 -COL00009_bit4 -COL00009_bit5 -COL00009_bit6 -COL00009_bit7 -COL00009_bit8 -COL00009_bit9 -COL00009_bit10 -COL00009_bit11 -COL00009_bit12 -COL00009_bit13 -COL00009_bit14 -COL00009_bit15 -COL00009_bit16 -COL00009_bit17 -COL00009_bit18 -COL00009_bit19 -COL00010_bit_10 -COL00010_bit_9 -COL00010_bit_8 -COL00010_bit_7 -COL00010_bit_6 -COL00010_bit_5 COL00010_bit_4 COL00010_bit_3 COL00010_bit_2 -COL00010_bit_1 COL00010_bit0 COL00010_bit1 COL00010_bit2 -COL00010_bit3 COL00010_bit4 -COL00010_bit5 -COL00010_bit6 -COL00010_bit7 -COL00010_bit8 -COL00010_bit9 -COL00010_bit10 -COL00010_bit11 -COL00010_bit12 -COL00010_bit13 -COL00010_bit14 -COL00010_bit15 -COL00010_bit16 -COL00010_bit17 -COL00010_bit18 -COL00010_bit19 COL00011_bit_10 COL00011_bit_9 -COL00011_bit_8 COL00011_bit_7 COL00011_bit_6 COL00011_bit_5 -COL00011_bit_4 -COL00011_bit_3 -COL00011_bit_2 -COL00011_bit_1 COL00011_bit0 COL00011_bit1 -COL00011_bit2 COL00011_bit3 -COL00011_bit4 -COL00011_bit5 COL00011_bit6 -COL00011_bit7 -COL00011_bit8 -COL00011_bit9 -COL00011_bit10 -COL00011_bit11 -COL00011_bit12 -COL00011_bit13 -COL00011_bit14 -COL00011_bit15 -COL00011_bit16 -COL00011_bit17 -COL00011_bit18 -COL00011_bit19 -COL00012_bit_10 -COL00012_bit_9 -COL00012_bit_8 -COL00012_bit_7 -COL00012_bit_6 -COL00012_bit_5 -COL00012_bit_4 -COL00012_bit_3 -COL00012_bit_2 -COL00012_bit_1 -COL00012_bit0 -COL00012_bit1 -COL00012_bit2 -COL00012_bit3 -COL00012_bit4 -COL00012_bit5 -COL00012_bit6 -COL00012_bit7 -COL00012_bit8 -COL00012_bit9 -COL00012_bit10 -COL00012_bit11 -COL00012_bit12 -COL00012_bit13 -COL00012_bit14 -COL00012_bit15 -COL00012_bit16 -COL00012_bit17 -COL00012_bit18 -COL00012_bit19 -COL00013_bit_10 -COL00013_bit_9 -COL00013_bit_8 -COL00013_bit_7 -COL00013_bit_6 -COL00013_bit_5 -COL00013_bit_4 -COL00013_bit_3 -COL00013_bit_2 -COL00013_bit_1 -COL00013_bit0 -COL00013_bit1 COL00013_bit2 COL00013_bit3 COL00013_bit4 -COL00013_bit5 -COL00013_bit6 -COL00013_bit7 -COL00013_bit8 -COL00013_bit9 -COL00013_bit10 -COL00013_bit11 -COL00013_bit12 -COL00013_bit13 -COL00013_bit14 -COL00013_bit15 -COL00013_bit16 -COL00013_bit17 -COL00013_bit18 -COL00013_bit19 -COL00014_bit_10 -COL00014_bit_9 -COL00014_bit_8 -COL00014_bit_7 -COL00014_bit_6 -COL00014_bit_5 -COL00014_bit_4 -COL00014_bit_3 -COL00014_bit_2 -COL00014_bit_1 -COL00014_bit0 -COL00014_bit1 -COL00014_bit2 COL00014_bit3 -COL00014_bit4 -COL00014_bit5 COL00014_bit6 -COL00014_bit7 -COL00014_bit8 -COL00014_bit9 -COL00014_bit10 -COL00014_bit11 -COL00014_bit12 -COL00014_bit13 -COL00014_bit14 -COL00014_bit15 -COL00014_bit16 -COL00014_bit17 -COL00014_bit18 -COL00014_bit19 -COL00015_bit_10 -COL00015_bit_9 -COL00015_bit_8 -COL00015_bit_7 COL00015_bit_6 -COL00015_bit_5 COL00015_bit_4 COL00015_bit_3 COL00015_bit_2 -COL00015_bit_1 -COL00015_bit0 -COL00015_bit1 -COL00015_bit2 -COL00015_bit3 -COL00015_bit4 -COL00015_bit5 COL00015_bit6 -COL00015_bit7 -COL00015_bit8 -COL00015_bit9 -COL00015_bit10 -COL00015_bit11 -COL00015_bit12 -COL00015_bit13 -COL00015_bit14 -COL00015_bit15 -COL00015_bit16 -COL00015_bit17 -COL00015_bit18 -COL00015_bit19 -COL00016_bit_10 -COL00016_bit_9 -COL00016_bit_8 -COL00016_bit_7 COL00016_bit_6 COL00016_bit_5 -COL00016_bit_4 -COL00016_bit_3 -COL00016_bit_2 -COL00016_bit_1 COL00016_bit0 COL00016_bit1 -COL00016_bit2 COL00016_bit3 COL00016_bit4 COL00016_bit5 COL00016_bit6 -COL00016_bit7 -COL00016_bit8 -COL00016_bit9 -COL00016_bit10 -COL00016_bit11 -COL00016_bit12 -COL00016_bit13 -COL00016_bit14 -COL00016_bit15 -COL00016_bit16 -COL00016_bit17 -COL00016_bit18 -COL00016_bit19 -COL00017_bit_10 -COL00017_bit_9 -COL00017_bit_8 -COL00017_bit_7 -COL00017_bit_6 -COL00017_bit_5 -COL00017_bit_4 -COL00017_bit_3 -COL00017_bit_2 -COL00017_bit_1 -COL00017_bit0 -COL00017_bit1 -COL00017_bit2 -COL00017_bit3 -COL00017_bit4 -COL00017_bit5 -COL00017_bit6 -COL00017_bit7 -COL00017_bit8 -COL00017_bit9 -COL00017_bit10 -COL00017_bit11 -COL00017_bit12 -COL00017_bit13 -COL00017_bit14 -COL00017_bit15 -COL00017_bit16 -COL00017_bit17 -COL00017_bit18 -COL00017_bit19 -COL00018_bit_10 -COL00018_bit_9 -COL00018_bit_8 -COL00018_bit_7 -COL00018_bit_6 -COL00018_bit_5 -COL00018_bit_4 -COL00018_bit_3 -COL00018_bit_2 -COL00018_bit_1 -COL00018_bit0 -COL00018_bit1 COL00018_bit2 -COL00018_bit3 COL00018_bit4 COL00018_bit5 -COL00018_bit6 -COL00018_bit7 -COL00018_bit8 -COL00018_bit9 -COL00018_bit10 -COL00018_bit11 -COL00018_bit12 -COL00018_bit13 -COL00018_bit14 -COL00018_bit15 -COL00018_bit16 -COL00018_bit17 -COL00018_bit18 -COL00018_bit19 -COL00019_bit_10 -COL00019_bit_9 -COL00019_bit_8 -COL00019_bit_7 -COL00019_bit_6 -COL00019_bit_5 -COL00019_bit_4 -COL00019_bit_3 -COL00019_bit_2 -COL00019_bit_1 -COL00019_bit0 -COL00019_bit1 COL00019_bit2 -COL00019_bit3 COL00019_bit4 -COL00019_bit5 -COL00019_bit6 COL00019_bit7 -COL00019_bit8 -COL00019_bit9 -COL00019_bit10 -COL00019_bit11 -COL00019_bit12 -COL00019_bit13 -COL00019_bit14 -COL00019_bit15 -COL00019_bit16 -COL00019_bit17 -COL00019_bit18 -COL00019_bit19 -COL00020_bit_10 -COL00020_bit_9 -COL00020_bit_8 -COL00020_bit_7 -COL00020_bit_6 -COL00020_bit_5 -COL00020_bit_4 -COL00020_bit_3 -COL00020_bit_2 -COL00020_bit_1 -COL00020_bit0 -COL00020_bit1 -COL00020_bit2 -COL00020_bit3 -COL00020_bit4 -COL00020_bit5 -COL00020_bit6 -COL00020_bit7 -COL00020_bit8 -COL00020_bit9 -COL00020_bit10 -COL00020_bit11 -COL00020_bit12 -COL00020_bit13 -COL00020_bit14 -COL00020_bit15 -COL00020_bit16 -COL00020_bit17 -COL00020_bit18 -COL00020_bit19 -COL00021_bit_10 COL00021_bit_9 -COL00021_bit_8 -COL00021_bit_7 COL00021_bit_6 COL00021_bit_5 -COL00021_bit_4 -COL00021_bit_3 -COL00021_bit_2 COL00021_bit_1 COL00021_bit0 -COL00021_bit1 -COL00021_bit2 -COL00021_bit3 COL00021_bit4 COL00021_bit5 -COL00021_bit6 -COL00021_bit7 -COL00021_bit8 -COL00021_bit9 -COL00021_bit10 -COL00021_bit11 -COL00021_bit12 -COL00021_bit13 -COL00021_bit14 -COL00021_bit15 -COL00021_bit16 -COL00021_bit17 -COL00021_bit18 -COL00021_bit19 COL00022_bit_10 COL00022_bit_9 -COL00022_bit_8 COL00022_bit_7 COL00022_bit_6 COL00022_bit_5 -COL00022_bit_4 -COL00022_bit_3 -COL00022_bit_2 COL00022_bit_1 -COL00022_bit0 COL00022_bit1 COL00022_bit2 -COL00022_bit3 COL00022_bit4 -COL00022_bit5 COL00022_bit6 -COL00022_bit7 -COL00022_bit8 -COL00022_bit9 -COL00022_bit10 -COL00022_bit11 -COL00022_bit12 -COL00022_bit13 -COL00022_bit14 -COL00022_bit15 -COL00022_bit16 -COL00022_bit17 -COL00022_bit18 -COL00022_bit19 -COL00023_bit_10 -COL00023_bit_9 -COL00023_bit_8 -COL00023_bit_7 -COL00023_bit_6 -COL00023_bit_5 COL00023_bit_4 COL00023_bit_3 COL00023_bit_2 COL00023_bit_1 -COL00023_bit0 COL00023_bit1 COL00023_bit2 -COL00023_bit3 COL00023_bit4 COL00023_bit5 -COL00023_bit6 -COL00023_bit7 -COL00023_bit8 -COL00023_bit9 -COL00023_bit10 -COL00023_bit11 -COL00023_bit12 -COL00023_bit13 -COL00023_bit14 -COL00023_bit15 -COL00023_bit16 -COL00023_bit17 -COL00023_bit18 -COL00023_bit19 -COL00024_bit_10 -COL00024_bit_9 -COL00024_bit_8 -COL00024_bit_7 -COL00024_bit_6 COL00024_bit_5 -COL00024_bit_4 COL00024_bit_3 COL00024_bit_2 COL00024_bit_1 COL00024_bit0 COL00024_bit1 COL00024_bit2 COL00024_bit3 COL00024_bit4 -COL00024_bit5 -COL00024_bit6 -COL00024_bit7 -COL00024_bit8 -COL00024_bit9 -COL00024_bit10 -COL00024_bit11 -COL00024_bit12 -COL00024_bit13 -COL00024_bit14 -COL00024_bit15 -COL00024_bit16 -COL00024_bit17 -COL00024_bit18 -COL00024_bit19 -COL00025_bit_10 -COL00025_bit_9 -COL00025_bit_8 -COL00025_bit_7 -COL00025_bit_6 -COL00025_bit_5 -COL00025_bit_4 COL00025_bit_3 COL00025_bit_2 COL00025_bit_1 -COL00025_bit0 COL00025_bit1 COL00025_bit2 -COL00025_bit3 -COL00025_bit4 -COL00025_bit5 -COL00025_bit6 -COL00025_bit7 -COL00025_bit8 -COL00025_bit9 -COL00025_bit10 -COL00025_bit11 -COL00025_bit12 -COL00025_bit13 -COL00025_bit14 -COL00025_bit15 -COL00025_bit16 -COL00025_bit17 -COL00025_bit18 -COL00025_bit19 -COL00026_bit_10 -COL00026_bit_9 -COL00026_bit_8 COL00026_bit_7 COL00026_bit_6 -COL00026_bit_5 -COL00026_bit_4 COL00026_bit_3 COL00026_bit_2 COL00026_bit_1 -COL00026_bit0 COL00026_bit1 COL00026_bit2 -COL00026_bit3 -COL00026_bit4 -COL00026_bit5 COL00026_bit6 -COL00026_bit7 -COL00026_bit8 -COL00026_bit9 -COL00026_bit10 -COL00026_bit11 -COL00026_bit12 -COL00026_bit13 -COL00026_bit14 -COL00026_bit15 -COL00026_bit16 -COL00026_bit17 -COL00026_bit18 -COL00026_bit19 -COL00027_bit_10 -COL00027_bit_9 -COL00027_bit_8 COL00027_bit_7 -COL00027_bit_6 -COL00027_bit_5 COL00027_bit_4 COL00027_bit_3 COL00027_bit_2 COL00027_bit_1 COL00027_bit0 -COL00027_bit1 -COL00027_bit2 -COL00027_bit3 -COL00027_bit4 -COL00027_bit5 COL00027_bit6 COL00027_bit7 -COL00027_bit8 -COL00027_bit9 -COL00027_bit10 -COL00027_bit11 -COL00027_bit12 -COL00027_bit13 -COL00027_bit14 -COL00027_bit15 -COL00027_bit16 -COL00027_bit17 -COL00027_bit18 -COL00027_bit19 -COL00028_bit_10 -COL00028_bit_9 -COL00028_bit_8 -COL00028_bit_7 -COL00028_bit_6 -COL00028_bit_5 COL00028_bit_4 COL00028_bit_3 COL00028_bit_2 COL00028_bit_1 -COL00028_bit0 COL00028_bit1 COL00028_bit2 -COL00028_bit3 COL00028_bit4 COL00028_bit5 -COL00028_bit6 -COL00028_bit7 -COL00028_bit8 -COL00028_bit9 -COL00028_bit10 -COL00028_bit11 -COL00028_bit12 -COL00028_bit13 -COL00028_bit14 -COL00028_bit15 -COL00028_bit16 -COL00028_bit17 -COL00028_bit18 -COL00028_bit19 -COL00029_bit_10 -COL00029_bit_9 -COL00029_bit_8 -COL00029_bit_7 -COL00029_bit_6 COL00029_bit_5 -COL00029_bit_4 COL00029_bit_3 COL00029_bit_2 COL00029_bit_1 COL00029_bit0 COL00029_bit1 -COL00029_bit2 -COL00029_bit3 COL00029_bit4 -COL00029_bit5 COL00029_bit6 -COL00029_bit7 -COL00029_bit8 -COL00029_bit9 -COL00029_bit10 -COL00029_bit11 -COL00029_bit12 -COL00029_bit13 -COL00029_bit14 -COL00029_bit15 -COL00029_bit16 -COL00029_bit17 -COL00029_bit18 -COL00029_bit19 -COL00030_bit_10 -COL00030_bit_9 -COL00030_bit_8 -COL00030_bit_7 -COL00030_bit_6 -COL00030_bit_5 -COL00030_bit_4 COL00030_bit_3 COL00030_bit_2 COL00030_bit_1 -COL00030_bit0 COL00030_bit1 -COL00030_bit2 COL00030_bit3 COL00030_bit4 -COL00030_bit5 -COL00030_bit6 COL00030_bit7 -COL00030_bit8 -COL00030_bit9 -COL00030_bit10 -COL00030_bit11 -COL00030_bit12 -COL00030_bit13 -COL00030_bit14 -COL00030_bit15 -COL00030_bit16 -COL00030_bit17 -COL00030_bit18 -COL00030_bit19 COL00031_bit_10 COL00031_bit_9 -COL00031_bit_8 COL00031_bit_7 COL00031_bit_6 -COL00031_bit_5 -COL00031_bit_4 -COL00031_bit_3 COL00031_bit_2 COL00031_bit_1 COL00031_bit0 COL00031_bit1 -COL00031_bit2 -COL00031_bit3 COL00031_bit4 COL00031_bit5 -COL00031_bit6 -COL00031_bit7 -COL00031_bit8 -COL00031_bit9 -COL00031_bit10 -COL00031_bit11 -COL00031_bit12 -COL00031_bit13 -COL00031_bit14 -COL00031_bit15 -COL00031_bit16 -COL00031_bit17 -COL00031_bit18 -COL00031_bit19 COL00032_bit_10 COL00032_bit_9 -COL00032_bit_8 COL00032_bit_7 COL00032_bit_6 COL00032_bit_5 COL00032_bit_4 -COL00032_bit_3 -COL00032_bit_2 COL00032_bit_1 COL00032_bit0 -COL00032_bit1 COL00032_bit2 COL00032_bit3 -COL00032_bit4 -COL00032_bit5 COL00032_bit6 -COL00032_bit7 -COL00032_bit8 -COL00032_bit9 -COL00032_bit10 -COL00032_bit11 -COL00032_bit12 -COL00032_bit13 -COL00032_bit14 -COL00032_bit15 -COL00032_bit16 -COL00032_bit17 -COL00032_bit18 -COL00032_bit19 -COL00033_bit_10 -COL00033_bit_9 -COL00033_bit_8 -COL00033_bit_7 COL00033_bit_6 -COL00033_bit_5 -COL00033_bit_4 COL00033_bit_3 -COL00033_bit_2 -COL00033_bit_1 -COL00033_bit0 COL00033_bit1 COL00033_bit2 -COL00033_bit3 COL00033_bit4 -COL00033_bit5 -COL00033_bit6 COL00033_bit7 -COL00033_bit8 -COL00033_bit9 -COL00033_bit10 -COL00033_bit11 -COL00033_bit12 -COL00033_bit13 -COL00033_bit14 -COL00033_bit15 -COL00033_bit16 -COL00033_bit17 -COL00033_bit18 -COL00033_bit19 -COL00034_bit_10 COL00034_bit_9 COL00034_bit_8 COL00034_bit_7 COL00034_bit_6 COL00034_bit_5 COL00034_bit_4 COL00034_bit_3 COL00034_bit_2 COL00034_bit_1 COL00034_bit0 COL00034_bit1 COL00034_bit2 COL00034_bit3 -COL00034_bit4 -COL00034_bit5 -COL00034_bit6 -COL00034_bit7 -COL00034_bit8 -COL00034_bit9 -COL00034_bit10 -COL00034_bit11 -COL00034_bit12 -COL00034_bit13 -COL00034_bit14 -COL00034_bit15 -COL00034_bit16 -COL00034_bit17 -COL00034_bit18 -COL00034_bit19 -COL00035_bit_10 -COL00035_bit_9 -COL00035_bit_8 COL00035_bit_7 COL00035_bit_6 -COL00035_bit_5 COL00035_bit_4 -COL00035_bit_3 -COL00035_bit_2 -COL00035_bit_1 -COL00035_bit0 -COL00035_bit1 COL00035_bit2 -COL00035_bit3 -COL00035_bit4 COL00035_bit5 -COL00035_bit6 -COL00035_bit7 -COL00035_bit8 -COL00035_bit9 -COL00035_bit10 -COL00035_bit11 -COL00035_bit12 -COL00035_bit13 -COL00035_bit14 -COL00035_bit15 -COL00035_bit16 -COL00035_bit17 -COL00035_bit18 -COL00035_bit19 -COL00036_bit_10 -COL00036_bit_9 -COL00036_bit_8 -COL00036_bit_7 COL00036_bit_6 -COL00036_bit_5 -COL00036_bit_4 -COL00036_bit_3 -COL00036_bit_2 -COL00036_bit_1 COL00036_bit0 -COL00036_bit1 -COL00036_bit2 -COL00036_bit3 -COL00036_bit4 -COL00036_bit5 COL00036_bit6 -COL00036_bit7 -COL00036_bit8 -COL00036_bit9 -COL00036_bit10 -COL00036_bit11 -COL00036_bit12 -COL00036_bit13 -COL00036_bit14 -COL00036_bit15 -COL00036_bit16 -COL00036_bit17 -COL00036_bit18 -COL00036_bit19 -COL00037_bit_10 -COL00037_bit_9 COL00037_bit_8 -COL00037_bit_7 COL00037_bit_6 COL00037_bit_5 COL00037_bit_4 COL00037_bit_3 COL00037_bit_2 COL00037_bit_1 COL00037_bit0 -COL00037_bit1 COL00037_bit2 COL00037_bit3 -COL00037_bit4 -COL00037_bit5 COL00037_bit6 -COL00037_bit7 -COL00037_bit8 -COL00037_bit9 -COL00037_bit10 -COL00037_bit11 -COL00037_bit12 -COL00037_bit13 -COL00037_bit14 -COL00037_bit15 -COL00037_bit16 -COL00037_bit17 -COL00037_bit18 -COL00037_bit19 -COL00038_bit_10 -COL00038_bit_9 COL00038_bit_8 COL00038_bit_7 COL00038_bit_6 COL00038_bit_5 -COL00038_bit_4 COL00038_bit_3 COL00038_bit_2 COL00038_bit_1 COL00038_bit0 COL00038_bit1 COL00038_bit2 COL00038_bit3 -COL00038_bit4 -COL00038_bit5 -COL00038_bit6 -COL00038_bit7 COL00038_bit8 -COL00038_bit9 -COL00038_bit10 -COL00038_bit11 -COL00038_bit12 -COL00038_bit13 -COL00038_bit14 -COL00038_bit15 -COL00038_bit16 -COL00038_bit17 -COL00038_bit18 -COL00038_bit19 -COL00039_bit_10 COL00039_bit_9 COL00039_bit_8 COL00039_bit_7 COL00039_bit_6 COL00039_bit_5 -COL00039_bit_4 COL00039_bit_3 COL00039_bit_2 COL00039_bit_1 -COL00039_bit0 COL00039_bit1 COL00039_bit2 -COL00039_bit3 -COL00039_bit4 -COL00039_bit5 COL00039_bit6 -COL00039_bit7 -COL00039_bit8 -COL00039_bit9 -COL00039_bit10 -COL00039_bit11 -COL00039_bit12 -COL00039_bit13 -COL00039_bit14 -COL00039_bit15 -COL00039_bit16 -COL00039_bit17 -COL00039_bit18 -COL00039_bit19 -COL00040_bit_10 -COL00040_bit_9 -COL00040_bit_8 COL00040_bit_7 COL00040_bit_6 COL00040_bit_5 COL00040_bit_4 COL00040_bit_3 COL00040_bit_2 COL00040_bit_1 COL00040_bit0 COL00040_bit1 COL00040_bit2 -COL00040_bit3 COL00040_bit4 COL00040_bit5 COL00040_bit6 -COL00040_bit7 -COL00040_bit8 -COL00040_bit9 -COL00040_bit10 -COL00040_bit11 -COL00040_bit12 -COL00040_bit13 -COL00040_bit14 -COL00040_bit15 -COL00040_bit16 -COL00040_bit17 -COL00040_bit18 -COL00040_bit19 -COL00041_bit_10 -COL00041_bit_9 -COL00041_bit_8 -COL00041_bit_7 COL00041_bit_6 -COL00041_bit_5 -COL00041_bit_4 COL00041_bit_3 COL00041_bit_2 COL00041_bit_1 COL00041_bit0 COL00041_bit1 -COL00041_bit2 COL00041_bit3 COL00041_bit4 -COL00041_bit5 COL00041_bit6 COL00041_bit7 -COL00041_bit8 -COL00041_bit9 -COL00041_bit10 -COL00041_bit11 -COL00041_bit12 -COL00041_bit13 -COL00041_bit14 -COL00041_bit15 -COL00041_bit16 -COL00041_bit17 -COL00041_bit18 -COL00041_bit19 -COL00042_bit_10 COL00042_bit_9 COL00042_bit_8 COL00042_bit_7 COL00042_bit_6 COL00042_bit_5 -COL00042_bit_4 COL00042_bit_3 COL00042_bit_2 COL00042_bit_1 -COL00042_bit0 COL00042_bit1 COL00042_bit2 -COL00042_bit3 -COL00042_bit4 -COL00042_bit5 COL00042_bit6 -COL00042_bit7 -COL00042_bit8 -COL00042_bit9 -COL00042_bit10 -COL00042_bit11 -COL00042_bit12 -COL00042_bit13 -COL00042_bit14 -COL00042_bit15 -COL00042_bit16 -COL00042_bit17 -COL00042_bit18 -COL00042_bit19 -COL00043_bit_10 -COL00043_bit_9 -COL00043_bit_8 COL00043_bit_7 COL00043_bit_6 -COL00043_bit_5 -COL00043_bit_4 -COL00043_bit_3 COL00043_bit_2 COL00043_bit_1 -COL00043_bit0 -COL00043_bit1 COL00043_bit2 COL00043_bit3 -COL00043_bit4 COL00043_bit5 COL00043_bit6 -COL00043_bit7 -COL00043_bit8 -COL00043_bit9 -COL00043_bit10 -COL00043_bit11 -COL00043_bit12 -COL00043_bit13 -COL00043_bit14 -COL00043_bit15 -COL00043_bit16 -COL00043_bit17 -COL00043_bit18 -COL00043_bit19 COL00044_bit_10 COL00044_bit_9 -COL00044_bit_8 -COL00044_bit_7 -COL00044_bit_6 COL00044_bit_5 COL00044_bit_4 COL00044_bit_3 COL00044_bit_2 COL00044_bit_1 COL00044_bit0 COL00044_bit1 COL00044_bit2 -COL00044_bit3 -COL00044_bit4 -COL00044_bit5 COL00044_bit6 COL00044_bit7 -COL00044_bit8 -COL00044_bit9 -COL00044_bit10 -COL00044_bit11 -COL00044_bit12 -COL00044_bit13 -COL00044_bit14 -COL00044_bit15 -COL00044_bit16 -COL00044_bit17 -COL00044_bit18 -COL00044_

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/16380/stat): 16380 (minisat+_script) R 16379 16380 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844176082 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/16380/statm): 174 3 169 147 0 27 0
[pid=16380] 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=16381
New process pid=16382
New process pid=16383
execve syscall for /bin/sed executable
One traced child (pid=16382) 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=16383) exited with status: 0
One traced child (pid=16381) exited with status: 0
New process pid=16384
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-sc50b.opb

[startup+10.0034 s]
Raw data (loadavg): 0.87 0.93 0.90 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 2111 0 0 0 977 9 0 0 25 0 1 0 1844176087 9388032 2006 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16384/statm): 2292 2006 145 145 0 2147 0
[pid=16384] vsize: 9168
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 11292

[startup+20.005 s]
Raw data (loadavg): 0.89 0.93 0.90 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 2368 0 0 0 1973 11 0 0 25 0 1 0 1844176087 10518528 2263 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16384/statm): 2568 2263 145 145 0 2423 0
[pid=16384] vsize: 10272
Current children cumulated CPU time (s) 19.85
Current children cumulated vsize (Kb) 12396

[startup+30.0056 s]
Raw data (loadavg): 0.90 0.93 0.90 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 2547 0 0 0 2969 13 0 0 25 0 1 0 1844176087 11284480 2442 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16384/statm): 2755 2442 145 145 0 2610 0
[pid=16384] vsize: 11020
Current children cumulated CPU time (s) 29.83
Current children cumulated vsize (Kb) 13144

[startup+40.0062 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 2842 0 0 0 3964 15 0 0 25 0 1 0 1844176087 12496896 2737 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16384/statm): 3051 2737 145 145 0 2906 0
[pid=16384] vsize: 12204
Current children cumulated CPU time (s) 39.8
Current children cumulated vsize (Kb) 14328

[startup+50.0068 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 3304 0 0 0 4956 19 0 0 25 0 1 0 1844176087 14364672 3199 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16384/statm): 3507 3199 145 145 0 3362 0
[pid=16384] vsize: 14028
Current children cumulated CPU time (s) 49.76
Current children cumulated vsize (Kb) 16152

[startup+60.0064 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 3669 0 0 0 5949 21 0 0 25 0 1 0 1844176087 15843328 3564 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16384/statm): 3868 3564 145 145 0 3723 0
[pid=16384] vsize: 15472
Current children cumulated CPU time (s) 59.71
Current children cumulated vsize (Kb) 17596

[startup+70.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 4029 0 0 0 6941 24 0 0 25 0 1 0 1844176087 17428480 3924 4294967295 134512640 135094434 3221224432 3221223104 134555957 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 4255 3924 145 145 0 4110 0
[pid=16384] vsize: 17020
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 19144

[startup+80.0096 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 4361 0 0 0 7934 27 0 0 25 0 1 0 1844176087 18759680 4256 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 4580 4256 145 145 0 4435 0
[pid=16384] vsize: 18320
Current children cumulated CPU time (s) 79.62
Current children cumulated vsize (Kb) 20444

[startup+90.0102 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 4748 0 0 0 8927 31 0 0 25 0 1 0 1844176087 20332544 4643 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 4964 4643 145 145 0 4819 0
[pid=16384] vsize: 19856
Current children cumulated CPU time (s) 89.59
Current children cumulated vsize (Kb) 21980

[startup+100.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 4959 0 0 0 9923 33 0 0 25 0 1 0 1844176087 21180416 4854 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 5171 4854 145 145 0 5026 0
[pid=16384] vsize: 20684
Current children cumulated CPU time (s) 99.57
Current children cumulated vsize (Kb) 22808

[startup+110.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 5127 0 0 0 10920 34 0 0 25 0 1 0 1844176087 21864448 5022 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 5338 5022 145 145 0 5193 0
[pid=16384] vsize: 21352
Current children cumulated CPU time (s) 109.55
Current children cumulated vsize (Kb) 23476

[startup+120.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 5309 0 0 0 11917 35 0 0 25 0 1 0 1844176087 22589440 5204 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 5515 5204 145 145 0 5370 0
[pid=16384] vsize: 22060
Current children cumulated CPU time (s) 119.53
Current children cumulated vsize (Kb) 24184

[startup+130.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 5473 0 0 0 12912 36 0 0 25 0 1 0 1844176087 23257088 5368 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 5678 5368 145 145 0 5533 0
[pid=16384] vsize: 22712
Current children cumulated CPU time (s) 129.49
Current children cumulated vsize (Kb) 24836

[startup+140.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 5669 0 0 0 13908 38 0 0 25 0 1 0 1844176087 24322048 5564 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 5938 5564 145 145 0 5793 0
[pid=16384] vsize: 23752
Current children cumulated CPU time (s) 139.47
Current children cumulated vsize (Kb) 25876

[startup+150.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 5898 0 0 0 14905 40 0 0 25 0 1 0 1844176087 25251840 5793 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6165 5793 145 145 0 6020 0
[pid=16384] vsize: 24660
Current children cumulated CPU time (s) 149.46
Current children cumulated vsize (Kb) 26784

[startup+160.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6230 0 0 0 15898 43 0 0 25 0 1 0 1844176087 26599424 6125 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6494 6125 145 145 0 6349 0
[pid=16384] vsize: 25976
Current children cumulated CPU time (s) 159.42
Current children cumulated vsize (Kb) 28100

[startup+170.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6460 0 0 0 16894 45 0 0 25 0 1 0 1844176087 27533312 6355 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6722 6355 145 145 0 6577 0
[pid=16384] vsize: 26888
Current children cumulated CPU time (s) 169.4
Current children cumulated vsize (Kb) 29012

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 17893 45 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0
[pid=16384] vsize: 27080
Current children cumulated CPU time (s) 179.39
Current children cumulated vsize (Kb) 29204

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 18892 46 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0
[pid=16384] vsize: 27080
Current children cumulated CPU time (s) 189.39
Current children cumulated vsize (Kb) 29204

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 19892 46 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134556880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0
[pid=16384] vsize: 27080
Current children cumulated CPU time (s) 199.39
Current children cumulated vsize (Kb) 29204

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 20891 46 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0
[pid=16384] vsize: 27080
Current children cumulated CPU time (s) 209.38
Current children cumulated vsize (Kb) 29204

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 21891 47 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0
[pid=16384] vsize: 27080
Current children cumulated CPU time (s) 219.39
Current children cumulated vsize (Kb) 29204

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 22891 47 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0
[pid=16384] vsize: 27080
Current children cumulated CPU time (s) 229.39
Current children cumulated vsize (Kb) 29204

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 23891 47 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0
[pid=16384] vsize: 27080
Current children cumulated CPU time (s) 239.39
Current children cumulated vsize (Kb) 29204

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 24891 48 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0
[pid=16384] vsize: 27080
Current children cumulated CPU time (s) 249.4
Current children cumulated vsize (Kb) 29204

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 25890 48 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223104 134555953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0
[pid=16384] vsize: 27080
Current children cumulated CPU time (s) 259.39
Current children cumulated vsize (Kb) 29204

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 26889 49 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0
[pid=16384] vsize: 27080
Current children cumulated CPU time (s) 269.39
Current children cumulated vsize (Kb) 29204

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6810 0 0 0 27884 51 0 0 25 0 1 0 1844176087 28966912 6705 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 7072 6705 145 145 0 6927 0
[pid=16384] vsize: 28288
Current children cumulated CPU time (s) 279.36
Current children cumulated vsize (Kb) 30412

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 7345 0 0 0 28874 55 0 0 25 0 1 0 1844176087 31162368 7240 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16384/statm): 7608 7240 145 145 0 7463 0
[pid=16384] vsize: 30432
Current children cumulated CPU time (s) 289.3
Current children cumulated vsize (Kb) 32556

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 7839 0 0 0 29865 59 0 0 25 0 1 0 1844176087 33189888 7734 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 8103 7734 145 145 0 7958 0
[pid=16384] vsize: 32412
Current children cumulated CPU time (s) 299.25
Current children cumulated vsize (Kb) 34536

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 8238 0 0 0 30857 62 0 0 25 0 1 0 1844176087 34832384 8133 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 8504 8133 145 145 0 8359 0
[pid=16384] vsize: 34016
Current children cumulated CPU time (s) 309.2
Current children cumulated vsize (Kb) 36140

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 8630 0 0 0 31850 66 0 0 25 0 1 0 1844176087 36450304 8525 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 8899 8525 145 145 0 8754 0
[pid=16384] vsize: 35596
Current children cumulated CPU time (s) 319.17
Current children cumulated vsize (Kb) 37720

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 9159 0 0 0 32839 71 0 0 25 0 1 0 1844176087 38617088 9054 4294967295 134512640 135094434 3221224432 3221223104 134556394 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 9428 9054 145 145 0 9283 0
[pid=16384] vsize: 37712
Current children cumulated CPU time (s) 329.11
Current children cumulated vsize (Kb) 39836

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 9522 0 0 0 33831 74 0 0 25 0 1 0 1844176087 40095744 9417 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 9789 9417 145 145 0 9644 0
[pid=16384] vsize: 39156
Current children cumulated CPU time (s) 339.06
Current children cumulated vsize (Kb) 41280

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 9872 0 0 0 34825 77 0 0 25 0 1 0 1844176087 41521152 9767 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10137 9767 145 145 0 9992 0
[pid=16384] vsize: 40548
Current children cumulated CPU time (s) 349.03
Current children cumulated vsize (Kb) 42672

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 35818 80 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 358.99
Current children cumulated vsize (Kb) 43864

[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 36818 80 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 368.99
Current children cumulated vsize (Kb) 43864

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 37817 80 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 378.98
Current children cumulated vsize (Kb) 43864

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 38816 81 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 388.98
Current children cumulated vsize (Kb) 43864

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 39816 81 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 398.98
Current children cumulated vsize (Kb) 43864

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 40816 82 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 408.99
Current children cumulated vsize (Kb) 43864

[startup+420.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 41815 82 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 418.98
Current children cumulated vsize (Kb) 43864

[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 42815 83 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 428.99
Current children cumulated vsize (Kb) 43864

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 43814 83 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 438.98
Current children cumulated vsize (Kb) 43864

[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 44814 84 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 448.99
Current children cumulated vsize (Kb) 43864

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 45814 84 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 458.99
Current children cumulated vsize (Kb) 43864

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 46813 84 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 468.98
Current children cumulated vsize (Kb) 43864

[startup+480.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 47813 85 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 478.99
Current children cumulated vsize (Kb) 43864

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 48813 85 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223104 134556068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 488.99
Current children cumulated vsize (Kb) 43864

[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 49813 85 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 498.99
Current children cumulated vsize (Kb) 43864

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 50812 85 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0
[pid=16384] vsize: 41740
Current children cumulated CPU time (s) 508.98
Current children cumulated vsize (Kb) 43864

[startup+520.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10370 0 0 0 51809 87 0 0 25 0 1 0 1844176087 43569152 10265 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10637 10265 145 145 0 10492 0
[pid=16384] vsize: 42548
Current children cumulated CPU time (s) 518.97
Current children cumulated vsize (Kb) 44672

[startup+530.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10646 0 0 0 52803 90 0 0 25 0 1 0 1844176087 44699648 10541 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 10913 10541 145 145 0 10768 0
[pid=16384] vsize: 43652
Current children cumulated CPU time (s) 528.94
Current children cumulated vsize (Kb) 45776

[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10910 0 0 0 53797 92 0 0 25 0 1 0 1844176087 45780992 10805 4294967295 134512640 135094434 3221224432 3221223104 134556487 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 11177 10805 145 145 0 11032 0
[pid=16384] vsize: 44708
Current children cumulated CPU time (s) 538.9
Current children cumulated vsize (Kb) 46832

[startup+550.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 11172 0 0 0 54793 94 0 0 25 0 1 0 1844176087 46850048 11067 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 11438 11067 145 145 0 11293 0
[pid=16384] vsize: 45752
Current children cumulated CPU time (s) 548.88
Current children cumulated vsize (Kb) 47876

[startup+560.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 11437 0 0 0 55787 97 0 0 25 0 1 0 1844176087 47935488 11332 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 11703 11332 145 145 0 11558 0
[pid=16384] vsize: 46812
Current children cumulated CPU time (s) 558.85
Current children cumulated vsize (Kb) 48936

[startup+570.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 11708 0 0 0 56782 99 0 0 25 0 1 0 1844176087 49029120 11603 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 11970 11603 145 145 0 11825 0
[pid=16384] vsize: 47880
Current children cumulated CPU time (s) 568.82
Current children cumulated vsize (Kb) 50004

[startup+580.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 11907 0 0 0 57779 101 0 0 25 0 1 0 1844176087 49909760 11802 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12185 11802 145 145 0 12040 0
[pid=16384] vsize: 48740
Current children cumulated CPU time (s) 578.81
Current children cumulated vsize (Kb) 50864

[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12029 0 0 0 58777 102 0 0 25 0 1 0 1844176087 50397184 11924 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12304 11924 145 145 0 12159 0
[pid=16384] vsize: 49216
Current children cumulated CPU time (s) 588.8
Current children cumulated vsize (Kb) 51340

[startup+600.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12187 0 0 0 59774 104 0 0 25 0 1 0 1844176087 51032064 12082 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12459 12082 145 145 0 12314 0
[pid=16384] vsize: 49836
Current children cumulated CPU time (s) 598.79
Current children cumulated vsize (Kb) 51960

[startup+610.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12381 0 0 0 60771 105 0 0 25 0 1 0 1844176087 51814400 12276 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12650 12276 145 145 0 12505 0
[pid=16384] vsize: 50600
Current children cumulated CPU time (s) 608.77
Current children cumulated vsize (Kb) 52724

[startup+620.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 61766 108 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221221088 134562642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 618.75
Current children cumulated vsize (Kb) 53952

[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 62765 108 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 628.74
Current children cumulated vsize (Kb) 53952

[startup+640.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 63765 108 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 638.74
Current children cumulated vsize (Kb) 53952

[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 64765 108 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 648.74
Current children cumulated vsize (Kb) 53952

[startup+660.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 65765 108 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223104 134555855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 658.74
Current children cumulated vsize (Kb) 53952

[startup+670.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 66764 109 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 668.74
Current children cumulated vsize (Kb) 53952

[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 67764 109 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 678.74
Current children cumulated vsize (Kb) 53952

[startup+690.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 68764 109 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557339 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 688.74
Current children cumulated vsize (Kb) 53952

[startup+700.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 69763 110 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 698.74
Current children cumulated vsize (Kb) 53952

[startup+710.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 70763 110 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 708.74
Current children cumulated vsize (Kb) 53952

[startup+720.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 71762 110 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 718.73
Current children cumulated vsize (Kb) 53952

[startup+730.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 72762 111 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134556931 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 728.74
Current children cumulated vsize (Kb) 53952

[startup+740.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 73762 111 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 738.74
Current children cumulated vsize (Kb) 53952

[startup+750.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 74762 111 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 748.74
Current children cumulated vsize (Kb) 53952

[startup+760.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 75761 112 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 758.74
Current children cumulated vsize (Kb) 53952

[startup+770.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 76761 112 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 768.74
Current children cumulated vsize (Kb) 53952

[startup+780.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 77761 112 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134556928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 778.74
Current children cumulated vsize (Kb) 53952

[startup+790.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 78761 112 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 788.74
Current children cumulated vsize (Kb) 53952

[startup+800.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 79760 113 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134556987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 798.74
Current children cumulated vsize (Kb) 53952

[startup+810.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 80760 113 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 808.74
Current children cumulated vsize (Kb) 53952

[startup+820.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 81760 113 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 818.74
Current children cumulated vsize (Kb) 53952

[startup+830.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 82759 114 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 828.74
Current children cumulated vsize (Kb) 53952

[startup+840.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 83759 114 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 838.74
Current children cumulated vsize (Kb) 53952

[startup+850.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 84758 115 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 848.74
Current children cumulated vsize (Kb) 53952

[startup+860.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 85758 115 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 858.74
Current children cumulated vsize (Kb) 53952

[startup+870.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12692 0 0 0 86758 115 0 0 25 0 1 0 1844176087 53071872 12587 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12587 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 868.74
Current children cumulated vsize (Kb) 53952

[startup+880.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 87757 115 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 878.73
Current children cumulated vsize (Kb) 53952

[startup+890.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 88757 116 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 888.74
Current children cumulated vsize (Kb) 53952

[startup+900.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 89757 116 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 898.74
Current children cumulated vsize (Kb) 53952

[startup+910.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 90756 117 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223024 134557300 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 908.74
Current children cumulated vsize (Kb) 53952

[startup+920.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 91756 117 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 918.74
Current children cumulated vsize (Kb) 53952

[startup+930.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 92755 118 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 928.74
Current children cumulated vsize (Kb) 53952

[startup+940.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 93754 119 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 938.74
Current children cumulated vsize (Kb) 53952

[startup+950.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 94754 119 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223024 134556894 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 948.74
Current children cumulated vsize (Kb) 53952

[startup+960.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 95753 120 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 958.74
Current children cumulated vsize (Kb) 53952

[startup+970.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 96753 120 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 968.74
Current children cumulated vsize (Kb) 53952

[startup+980.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 97753 120 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 978.74
Current children cumulated vsize (Kb) 53952

[startup+990.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 98752 121 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 988.74
Current children cumulated vsize (Kb) 53952

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 99752 121 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 998.74
Current children cumulated vsize (Kb) 53952

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 100752 121 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1008.74
Current children cumulated vsize (Kb) 53952

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 101752 121 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1018.74
Current children cumulated vsize (Kb) 53952

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 102751 122 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1028.74
Current children cumulated vsize (Kb) 53952

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 103751 122 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1038.74
Current children cumulated vsize (Kb) 53952

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 104751 122 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1048.74
Current children cumulated vsize (Kb) 53952

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 105750 123 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1058.74
Current children cumulated vsize (Kb) 53952

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12698 0 0 0 106750 123 0 0 25 0 1 0 1844176087 53071872 12593 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12593 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1068.74
Current children cumulated vsize (Kb) 53952

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12698 0 0 0 107750 123 0 0 25 0 1 0 1844176087 53071872 12593 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12593 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1078.74
Current children cumulated vsize (Kb) 53952

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12699 0 0 0 108749 124 0 0 25 0 1 0 1844176087 53071872 12594 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12594 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1088.74
Current children cumulated vsize (Kb) 53952

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12702 0 0 0 109749 124 0 0 25 0 1 0 1844176087 53071872 12597 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12597 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1098.74
Current children cumulated vsize (Kb) 53952

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 110749 124 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1108.74
Current children cumulated vsize (Kb) 53952

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 111748 125 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1118.74
Current children cumulated vsize (Kb) 53952

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 112748 125 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1128.74
Current children cumulated vsize (Kb) 53952

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 113748 125 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1138.74
Current children cumulated vsize (Kb) 53952

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 114747 126 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1148.74
Current children cumulated vsize (Kb) 53952

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 115747 126 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1158.74
Current children cumulated vsize (Kb) 53952

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 116747 127 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1168.75
Current children cumulated vsize (Kb) 53952

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 117746 127 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1178.74
Current children cumulated vsize (Kb) 53952

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 118746 128 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0
[pid=16384] vsize: 51828
Current children cumulated CPU time (s) 1188.75
Current children cumulated vsize (Kb) 53952

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12718 0 0 0 119745 128 0 0 25 0 1 0 1844176087 53190656 12613 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12986 12613 145 145 0 12841 0
[pid=16384] vsize: 51944
Current children cumulated CPU time (s) 1198.74
Current children cumulated vsize (Kb) 54068

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12719 0 0 0 120745 128 0 0 25 0 1 0 1844176087 53190656 12614 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12986 12614 145 145 0 12841 0
[pid=16384] vsize: 51944
Current children cumulated CPU time (s) 1208.74
Current children cumulated vsize (Kb) 54068



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16384
Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16380/statm): 531 226 485 147 0 384 0
[pid=16380] vsize: 2124
Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12719 0 0 0 120745 128 0 0 25 0 1 0 1844176087 53190656 12614 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16384/statm): 12986 12614 145 145 0 12841 0
[pid=16384] vsize: 51944
Current children cumulated CPU time (s) 1208.74
Current children cumulated vsize (Kb) 54068

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1208.77
CPU user time (s): 1207.46
CPU system time (s): 1.3128
CPU usage (%): 99.8869
Max. virtual memory (cumulated for all children) (Kb): 54068

Verifier Data

ERROR: no interpretation found !