Some explanations

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

General information on the benchmark

Namesubmitted/een/normalized-l152lav.opb
MD5SUM7ef542195551d721d26b015e392d6d4b
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved YES
Number of terms in the objective function 1989
Biggest coefficient in the objective function 268
Number of bits for the biggest coefficient in the objective function 9
Sum of the numbers in the objective function 382524
Number of bits of the sum of numbers in the objective function 19
Biggest number in a constraint 1961
Number of bits of the biggest number in a constraint 11
Biggest sum of numbers in a constraint 382524
Number of bits of the biggest sum of numbers19
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark0.245961
Number of variables1989
Total number of constraints193
Number of constraints which are clauses95
Number of constraints which are cardinality constraints (but not clauses)97
Number of constraints which are nor clauses,nor cardinality constraints1
Minimum length of a constraint3
Maximum length of a constraint1989

Trace number 2260

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        927776 kB
Buffers:         31448 kB
Cached:          48128 kB
SwapCached:        732 kB
Active:          43040 kB
Inactive:        39088 kB
HighTotal:      131008 kB
HighFree:        81060 kB
LowTotal:       903652 kB
LowFree:        846716 kB
SwapTotal:     2097136 kB
SwapFree:      2095856 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            19048 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:44:02 (client local time) WITH STATUS 30 IN 1080.47 SECONDS
stats: 2629 0 1080.47 30

Solver Data

c Parsing PB file...
c Converting 193 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ==========================================================================================
c   -- Clauses(.)/Splits(s): ......
c ---[ 191]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:    7
c ---[ 187]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:   21
c ---[ 183]---> BDD-cost:   35
c ---[ 181]---> BDD-cost:   39
c ---[ 179]---> BDD-cost:   41
c ---[ 177]---> BDD-cost:   45
c ---[ 175]---> BDD-cost:   49
c ---[ 173]---> BDD-cost:   51
c ---[ 171]---> BDD-cost:   59
c ---[ 170]---> BDD-cost:   59
c ---[ 167]---> BDD-cost:   61
c ---[ 165]---> BDD-cost:   61
c ---[ 163]---> BDD-cost:   63
c ---[ 161]---> BDD-cost:   67
c ---[ 159]---> BDD-cost:   71
c ---[ 157]---> BDD-cost:   71
c ---[ 155]---> BDD-cost:   71
c ---[ 153]---> BDD-cost:   77
c ---[ 151]---> BDD-cost:   81
c ---[ 148]---> BDD-cost:   81
c ---[ 147]---> BDD-cost:   81
c ---[ 145]---> BDD-cost:   83
c ---[ 143]---> BDD-cost:   85
c ---[ 141]---> BDD-cost:   85
c ---[ 139]---> BDD-cost:   85
c ---[ 137]---> BDD-cost:   87
c ---[ 135]---> BDD-cost:   89
c ---[ 133]---> BDD-cost:   91
c ---[ 131]---> BDD-cost:   93
c ---[ 129]---> BDD-cost:   91
c ---[ 127]---> BDD-cost:   93
c ---[ 125]---> BDD-cost:   95
c ---[ 123]---> BDD-cost:   97
c ---[ 120]---> BDD-cost:  101
c ---[ 119]---> BDD-cost:  101
c ---[ 117]---> BDD-cost:  103
c ---[ 115]---> BDD-cost:  105
c ---[ 113]---> BDD-cost:  109
c ---[ 111]---> BDD-cost:  109
c ---[ 109]---> BDD-cost:  113
c ---[ 107]---> BDD-cost:  117
c ---[ 105]---> BDD-cost:  121
c ---[ 103]---> BDD-cost:  121
c ---[ 101]---> BDD-cost:  129
c ---[  99]---> BDD-cost:  133
c ---[  97]---> BDD-cost:  133
c ---[  95]---> BDD-cost:  133
c ---[  93]---> BDD-cost:  143
c ---[  91]---> BDD-cost:  145
c ---[  89]---> BDD-cost:  147
c ---[  87]---> BDD-cost:  147
c ---[  85]---> BDD-cost:  147
c ---[  83]---> BDD-cost:  149
c ---[  81]---> BDD-cost:  151
c ---[  79]---> BDD-cost:  151
c ---[  77]---> BDD-cost:  153
c ---[  75]---> BDD-cost:  155
c ---[  73]---> BDD-cost:  149
c ---[  71]---> BDD-cost:  171
c ---[  69]---> BDD-cost:  173
c ---[  67]---> BDD-cost:  171
c ---[  65]---> BDD-cost:  179
c ---[  63]---> BDD-cost:  181
c ---[  61]---> BDD-cost:  179
c ---[  59]---> BDD-cost:  183
c ---[  57]---> BDD-cost:  181
c ---[  55]---> BDD-cost:  189
c ---[  53]---> BDD-cost:  189
c ---[  52]---> BDD-cost:  189
c ---[  49]---> BDD-cost:  191
c ---[  47]---> BDD-cost:  201
c ---[  45]---> BDD-cost:  201
c ---[  43]---> BDD-cost:  203
c ---[  41]---> BDD-cost:  205
c ---[  39]---> BDD-cost:  209
c ---[  37]---> BDD-cost:  213
c ---[  35]---> BDD-cost:  213
c ---[  33]---> BDD-cost:  211
c ---[  31]---> BDD-cost:  221
c ---[  29]---> BDD-cost:  225
c ---[  27]---> BDD-cost:  231
c ---[  25]---> BDD-cost:  239
c ---[  23]---> BDD-cost:  231
c ---[  21]---> BDD-cost:  235
c ---[  19]---> BDD-cost:  235
c ---[  17]---> BDD-cost:  253
c ---[  15]---> BDD-cost:  255
c ---[  13]---> BDD-cost:  271
c ---[  11]---> BDD-cost:  301
c ---[   9]---> BDD-cost:  317
c ---[   7]---> BDD-cost:  323
c ---[   5]---> BDD-cost:  339
c ---[   3]---> BDD-cost:  433
c ---[   2]---> Adder-cost: 5478   maxlim: 25152   bits: 15/15
c ---[   0]---> Adder-cost: 3598   maxlim: 1960   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   97008   314147 |   32336       0        0     nan |  0.000 % |
c |       100 |   96925   313864 |   35569      88      873     9.9 |  0.509 % |
c |       250 |   96874   313679 |   39126     229     2112     9.2 |  0.541 % |
c |       475 |   96614   312745 |   43039     413     6085    14.7 |  0.737 % |
c |       812 |   96544   312487 |   47343     740    11385    15.4 |  0.777 % |
c |      1318 |   95598   309174 |   52077    1054    17038    16.2 |  1.429 % |
c |      2078 |   95451   308639 |   57285    1792    30764    17.2 |  1.527 % |
c ==============================================================================
c Found solution: 2828
c ---[   0]---> Adder-cost: 14768   maxlim: 379696   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2650 |  198564   676901 |   66188    2342    44415    19.0 |  1.527 % |
c |      2750 |  198452   676527 |   72806    2422    45131    18.6 |  1.111 % |
c |      2903 |  198364   676237 |   80087    2560    46999    18.4 |  1.149 % |
c |      3128 |  198266   675903 |   88096    2770    48832    17.6 |  1.192 % |
c |      3465 |  198097   675312 |   96905    3081    52260    17.0 |  1.263 % |
c |      3971 |  198013   675026 |  106596    3571    65032    18.2 |  1.299 % |
c |      4731 |  197959   674828 |  117256    4321    80083    18.5 |  1.319 % |
c |      5870 |  197709   673974 |  128981    5418   116091    21.4 |  1.423 % |
c |      7578 |  197525   673338 |  141879    7097   152104    21.4 |  1.502 % |
c |     10142 |  197296   672569 |  156067    9621   208071    21.6 |  1.601 % |
c |     13987 |  196436   669565 |  171674   13331   313151    23.5 |  1.944 % |
c |     19753 |  196247   668908 |  188842   19064   848432    44.5 |  2.016 % |
c |     28402 |  195994   668038 |  207726   27668  1764015    63.8 |  2.120 % |
c ==============================================================================
c Found solution: 2194
c ---[   0]---> Adder-cost: 0   maxlim: 380330   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30074 |  196013   668146 |   65337   29340  1915833    65.3 |  2.120 % |
c |     30174 |  196013   668146 |   71870   29440  1920627    65.2 |  2.137 % |
c |     30325 |  196013   668146 |   79057   29591  1927091    65.1 |  2.137 % |
c |     30551 |  196013   668146 |   86963   29817  1943337    65.2 |  2.137 % |
c |     30890 |  196004   668115 |   95659   30153  1969717    65.3 |  2.140 % |
c |     31396 |  196004   668115 |  105225   30659  2020608    65.9 |  2.140 % |
c |     32155 |  195967   667990 |  115748   31412  2084379    66.4 |  2.152 % |
c |     33294 |  195967   667990 |  127323   32551  2242568    68.9 |  2.152 % |
c |     35002 |  195886   667723 |  140055   34132  2515701    73.7 |  2.191 % |
c |     37564 |  195631   666846 |  154061   36650  2632782    71.8 |  2.300 % |
c |     41408 |  195592   666713 |  169467   40484  3041077    75.1 |  2.315 % |
c |     47174 |  195545   666552 |  186414   46240  3538233    76.5 |  2.338 % |
c |     55823 |  195376   665977 |  205055   54855  4718161    86.0 |  2.407 % |
c |     68797 |  195151   665222 |  225561   67754  5930725    87.5 |  2.501 % |
c |     88260 |  194943   664498 |  248117   87177  7549571    86.6 |  2.564 % |
c |    117452 |  194774   663923 |  272928  116338 11004517    94.6 |  2.618 % |
c ==============================================================================
c Found solution: 2082
c ---[   0]---> Adder-cost: 0   maxlim: 380442   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    124059 |  194624   663439 |   64874  122900 11672423    95.0 |  2.618 % |
c |    124159 |  194624   663439 |   71361   33278  1701621    51.1 |  2.673 % |
c |    124309 |  194624   663439 |   78497   33428  1704132    51.0 |  2.673 % |
c |    124535 |  194624   663439 |   86347   33654  1711323    50.9 |  2.673 % |
c |    124874 |  194624   663439 |   94982   33993  1723516    50.7 |  2.673 % |
c |    125380 |  194624   663439 |  104480   34499  1774855    51.4 |  2.673 % |
c |    126140 |  194608   663387 |  114928   35256  1853959    52.6 |  2.681 % |
c |    127281 |  194608   663387 |  126421   36397  2011665    55.3 |  2.681 % |
c |    128990 |  194593   663336 |  139063   38102  2213215    58.1 |  2.686 % |
c ==============================================================================
c Found solution: 2078
c ---[   0]---> Adder-cost: 0   maxlim: 380446   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    130316 |  194600   663391 |   64866   39428  2368148    60.1 |  2.686 % |
c |    130417 |  194600   663391 |   71352   39529  2369573    59.9 |  2.693 % |
c |    130567 |  194600   663391 |   78487   39679  2373954    59.8 |  2.693 % |
c |    130792 |  194600   663391 |   86336   39904  2378530    59.6 |  2.693 % |
c |    131129 |  194600   663391 |   94970   40241  2383781    59.2 |  2.693 % |
c |    131635 |  194600   663391 |  104467   40747  2403774    59.0 |  2.693 % |
c |    132396 |  194600   663391 |  114914   41508  2441878    58.8 |  2.693 % |
c |    133535 |  194600   663391 |  126405   42647  2728013    64.0 |  2.693 % |
c |    135248 |  194585   663338 |  139046   44356  2971207    67.0 |  2.696 % |
c |    137810 |  194585   663338 |  152950   46918  3393813    72.3 |  2.696 % |
c |    141654 |  194549   663212 |  168245   50754  3969744    78.2 |  2.703 % |
c |    147421 |  194438   662829 |  185070   56499  4569672    80.9 |  2.734 % |
c ==============================================================================
c Found solution: 2073
c ---[   0]---> Adder-cost: 0   maxlim: 380451   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    150709 |  194441   662852 |   64813   59787  5108139    85.4 |  2.734 % |
c |    150810 |  194441   662852 |   71294   59888  5109856    85.3 |  2.739 % |
c |    150963 |  194441   662852 |   78423   60041  5118422    85.2 |  2.739 % |
c |    151190 |  194441   662852 |   86266   60268  5134206    85.2 |  2.739 % |
c |    151527 |  194420   662779 |   94892   60599  5153084    85.0 |  2.744 % |
c |    152033 |  194420   662779 |  104381   61105  5186159    84.9 |  2.744 % |
c |    152792 |  194420   662779 |  114820   61864  5242649    84.7 |  2.744 % |
c ==============================================================================
c Found solution: 1449
c ---[   0]---> Adder-cost: 0   maxlim: 381075   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    153361 |  192837   657107 |   64279   57378  4622504    80.6 |  2.744 % |
c |    153461 |  192837   657107 |   70706   57478  4639376    80.7 |  3.457 % |
c |    153611 |  192837   657107 |   77777   57628  4666605    81.0 |  3.457 % |
c |    153840 |  192837   657107 |   85555   57857  4683429    80.9 |  3.457 % |
c |    154179 |  192837   657107 |   94110   58196  4710955    80.9 |  3.457 % |
c |    154686 |  192837   657107 |  103521   58703  4791232    81.6 |  3.457 % |
c |    155445 |  192811   657015 |  113874   59454  4924617    82.8 |  3.465 % |
c |    156585 |  192811   657015 |  125261   60594  5021617    82.9 |  3.465 % |
c |    158295 |  192811   657015 |  137787   62304  5198381    83.4 |  3.465 % |
c |    160857 |  192802   656984 |  151566   64865  5753119    88.7 |  3.467 % |
c |    164702 |  192793   656953 |  166723   68707  6204665    90.3 |  3.470 % |
c ==============================================================================
c Found solution: 1441
c ---[   0]---> Adder-cost: 0   maxlim: 381083   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    169856 |  192788   656945 |   64262   73859  6965183    94.3 |  3.470 % |
c |    169957 |  192788   656945 |   70688   31646  2001577    63.2 |  3.477 % |
c |    170108 |  192788   656945 |   77757   31797  2003628    63.0 |  3.477 % |
c |    170334 |  192788   656945 |   85532   32023  2010530    62.8 |  3.477 % |
c |    170671 |  192779   656916 |   94085   32359  2022619    62.5 |  3.482 % |
c |    171178 |  192779   656916 |  103494   32866  2051304    62.4 |  3.482 % |
c |    171937 |  192779   656916 |  113844   33625  2112371    62.8 |  3.482 % |
c |    173077 |  192758   656843 |  125228   34761  2259735    65.0 |  3.487 % |
c |    174786 |  192758   656843 |  137751   36470  2947139    80.8 |  3.487 % |
c ==============================================================================
c Found solution: 1115
c ---[   0]---> Adder-cost: 0   maxlim: 381409   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    177140 |  192730   656758 |   64243   38816  3240944    83.5 |  3.487 % |
c |    177241 |  192721   656727 |   70667   38913  3245024    83.4 |  3.510 % |
c |    177392 |  192706   656674 |   77734   39061  3252906    83.3 |  3.512 % |
c |    177618 |  192706   656674 |   85507   39287  3260332    83.0 |  3.512 % |
c |    177957 |  192685   656601 |   94058   39623  3275931    82.7 |  3.517 % |
c |    178463 |  192660   656510 |  103463   40124  3310700    82.5 |  3.525 % |
c |    179222 |  192660   656510 |  113810   40883  3375838    82.6 |  3.525 % |
c |    180361 |  192660   656510 |  125191   42022  3512409    83.6 |  3.525 % |
c |    182069 |  192660   656510 |  137710   43730  3691235    84.4 |  3.525 % |
c |    184631 |  192651   656479 |  151481   46288  3900068    84.3 |  3.527 % |
c ==============================================================================
c Found solution: 1111
c ---[   0]---> Adder-cost: 0   maxlim: 381413   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    185925 |  192654   656502 |   64218   47582  4399355    92.5 |  3.527 % |
c |    186025 |  192654   656502 |   70639   47682  4414385    92.6 |  3.532 % |
c |    186176 |  192654   656502 |   77703   47833  4429595    92.6 |  3.532 % |
c |    186401 |  192654   656502 |   85474   48058  4458567    92.8 |  3.532 % |
c |    186739 |  192618   656376 |   94021   48392  4483779    92.7 |  3.540 % |
c |    187246 |  192618   656376 |  103423   48899  4524585    92.5 |  3.540 % |
c |    188006 |  192618   656376 |  113766   49659  4653725    93.7 |  3.540 % |
c |    189146 |  192618   656376 |  125142   50799  4786639    94.2 |  3.540 % |
c |    190855 |  192603   656323 |  137656   52506  5046736    96.1 |  3.542 % |
c |    193417 |  192594   656292 |  151422   55066  5433251    98.7 |  3.545 % |
c ==============================================================================
c Found solution: 1046
c ---[   0]---> Adder-cost: 0   maxlim: 381478   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    194032 |  192603   656340 |   64201   55681  5559826    99.9 |  3.545 % |
c |    194132 |  192603   656340 |   70621   55781  5563829    99.7 |  3.557 % |
c |    194283 |  192603   656340 |   77683   55932  5573898    99.7 |  3.557 % |
c |    194509 |  192603   656340 |   85451   56158  5613679   100.0 |  3.557 % |
c |    194848 |  192603   656340 |   93996   56497  5642409    99.9 |  3.557 % |
c |    195354 |  192603   656340 |  103396   57003  5667609    99.4 |  3.557 % |
c |    196115 |  192603   656340 |  113735   57764  5746468    99.5 |  3.557 % |
c |    197254 |  192603   656340 |  125109   58903  5955335   101.1 |  3.557 % |
c |    198962 |  192596   656317 |  137620   60610  6090148   100.5 |  3.559 % |
c |    201524 |  192596   656317 |  151382   63172  6713393   106.3 |  3.559 % |
c ==============================================================================
c Found solution: 566
c ---[   0]---> Adder-cost: 0   maxlim: 381958   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    203979 |  189623   645896 |   63207   57904  5223834    90.2 |  3.559 % |
c |    204079 |  189623   645896 |   69527   58004  5229127    90.2 |  4.843 % |
c |    204230 |  189623   645896 |   76480   58155  5248198    90.2 |  4.843 % |
c |    204456 |  189623   645896 |   84128   58381  5265260    90.2 |  4.843 % |
c |    204793 |  189623   645896 |   92541   58718  5290968    90.1 |  4.843 % |
c |    205299 |  189616   645873 |  101795   59220  5347622    90.3 |  4.846 % |
c |    206060 |  189616   645873 |  111975   59981  5461182    91.0 |  4.846 % |
c ==============================================================================
c Found solution: 546
c ---[   0]---> Adder-cost: 0   maxlim: 381978   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    206227 |  189609   645858 |   63203   60144  5476802    91.1 |  4.846 % |
c |    206327 |  189609   645858 |   69523   60244  5483080    91.0 |  4.860 % |
c |    206478 |  189609   645858 |   76475   60395  5500220    91.1 |  4.860 % |
c |    206704 |  189600   645827 |   84123   60619  5533389    91.3 |  4.862 % |
c |    207042 |  189600   645827 |   92535   60957  5586416    91.6 |  4.862 % |
c |    207548 |  189600   645827 |  101789   61463  5791937    94.2 |  4.862 % |
c ==============================================================================
c Found solution: 167
c ---[   0]---> Sorter-cost:32661     Base: 3 3 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207650 |  101622   262329 |   33874   14444   884050    61.2 |  4.862 % |
c |    207750 |  101607   262278 |   37261   14538   886482    61.0 | 41.529 % |
c |    207900 |  101607   262278 |   40987   14688   913153    62.2 | 41.529 % |
c ==============================================================================
c Found solution: 69
c ---[   0]---> BDD-cost: 1070
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207929 |   69469   179291 |   23156   11463   720814    62.9 | 41.529 % |
c ==============================================================================
c Found solution: 32
c ---[   0]---> BDD-cost:    0
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207933 |   29650    72478 |    9883    2525   113113    44.8 | 41.529 % |
c ==============================================================================
c Found solution: 25
c ---[   0]---> BDD-cost:    0
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207944 |   22667    53948 |    7555     989    17172    17.4 | 41.529 % |
c ==============================================================================
c Found solution: 24
c ---[   0]---> BDD-cost:    0
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207945 |   22108    52315 |    7369     785    13865    17.7 | 41.529 % |
c ==============================================================================
c Found solution: 13
c ---[   0]---> BDD-cost:    0
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207947 |   18495    41799 |    6165      41      306     7.5 | 41.529 % |
c ==============================================================================
c Found solution: 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207948 |   18221    40939 |    6073       1        3     3.0 | 41.529 % |
c ==============================================================================
c Found solution: 0
c Optimal solution: 0
s OPTIMUM FOUND
v -x0 -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 -x765 -x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 -x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 -x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 -x1336 -x1337 -x1338 -x1339 -x1340 -x1341 -x1342 -x1343 -x1344 -x1345 -x1346 -x1347 -x1348 -x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 -x1408 -x1409 -x1410 -x1411 -x1412 -x1413 -x1414 -x1415 -x1416 -x1417 -x1418 -x1419 -x1420 -x1421 -x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 -x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 -x1470 -x1471 -x1472 -x1473 -x1474 -x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 -x1498 -x1499 -x1500 -x1501 -x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 -x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 -x1518 -x1519 -x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 -x1527 -x1528 -x1529 -x1530 -x1531 -x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 -x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 -x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 -x1567 -x1568 -x1569 -x1570 -x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 -x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 -x1622 -x1623 -x1624 -x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 -x1633 -x1634 -x1635 -x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 -x1654 -x1655 -x1656 -x1657 -x1658 -x1659 -x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 -x1676 -x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 -x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 -x1709 -x1710 -x1711 -x1712 -x1713 -x1714 -x1715 -x1716 -x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 -x1743 -x1744 -x1745 -x1746 -x1747 -x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 -x1765 -x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 -x1787 -x1788 -x1789 -x1790 -x1791 -x1792 -x1793 -x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 -x1801 -x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 -x1818 -x1819 -x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 -x1827 -x1828 -x1829 -x1830 -x1831 -x1832 -x1833 -x1834 -x1835 -x1836 -x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 -x1848 -x1849 -x1850 -x1851 -x1852 -x1853 -x1854 -x1855 -x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 -x1876 -x1877 -x1878 -x1879 -x1880 -x1881 -x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 -x1919 -x1920 -x1921 -x1922 -x1923 -x1924 -x1925 -x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 -x1943 -x1944 -x1945 -x1946 -x1947 -x1948 -x1949 -x1950 -x1951 -x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 -x1962 -x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 -x1970 -x1971 -x1972 -x1973 -x1974 -x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981 -x1982 -x1983 -x1984 -x1985 -x1986 -x1987 -x1988
c _______________________________________________________________________________
c 
c restarts              : 136
c conflicts             : 207948         (193 /sec)
c decisions             : 1927046        (1786 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1078.71 s
c _______________________________________________________________________________

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/16330/stat): 16330 (minisat+_script) R 16329 16330 9854 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785170516 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/16330/statm): 174 3 169 147 0 27 0
[pid=16330] 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=16331
New process pid=16332
New process pid=16333
execve syscall for /bin/sed executable
One traced child (pid=16332) 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=16333) exited with status: 0
One traced child (pid=16331) exited with status: 0
New process pid=16334
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-l152lav.opb

[startup+10.0035 s]
Raw data (loadavg): 0.88 0.97 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 4757 0 0 0 962 18 0 0 25 0 1 0 1785170521 17752064 3727 4294967295 134512640 135094434 3221224448 3221222176 134677310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 4334 3727 145 145 0 4189 0
[pid=16334] vsize: 17336
Current children cumulated CPU time (s) 9.82
Current children cumulated vsize (Kb) 19460

[startup+20.0043 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 11976 0 0 0 1915 45 0 0 25 0 1 0 1785170521 48316416 9950 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 11796 9950 145 145 0 11651 0
[pid=16334] vsize: 47184
Current children cumulated CPU time (s) 19.62
Current children cumulated vsize (Kb) 49308

[startup+30.0061 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 12071 0 0 0 2913 46 0 0 25 0 1 0 1785170521 48709632 10045 4294967295 134512640 135094434 3221224448 3221223108 134553519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 11892 10045 145 145 0 11747 0
[pid=16334] vsize: 47568
Current children cumulated CPU time (s) 29.61
Current children cumulated vsize (Kb) 49692

[startup+40.0068 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 12149 0 0 0 3910 47 0 0 25 0 1 0 1785170521 49053696 10123 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 11976 10123 145 145 0 11831 0
[pid=16334] vsize: 47904
Current children cumulated CPU time (s) 39.59
Current children cumulated vsize (Kb) 50028

[startup+50.0076 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 12230 0 0 0 4909 48 0 0 25 0 1 0 1785170521 49348608 10204 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 12048 10204 145 145 0 11903 0
[pid=16334] vsize: 48192
Current children cumulated CPU time (s) 49.59
Current children cumulated vsize (Kb) 50316

[startup+60.0084 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 12432 0 0 0 5906 49 0 0 25 0 1 0 1785170521 50167808 10406 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 12248 10406 145 145 0 12103 0
[pid=16334] vsize: 48992
Current children cumulated CPU time (s) 59.57
Current children cumulated vsize (Kb) 51116

[startup+70.0092 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 12829 0 0 0 6900 51 0 0 25 0 1 0 1785170521 51838976 10803 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 12656 10803 145 145 0 12511 0
[pid=16334] vsize: 50624
Current children cumulated CPU time (s) 69.53
Current children cumulated vsize (Kb) 52748

[startup+80.01 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 13125 0 0 0 7896 52 0 0 25 0 1 0 1785170521 53039104 11099 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 12949 11099 145 145 0 12804 0
[pid=16334] vsize: 51796
Current children cumulated CPU time (s) 79.5
Current children cumulated vsize (Kb) 53920

[startup+90.0108 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 13534 0 0 0 8887 57 0 0 25 0 1 0 1785170521 54714368 11508 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 13358 11508 145 145 0 13213 0
[pid=16334] vsize: 53432
Current children cumulated CPU time (s) 89.46
Current children cumulated vsize (Kb) 55556

[startup+100.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 13842 0 0 0 9881 59 0 0 25 0 1 0 1785170521 55963648 11816 4294967295 134512640 135094434 3221224448 3221223040 134556776 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 13663 11816 145 145 0 13518 0
[pid=16334] vsize: 54652
Current children cumulated CPU time (s) 99.42
Current children cumulated vsize (Kb) 56776

[startup+110.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 14427 0 0 0 10873 63 0 0 25 0 1 0 1785170521 57417728 12148 4294967295 134512640 135094434 3221224448 3221221792 134519312 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 14018 12148 145 145 0 13873 0
[pid=16334] vsize: 56072
Current children cumulated CPU time (s) 109.38
Current children cumulated vsize (Kb) 58196

[startup+120.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 14728 0 0 0 11870 65 0 0 25 0 1 0 1785170521 58400768 12449 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 14258 12449 145 145 0 14113 0
[pid=16334] vsize: 57032
Current children cumulated CPU time (s) 119.37
Current children cumulated vsize (Kb) 59156

[startup+130.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 15100 0 0 0 12863 67 0 0 25 0 1 0 1785170521 60047360 12821 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 14660 12821 145 145 0 14515 0
[pid=16334] vsize: 58640
Current children cumulated CPU time (s) 129.32
Current children cumulated vsize (Kb) 60764

[startup+140.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 15196 0 0 0 13861 68 0 0 25 0 1 0 1785170521 60432384 12917 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 14754 12917 145 145 0 14609 0
[pid=16334] vsize: 59016
Current children cumulated CPU time (s) 139.31
Current children cumulated vsize (Kb) 61140

[startup+150.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 15378 0 0 0 14857 70 0 0 25 0 1 0 1785170521 61169664 13099 4294967295 134512640 135094434 3221224448 3221223040 134556949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 14934 13099 145 145 0 14789 0
[pid=16334] vsize: 59736
Current children cumulated CPU time (s) 149.29
Current children cumulated vsize (Kb) 61860

[startup+160.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 15724 0 0 0 15852 72 0 0 25 0 1 0 1785170521 62574592 13445 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 15277 13445 145 145 0 15132 0
[pid=16334] vsize: 61108
Current children cumulated CPU time (s) 159.26
Current children cumulated vsize (Kb) 63232

[startup+170.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 16005 0 0 0 16846 75 0 0 25 0 1 0 1785170521 63717376 13726 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 15556 13726 145 145 0 15411 0
[pid=16334] vsize: 62224
Current children cumulated CPU time (s) 169.23
Current children cumulated vsize (Kb) 64348

[startup+180.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 16305 0 0 0 17840 77 0 0 25 0 1 0 1785170521 64933888 14026 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 15853 14026 145 145 0 15708 0
[pid=16334] vsize: 63412
Current children cumulated CPU time (s) 179.19
Current children cumulated vsize (Kb) 65536

[startup+190.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 16603 0 0 0 18835 79 0 0 25 0 1 0 1785170521 66150400 14324 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 16150 14324 145 145 0 16005 0
[pid=16334] vsize: 64600
Current children cumulated CPU time (s) 189.16
Current children cumulated vsize (Kb) 66724

[startup+200.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 16895 0 0 0 19828 83 0 0 25 0 1 0 1785170521 67338240 14616 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 16440 14616 145 145 0 16295 0
[pid=16334] vsize: 65760
Current children cumulated CPU time (s) 199.13
Current children cumulated vsize (Kb) 67884

[startup+210.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 17253 0 0 0 20822 86 0 0 25 0 1 0 1785170521 68792320 14974 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 16795 14974 145 145 0 16650 0
[pid=16334] vsize: 67180
Current children cumulated CPU time (s) 209.1
Current children cumulated vsize (Kb) 69304

[startup+220.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 17556 0 0 0 21815 90 0 0 25 0 1 0 1785170521 70025216 15277 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 17096 15277 145 145 0 16951 0
[pid=16334] vsize: 68384
Current children cumulated CPU time (s) 219.07
Current children cumulated vsize (Kb) 70508

[startup+230.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 17813 0 0 0 22811 91 0 0 25 0 1 0 1785170521 71069696 15534 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 17351 15534 145 145 0 17206 0
[pid=16334] vsize: 69404
Current children cumulated CPU time (s) 229.04
Current children cumulated vsize (Kb) 71528

[startup+240.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 18069 0 0 0 23805 94 0 0 25 0 1 0 1785170521 72105984 15790 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 17604 15790 145 145 0 17459 0
[pid=16334] vsize: 70416
Current children cumulated CPU time (s) 239.01
Current children cumulated vsize (Kb) 72540

[startup+250.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 18381 0 0 0 24800 96 0 0 25 0 1 0 1785170521 73375744 16102 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 17914 16102 145 145 0 17769 0
[pid=16334] vsize: 71656
Current children cumulated CPU time (s) 248.98
Current children cumulated vsize (Kb) 73780

[startup+260.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 18500 0 0 0 25797 97 0 0 25 0 1 0 1785170521 73859072 16221 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 18032 16221 145 145 0 17887 0
[pid=16334] vsize: 72128
Current children cumulated CPU time (s) 258.96
Current children cumulated vsize (Kb) 74252

[startup+270.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 18525 0 0 0 26797 98 0 0 25 0 1 0 1785170521 73953280 16246 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 18055 16246 145 145 0 17910 0
[pid=16334] vsize: 72220
Current children cumulated CPU time (s) 268.97
Current children cumulated vsize (Kb) 74344

[startup+280.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 18689 0 0 0 27794 99 0 0 25 0 1 0 1785170521 74887168 16410 4294967295 134512640 135094434 3221224448 3221223104 134558033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 18283 16410 145 145 0 18138 0
[pid=16334] vsize: 73132
Current children cumulated CPU time (s) 278.95
Current children cumulated vsize (Kb) 75256

[startup+290.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 18880 0 0 0 28790 101 0 0 25 0 1 0 1785170521 75657216 16601 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 18471 16601 145 145 0 18326 0
[pid=16334] vsize: 73884
Current children cumulated CPU time (s) 288.93
Current children cumulated vsize (Kb) 76008

[startup+300.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 19039 0 0 0 29787 102 0 0 25 0 1 0 1785170521 76300288 16760 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 18628 16760 145 145 0 18483 0
[pid=16334] vsize: 74512
Current children cumulated CPU time (s) 298.91
Current children cumulated vsize (Kb) 76636

[startup+310.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 19257 0 0 0 30784 104 0 0 25 0 1 0 1785170521 77189120 16978 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 18845 16978 145 145 0 18700 0
[pid=16334] vsize: 75380
Current children cumulated CPU time (s) 308.9
Current children cumulated vsize (Kb) 77504

[startup+320.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 19411 0 0 0 31780 106 0 0 25 0 1 0 1785170521 77811712 17132 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 18997 17132 145 145 0 18852 0
[pid=16334] vsize: 75988
Current children cumulated CPU time (s) 318.88
Current children cumulated vsize (Kb) 78112

[startup+330.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 19736 0 0 0 32774 109 0 0 25 0 1 0 1785170521 79134720 17457 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 19320 17457 145 145 0 19175 0
[pid=16334] vsize: 77280
Current children cumulated CPU time (s) 328.85
Current children cumulated vsize (Kb) 79404

[startup+340.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 19944 0 0 0 33770 110 0 0 25 0 1 0 1785170521 79978496 17665 4294967295 134512640 135094434 3221224448 3221223060 134563064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 19526 17665 145 145 0 19381 0
[pid=16334] vsize: 78104
Current children cumulated CPU time (s) 338.82
Current children cumulated vsize (Kb) 80228

[startup+350.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 20061 0 0 0 34767 111 0 0 25 0 1 0 1785170521 80449536 17782 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 19641 17782 145 145 0 19496 0
[pid=16334] vsize: 78564
Current children cumulated CPU time (s) 348.8
Current children cumulated vsize (Kb) 80688

[startup+360.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 20142 0 0 0 35765 112 0 0 25 0 1 0 1785170521 80773120 17863 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 19720 17863 145 145 0 19575 0
[pid=16334] vsize: 78880
Current children cumulated CPU time (s) 358.79
Current children cumulated vsize (Kb) 81004

[startup+370.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 20349 0 0 0 36762 114 0 0 25 0 1 0 1785170521 81616896 18070 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 19926 18070 145 145 0 19781 0
[pid=16334] vsize: 79704
Current children cumulated CPU time (s) 368.78
Current children cumulated vsize (Kb) 81828

[startup+380.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 20576 0 0 0 37759 115 0 0 25 0 1 0 1785170521 82550784 18297 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 20154 18297 145 145 0 20009 0
[pid=16334] vsize: 80616
Current children cumulated CPU time (s) 378.76
Current children cumulated vsize (Kb) 82740

[startup+390.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 20826 0 0 0 38755 116 0 0 25 0 1 0 1785170521 83562496 18547 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 20401 18547 145 145 0 20256 0
[pid=16334] vsize: 81604
Current children cumulated CPU time (s) 388.73
Current children cumulated vsize (Kb) 83728

[startup+400.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 21194 0 0 0 39750 119 0 0 25 0 1 0 1785170521 85053440 18915 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 20765 18915 145 145 0 20620 0
[pid=16334] vsize: 83060
Current children cumulated CPU time (s) 398.71
Current children cumulated vsize (Kb) 85184

[startup+410.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 21478 0 0 0 40746 120 0 0 25 0 1 0 1785170521 86208512 19199 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 21047 19199 145 145 0 20902 0
[pid=16334] vsize: 84188
Current children cumulated CPU time (s) 408.68
Current children cumulated vsize (Kb) 86312

[startup+420.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 21585 0 0 0 41744 121 0 0 25 0 1 0 1785170521 86638592 19306 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 21152 19306 145 145 0 21007 0
[pid=16334] vsize: 84608
Current children cumulated CPU time (s) 418.67
Current children cumulated vsize (Kb) 86732

[startup+430.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 21787 0 0 0 42740 123 0 0 25 0 1 0 1785170521 87457792 19508 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 21352 19508 145 145 0 21207 0
[pid=16334] vsize: 85408
Current children cumulated CPU time (s) 428.65
Current children cumulated vsize (Kb) 87532

[startup+440.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 22005 0 0 0 43737 124 0 0 25 0 1 0 1785170521 88342528 19726 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 21568 19726 145 145 0 21423 0
[pid=16334] vsize: 86272
Current children cumulated CPU time (s) 438.63
Current children cumulated vsize (Kb) 88396

[startup+450.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 22397 0 0 0 44732 127 0 0 25 0 1 0 1785170521 89939968 20118 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 21958 20118 145 145 0 21813 0
[pid=16334] vsize: 87832
Current children cumulated CPU time (s) 448.61
Current children cumulated vsize (Kb) 89956

[startup+460.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 22509 0 0 0 45730 128 0 0 25 0 1 0 1785170521 90390528 20230 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 22068 20230 145 145 0 21923 0
[pid=16334] vsize: 88272
Current children cumulated CPU time (s) 458.6
Current children cumulated vsize (Kb) 90396

[startup+470.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 22729 0 0 0 46726 129 0 0 25 0 1 0 1785170521 91287552 20450 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 22287 20450 145 145 0 22142 0
[pid=16334] vsize: 89148
Current children cumulated CPU time (s) 468.57
Current children cumulated vsize (Kb) 91272

[startup+480.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 23057 0 0 0 47720 131 0 0 25 0 1 0 1785170521 92614656 20778 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 22611 20778 145 145 0 22466 0
[pid=16334] vsize: 90444
Current children cumulated CPU time (s) 478.53
Current children cumulated vsize (Kb) 92568

[startup+490.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 23295 0 0 0 48715 133 0 0 25 0 1 0 1785170521 93581312 21016 4294967295 134512640 135094434 3221224448 3221223072 134562110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 22847 21016 145 145 0 22702 0
[pid=16334] vsize: 91388
Current children cumulated CPU time (s) 488.5
Current children cumulated vsize (Kb) 93512

[startup+500.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 23496 0 0 0 49711 135 0 0 25 0 1 0 1785170521 94400512 21217 4294967295 134512640 135094434 3221224448 3221223088 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 23047 21217 145 145 0 22902 0
[pid=16334] vsize: 92188
Current children cumulated CPU time (s) 498.48
Current children cumulated vsize (Kb) 94312

[startup+510.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 23717 0 0 0 50707 137 0 0 25 0 1 0 1785170521 95297536 21438 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 23266 21438 145 145 0 23121 0
[pid=16334] vsize: 93064
Current children cumulated CPU time (s) 508.46
Current children cumulated vsize (Kb) 95188

[startup+520.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 24084 0 0 0 51701 139 0 0 25 0 1 0 1785170521 96792576 21805 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 23631 21805 145 145 0 23486 0
[pid=16334] vsize: 94524
Current children cumulated CPU time (s) 518.42
Current children cumulated vsize (Kb) 96648

[startup+530.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 24318 0 0 0 52698 141 0 0 25 0 1 0 1785170521 97746944 22039 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 23864 22039 145 145 0 23719 0
[pid=16334] vsize: 95456
Current children cumulated CPU time (s) 528.41
Current children cumulated vsize (Kb) 97580

[startup+540.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 24473 0 0 0 53695 143 0 0 25 0 1 0 1785170521 98369536 22194 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 24016 22194 145 145 0 23871 0
[pid=16334] vsize: 96064
Current children cumulated CPU time (s) 538.4
Current children cumulated vsize (Kb) 98188

[startup+550.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 24694 0 0 0 54692 144 0 0 25 0 1 0 1785170521 99266560 22415 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 24235 22415 145 145 0 24090 0
[pid=16334] vsize: 96940
Current children cumulated CPU time (s) 548.38
Current children cumulated vsize (Kb) 99064

[startup+560.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 24908 0 0 0 55688 146 0 0 25 0 1 0 1785170521 100134912 22629 4294967295 134512640 135094434 3221224448 3221223040 134556999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 24447 22629 145 145 0 24302 0
[pid=16334] vsize: 97788
Current children cumulated CPU time (s) 558.36
Current children cumulated vsize (Kb) 99912

[startup+570.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25694 0 0 0 56683 148 0 0 25 0 1 0 1785170521 101150720 22869 4294967295 134512640 135094434 3221224448 3221220864 134519670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 24695 22869 145 145 0 24550 0
[pid=16334] vsize: 98780
Current children cumulated CPU time (s) 568.33
Current children cumulated vsize (Kb) 100904

[startup+580.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25705 0 0 0 57682 149 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 578.33
Current children cumulated vsize (Kb) 100764

[startup+590.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25705 0 0 0 58682 149 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 588.33
Current children cumulated vsize (Kb) 100764

[startup+600.065 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25705 0 0 0 59682 149 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 598.33
Current children cumulated vsize (Kb) 100764

[startup+610.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25995 0 0 0 60681 150 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 608.33
Current children cumulated vsize (Kb) 100764

[startup+620.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25995 0 0 0 61680 151 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 618.33
Current children cumulated vsize (Kb) 100764

[startup+630.069 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25995 0 0 0 62680 151 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223040 134557042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 628.33
Current children cumulated vsize (Kb) 100764

[startup+640.071 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25995 0 0 0 63680 151 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 638.33
Current children cumulated vsize (Kb) 100764

[startup+650.072 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25995 0 0 0 64680 151 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 648.33
Current children cumulated vsize (Kb) 100764

[startup+660.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25995 0 0 0 65680 152 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 658.34
Current children cumulated vsize (Kb) 100764

[startup+670.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25995 0 0 0 66680 152 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 668.34
Current children cumulated vsize (Kb) 100764

[startup+680.075 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25995 0 0 0 67681 152 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 678.35
Current children cumulated vsize (Kb) 100764

[startup+690.076 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25995 0 0 0 68679 153 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 688.34
Current children cumulated vsize (Kb) 100764

[startup+700.077 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 25995 0 0 0 69679 153 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 698.34
Current children cumulated vsize (Kb) 100764

[startup+710.079 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26285 0 0 0 70679 154 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 708.35
Current children cumulated vsize (Kb) 100764

[startup+720.079 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26285 0 0 0 71679 154 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 718.35
Current children cumulated vsize (Kb) 100764

[startup+730.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26410 0 0 0 72678 155 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 728.35
Current children cumulated vsize (Kb) 100764

[startup+740.081 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26410 0 0 0 73678 155 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223136 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 738.35
Current children cumulated vsize (Kb) 100764

[startup+750.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26410 0 0 0 74678 155 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 748.35
Current children cumulated vsize (Kb) 100764

[startup+760.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26410 0 0 0 75678 155 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223040 134557213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 758.35
Current children cumulated vsize (Kb) 100764

[startup+770.083 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26410 0 0 0 76678 156 0 0 25 0 1 0 1785170521 101007360 22844 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22844 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 768.36
Current children cumulated vsize (Kb) 100764

[startup+780.085 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26411 0 0 0 77679 156 0 0 25 0 1 0 1785170521 101007360 22845 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22845 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 778.37
Current children cumulated vsize (Kb) 100764

[startup+790.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26411 0 0 0 78679 156 0 0 25 0 1 0 1785170521 101007360 22845 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22845 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 788.37
Current children cumulated vsize (Kb) 100764

[startup+800.087 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26411 0 0 0 79679 156 0 0 25 0 1 0 1785170521 101007360 22845 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22845 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 798.37
Current children cumulated vsize (Kb) 100764

[startup+810.087 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26411 0 0 0 80679 156 0 0 25 0 1 0 1785170521 101007360 22845 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22845 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 808.37
Current children cumulated vsize (Kb) 100764

[startup+820.088 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26411 0 0 0 81679 156 0 0 25 0 1 0 1785170521 101007360 22845 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22845 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 818.37
Current children cumulated vsize (Kb) 100764

[startup+830.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26537 0 0 0 82679 157 0 0 25 0 1 0 1785170521 101007360 22846 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22846 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 828.38
Current children cumulated vsize (Kb) 100764

[startup+840.091 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26537 0 0 0 83679 157 0 0 25 0 1 0 1785170521 101007360 22846 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22846 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 838.38
Current children cumulated vsize (Kb) 100764

[startup+850.092 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26537 0 0 0 84679 157 0 0 25 0 1 0 1785170521 101007360 22846 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22846 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 848.38
Current children cumulated vsize (Kb) 100764

[startup+860.092 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26538 0 0 0 85679 157 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223040 134557393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 858.38
Current children cumulated vsize (Kb) 100764

[startup+870.093 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26538 0 0 0 86679 157 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 868.38
Current children cumulated vsize (Kb) 100764

[startup+880.094 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26538 0 0 0 87680 157 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 878.39
Current children cumulated vsize (Kb) 100764

[startup+890.095 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26621 0 0 0 88680 157 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 888.39
Current children cumulated vsize (Kb) 100764

[startup+900.096 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26621 0 0 0 89680 158 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 898.4
Current children cumulated vsize (Kb) 100764

[startup+910.096 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26621 0 0 0 90680 158 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 908.4
Current children cumulated vsize (Kb) 100764

[startup+920.097 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26621 0 0 0 91680 158 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 918.4
Current children cumulated vsize (Kb) 100764

[startup+930.098 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26621 0 0 0 92680 158 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223040 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 928.4
Current children cumulated vsize (Kb) 100764

[startup+940.099 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26704 0 0 0 93680 158 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 938.4
Current children cumulated vsize (Kb) 100764

[startup+950.099 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26704 0 0 0 94680 158 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223040 134557020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 948.4
Current children cumulated vsize (Kb) 100764

[startup+960.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26704 0 0 0 95680 158 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223040 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 958.4
Current children cumulated vsize (Kb) 100764

[startup+970.101 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26704 0 0 0 96680 159 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 968.41
Current children cumulated vsize (Kb) 100764

[startup+980.102 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26704 0 0 0 97681 159 0 0 25 0 1 0 1785170521 101007360 22847 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22847 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 978.42
Current children cumulated vsize (Kb) 100764

[startup+990.103 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26953 0 0 0 98680 159 0 0 25 0 1 0 1785170521 101007360 22848 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22848 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 988.41
Current children cumulated vsize (Kb) 100764

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26953 0 0 0 99680 159 0 0 25 0 1 0 1785170521 101007360 22848 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22848 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 998.41
Current children cumulated vsize (Kb) 100764

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26953 0 0 0 100680 159 0 0 25 0 1 0 1785170521 101007360 22848 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22848 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 1008.41
Current children cumulated vsize (Kb) 100764

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26953 0 0 0 101681 159 0 0 25 0 1 0 1785170521 101007360 22848 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22848 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 1018.42
Current children cumulated vsize (Kb) 100764

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26953 0 0 0 102680 160 0 0 25 0 1 0 1785170521 101007360 22848 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22848 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 1028.42
Current children cumulated vsize (Kb) 100764

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 26953 0 0 0 103681 160 0 0 25 0 1 0 1785170521 101007360 22848 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22848 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 1038.43
Current children cumulated vsize (Kb) 100764

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 27037 0 0 0 104681 160 0 0 25 0 1 0 1785170521 101007360 22849 4294967295 134512640 135094434 3221224448 3221223236 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22849 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 1048.43
Current children cumulated vsize (Kb) 100764

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 27037 0 0 0 105681 160 0 0 25 0 1 0 1785170521 101007360 22849 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22849 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 1058.43
Current children cumulated vsize (Kb) 100764

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 27120 0 0 0 106681 160 0 0 25 0 1 0 1785170521 101007360 22849 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 24660 22849 145 145 0 24515 0
[pid=16334] vsize: 98640
Current children cumulated CPU time (s) 1068.43
Current children cumulated vsize (Kb) 100764

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 16334
Raw data (/proc/16330/stat): 16330 (minisat+_script) S 16329 16330 9854 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1785170516 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16330/statm): 531 226 485 147 0 384 0
[pid=16330] vsize: 2124
Raw data (/proc/16334/stat): 16334 (minisat+_64-bit) R 16330 16330 9854 0 -1 0 27623 0 0 0 107679 162 0 0 25 0 1 0 1785170521 105242624 23352 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16334/statm): 25694 23352 145 145 0 25549 0
[pid=16334] vsize: 102776
Current children cumulated CPU time (s) 1078.43
Current children cumulated vsize (Kb) 104900
One traced child (pid=16334) exited with status: 30
One traced child (pid=16330) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 1082.14
CPU time (s): 1080.47
CPU user time (s): 1078.77
CPU system time (s): 1.69674
CPU usage (%): 99.8461
Max. virtual memory (cumulated for all children) (Kb): 104900

Verifier Data

Verifier:	OK	0