Some explanations

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

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-ran13x13.opb
MD5SUM52c9f5bb9e744e5b269906d75a40a640
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 8366094
Optimality of the best value was proved NO
Number of terms in the objective function 5239
Biggest coefficient in the objective function 5368709120
Number of bits for the biggest coefficient in the objective function 33
Sum of the numbers in the objective function 968548072570
Number of bits of the sum of numbers in the objective function 40
Biggest number in a constraint 5368709120
Number of bits of the biggest number in a constraint 33
Biggest sum of numbers in a constraint 968548072570
Number of bits of the biggest sum of numbers40
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1216.34
Number of variables5239
Total number of constraints195
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints195
Minimum length of a constraint31
Maximum length of a constraint390

Trace number 5876

Launcher Data

LAUNCH ON wulflinc10 THE 2005-09-20 01:25:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3052 boxname=wulflinc10 idbench=708 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  52c9f5bb9e744e5b269906d75a40a640  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-ran13x13.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-ran13x13.opb
IDLAUNCH: 3052
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        797652 kB
Buffers:         38284 kB
Cached:         171268 kB
SwapCached:        228 kB
Active:          73228 kB
Inactive:       139336 kB
HighTotal:      131008 kB
HighFree:        16744 kB
LowTotal:       903652 kB
LowFree:        780908 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6272 kB
Slab:            18912 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 01:45:16 (client local time) WITH STATUS 10 IN 1208.16 SECONDS
stats: 3052 7 1208.16 10

Solver Data

c Parsing PB file...
c Converting 221 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 219]---> Adder-cost: 322   maxlim: 135155   bits: 18/18
c ---[ 217]---> Adder-cost: 330   maxlim: 209907   bits: 18/18
c ---[ 215]---> Adder-cost: 330   maxlim: 215027   bits: 18/18
c ---[ 213]---> Adder-cost: 322   maxlim: 137203   bits: 18/18
c ---[ 211]---> Adder-cost: 330   maxlim: 210931   bits: 18/18
c ---[ 209]---> Adder-cost: 322   maxlim: 138227   bits: 18/18
c ---[ 207]---> Adder-cost: 330   maxlim: 202739   bits: 18/18
c ---[ 205]---> Adder-cost: 322   maxlim: 136179   bits: 18/18
c ---[ 203]---> Adder-cost: 306   maxlim: 84979   bits: 17/17
c ---[ 201]---> Adder-cost: 330   maxlim: 209907   bits: 18/18
c ---[ 199]---> Adder-cost: 306   maxlim: 84979   bits: 17/17
c ---[ 197]---> Adder-cost: 330   maxlim: 212979   bits: 18/18
c ---[ 195]---> Adder-cost: 322   maxlim: 137203   bits: 18/18
c ---[ 193]---> Adder-cost: 344   maxlim: 274419   bits: 19/19
c ---[ 191]---> Adder-cost: 344   maxlim: 266227   bits: 19/19
c ---[ 189]---> Adder-cost: 288   maxlim: 51187   bits: 16/16
c ---[ 187]---> Adder-cost: 330   maxlim: 187379   bits: 18/18
c ---[ 185]---> Adder-cost: 312   maxlim: 101363   bits: 17/17
c ---[ 183]---> Adder-cost: 330   maxlim: 183283   bits: 18/18
c ---[ 181]---> Adder-cost: 312   maxlim: 100339   bits: 17/17
c ---[ 179]---> Adder-cost: 288   maxlim: 50163   bits: 16/16
c ---[ 177]---> Adder-cost: 344   maxlim: 250867   bits: 19/18
c ---[ 175]---> Adder-cost: 312   maxlim: 102387   bits: 17/17
c ---[ 173]---> Adder-cost: 264   maxlim: 25587   bits: 15/15
c ---[ 171]---> Adder-cost: 344   maxlim: 260083   bits: 19/18
c ---[ 169]---> Adder-cost: 344   maxlim: 262131   bits: 19/18
c ---[ 168]---> BDD-cost:   17
c ---[ 167]---> BDD-cost:   17
c ---[ 166]---> BDD-cost:   13
c ---[ 165]---> BDD-cost:   16
c ---[ 164]---> BDD-cost:   13
c ---[ 163]---> BDD-cost:   16
c ---[ 162]---> BDD-cost:   16
c ---[ 161]---> BDD-cost:   19
c ---[ 160]---> BDD-cost:   19
c ---[ 159]---> BDD-cost:   18
c ---[ 158]---> BDD-cost:   15
c ---[ 157]---> BDD-cost:   14
c ---[ 156]---> BDD-cost:   19
c ---[ 155]---> BDD-cost:   18
c ---[ 154]---> BDD-cost:   14
c ---[ 153]---> BDD-cost:   12
c ---[ 152]---> BDD-cost:   19
c ---[ 151]---> BDD-cost:   19
c ---[ 150]---> BDD-cost:   13
c ---[ 149]---> BDD-cost:   18
c ---[ 148]---> BDD-cost:   16
c ---[ 147]---> BDD-cost:   16
c ---[ 146]---> BDD-cost:   16
c ---[ 145]---> BDD-cost:   16
c ---[ 144]---> BDD-cost:   16
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   14
c ---[ 141]---> BDD-cost:   16
c ---[ 140]---> BDD-cost:   14
c ---[ 139]---> BDD-cost:   12
c ---[ 138]---> BDD-cost:   16
c ---[ 137]---> BDD-cost:   16
c ---[ 136]---> BDD-cost:   13
c ---[ 135]---> BDD-cost:   18
c ---[ 134]---> BDD-cost:   16
c ---[ 133]---> BDD-cost:   18
c ---[ 132]---> BDD-cost:   16
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:   18
c ---[ 129]---> BDD-cost:   15
c ---[ 128]---> BDD-cost:   14
c ---[ 127]---> BDD-cost:   16
c ---[ 126]---> BDD-cost:   14
c ---[ 125]---> BDD-cost:   12
c ---[ 124]---> BDD-cost:   16
c ---[ 123]---> BDD-cost:   16
c ---[ 122]---> BDD-cost:   20
c ---[ 121]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   18
c ---[ 119]---> BDD-cost:   16
c ---[ 118]---> BDD-cost:   16
c ---[ 117]---> BDD-cost:   16
c ---[ 116]---> BDD-cost:   16
c ---[ 115]---> BDD-cost:   15
c ---[ 114]---> BDD-cost:   14
c ---[ 113]---> BDD-cost:   16
c ---[ 112]---> BDD-cost:   14
c ---[ 111]---> BDD-cost:   18
c ---[ 110]---> BDD-cost:   12
c ---[ 109]---> BDD-cost:   16
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   18
c ---[ 105]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   18
c ---[ 103]---> BDD-cost:   18
c ---[ 102]---> BDD-cost:   18
c ---[ 101]---> BDD-cost:   15
c ---[ 100]---> BDD-cost:   15
c ---[  99]---> BDD-cost:   14
c ---[  98]---> BDD-cost:   18
c ---[  97]---> BDD-cost:   14
c ---[  96]---> BDD-cost:   12
c ---[  95]---> BDD-cost:   18
c ---[  94]---> BDD-cost:   18
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:   18
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:   14
c ---[  89]---> BDD-cost:   20
c ---[  88]---> BDD-cost:   14
c ---[  87]---> BDD-cost:   18
c ---[  86]---> BDD-cost:   12
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   20
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   18
c ---[  81]---> BDD-cost:   16
c ---[  80]---> BDD-cost:   18
c ---[  79]---> BDD-cost:   18
c ---[  78]---> BDD-cost:   18
c ---[  77]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   15
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   18
c ---[  73]---> BDD-cost:   14
c ---[  72]---> BDD-cost:   12
c ---[  71]---> BDD-cost:   18
c ---[  70]---> BDD-cost:   18
c ---[  69]---> BDD-cost:   13
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   16
c ---[  66]---> BDD-cost:   18
c ---[  65]---> BDD-cost:   14
c ---[  64]---> BDD-cost:   18
c ---[  63]---> BDD-cost:   18
c ---[  62]---> BDD-cost:   15
c ---[  61]---> BDD-cost:   14
c ---[  60]---> BDD-cost:   18
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   12
c ---[  57]---> BDD-cost:   18
c ---[  56]---> BDD-cost:   18
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   17
c ---[  53]---> BDD-cost:   18
c ---[  52]---> BDD-cost:   16
c ---[  51]---> BDD-cost:   18
c ---[  50]---> BDD-cost:   18
c ---[  49]---> BDD-cost:   18
c ---[  48]---> BDD-cost:   15
c ---[  47]---> BDD-cost:   14
c ---[  46]---> BDD-cost:   18
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   18
c ---[  41]---> BDD-cost:   18
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   16
c ---[  37]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   16
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   12
c ---[  31]---> BDD-cost:   16
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:   12
c ---[  28]---> BDD-cost:   16
c ---[  27]---> BDD-cost:   16
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   16
c ---[  23]---> BDD-cost:   18
c ---[  22]---> BDD-cost:   20
c ---[  21]---> BDD-cost:   17
c ---[  20]---> BDD-cost:   18
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   20
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   18
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   16
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   16
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:   12
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   59169   205907 |   19723       0        0     nan |  0.000 % |
c |       100 |   58966   205226 |   21695      81      248     3.1 | 26.670 % |
c |       250 |   58929   205105 |   23864     224      679     3.0 | 26.710 % |
c |       475 |   58776   204580 |   26251     435     1416     3.3 | 26.899 % |
c |       812 |   58736   204450 |   28876     767     2502     3.3 | 26.946 % |
c |      1318 |   58704   204346 |   31764    1269     4112     3.2 | 26.986 % |
c |      2077 |   58650   204170 |   34940    2021     6941     3.4 | 27.033 % |
c |      3217 |   58607   204027 |   38434    3156    12260     3.9 | 27.081 % |
c |      4925 |   58558   203860 |   42278    4858    29543     6.1 | 27.134 % |
c |      7487 |   58532   203772 |   46505    7418    57519     7.8 | 27.168 % |
c |     11332 |   58499   203663 |   51156   11258    97364     8.6 | 27.202 % |
c |     17098 |   58499   203663 |   56272   17024   235102    13.8 | 27.202 % |
c |     25748 |   58358   203180 |   61899   25653   369038    14.4 | 27.363 % |
c |     38723 |   58332   203092 |   68089   38625  1061555    27.5 | 27.397 % |
c |     58184 |   58178   202572 |   74898   58063  1362471    23.5 | 27.579 % |
c |     87376 |   57836   201424 |   82387   29884   394312    13.2 | 28.003 % |
c ==============================================================================
c Found solution: 33155221
c ---[   0]---> Adder-cost: 8227   maxlim: 12393445   bits: 25/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    117520 |  115043   405890 |   38347   59987  1494905    24.9 | 28.003 % |
c |    117620 |  115036   405867 |   42181   22990   201489     8.8 | 18.278 % |
c |    117771 |  115029   405844 |   46399   23139   202349     8.7 | 18.283 % |
c |    117996 |  114987   405700 |   51039   23356   203616     8.7 | 18.309 % |
c |    118334 |  114978   405671 |   56143   23693   205716     8.7 | 18.317 % |
c |    118840 |  114978   405671 |   61758   24199   208869     8.6 | 18.317 % |
c |    119599 |  114978   405671 |   67934   24958   214627     8.6 | 18.317 % |
c |    120738 |  114978   405671 |   74727   26097   224536     8.6 | 18.317 % |
c |    122446 |  114971   405648 |   82200   27803   239431     8.6 | 18.322 % |
c |    125009 |  114897   405398 |   90420   30346   259028     8.5 | 18.374 % |
c |    128853 |  114840   405203 |   99462   34183   293418     8.6 | 18.413 % |
c |    134619 |  114777   404990 |  109408   39934   358967     9.0 | 18.460 % |
c |    143269 |  114777   404990 |  120349   48584   497222    10.2 | 18.460 % |
c ==============================================================================
c Found solution: 28619477
c ---[   0]---> Adder-cost: 2   maxlim: 16929189   bits: 26/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    149142 |  114806   405203 |   38268   54457   604992    11.1 | 18.460 % |
c |    149242 |  114806   405203 |   42094   24036   246610    10.3 | 18.489 % |
c |    149392 |  114806   405203 |   46304   24186   247331    10.2 | 18.489 % |
c |    149617 |  114797   405174 |   50934   24409   248759    10.2 | 18.497 % |
c |    149956 |  114797   405174 |   56028   24748   251161    10.1 | 18.497 % |
c |    150462 |  114797   405174 |   61630   25254   254327    10.1 | 18.497 % |
c |    151221 |  114773   405092 |   67794   26010   258715     9.9 | 18.515 % |
c |    152361 |  114773   405092 |   74573   27150   266147     9.8 | 18.515 % |
c |    154069 |  114773   405092 |   82030   28858   278656     9.7 | 18.515 % |
c |    156631 |  114773   405092 |   90233   31420   298787     9.5 | 18.515 % |
c |    160475 |  114758   405043 |   99257   35261   332503     9.4 | 18.528 % |
c |    166242 |  114749   405012 |  109183   41025   398407     9.7 | 18.532 % |
c |    174891 |  114740   404981 |  120101   49671   816775    16.4 | 18.536 % |
c |    187865 |  114680   404767 |  132111   62637  1096475    17.5 | 18.580 % |
c |    207326 |  114647   404656 |  145322   82094  4770429    58.1 | 18.606 % |
c |    236519 |  114614   404545 |  159854  111280 10147150    91.2 | 18.632 % |
c ==============================================================================
c Found solution: 23702357
c ---[   0]---> Adder-cost: 0   maxlim: 21846309   bits: 26/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    240672 |  114552   404460 |   38184  115418 10273582    89.0 | 18.632 % |
c |    240772 |  114552   404460 |   42002   22162  1907867    86.1 | 18.730 % |
c |    240922 |  114552   404460 |   46202   22312  1908900    85.6 | 18.730 % |
c |    241149 |  114552   404460 |   50822   22539  1911906    84.8 | 18.730 % |
c |    241487 |  114552   404460 |   55905   22877  1913606    83.6 | 18.730 % |
c |    241993 |  114552   404460 |   61495   23383  1916932    82.0 | 18.730 % |
c |    242754 |  114552   404460 |   67645   24144  1928308    79.9 | 18.730 % |
c |    243893 |  114552   404460 |   74409   25283  1936448    76.6 | 18.730 % |
c |    245601 |  114545   404437 |   81850   26989  1949899    72.2 | 18.735 % |
c |    248163 |  114545   404437 |   90035   29551  1978783    67.0 | 18.735 % |
c |    252008 |  114545   404437 |   99039   33396  2096875    62.8 | 18.735 % |
c |    257774 |  114545   404437 |  108943   39162  2241626    57.2 | 18.735 % |
c |    266423 |  114545   404437 |  119837   47811  2825493    59.1 | 18.735 % |
c |    279397 |  114545   404437 |  131821   60785  3650200    60.1 | 18.735 % |
c |    298858 |  114513   404333 |  145003   80240  4048618    50.5 | 18.761 % |
c |    328051 |  114513   404333 |  159504  109433  5806871    53.1 | 18.761 % |
c ==============================================================================
c Found solution: 23459838
c ---[   0]---> Adder-cost: 0   maxlim: 22088828   bits: 26/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    340331 |  114528   404551 |   38176  121711  6139137    50.4 | 18.761 % |
c |    340431 |  114528   404551 |   41993   25512   404097    15.8 | 18.803 % |
c |    340581 |  114528   404551 |   46192   25662   404810    15.8 | 18.803 % |
c |    340806 |  114528   404551 |   50812   25887   406459    15.7 | 18.803 % |
c |    341143 |  114528   404551 |   55893   26224   408841    15.6 | 18.803 % |
c |    341650 |  114528   404551 |   61482   26731   412457    15.4 | 18.803 % |
c |    342409 |  114519   404522 |   67631   27489   419514    15.3 | 18.812 % |
c |    343548 |  114519   404522 |   74394   28628   429035    15.0 | 18.812 % |
c |    345256 |  114519   404522 |   81833   30336   445719    14.7 | 18.812 % |
c |    347818 |  114519   404522 |   90017   32898   469615    14.3 | 18.812 % |
c |    351662 |  114519   404522 |   99018   36742   503239    13.7 | 18.812 % |
c |    357428 |  114519   404522 |  108920   42508   632366    14.9 | 18.812 % |
c ==============================================================================
c Found solution: 18381569
c ---[   0]---> Adder-cost: 0   maxlim: 27167097   bits: 26/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    365398 |  114540   404740 |   38180   50478   774054    15.3 | 18.812 % |
c |    365498 |  114540   404740 |   41998   22479   288028    12.8 | 18.853 % |
c |    365648 |  114540   404740 |   46197   22629   288914    12.8 | 18.853 % |
c |    365873 |  114540   404740 |   50817   22854   290254    12.7 | 18.853 % |
c |    366210 |  114540   404740 |   55899   23191   292257    12.6 | 18.853 % |
c |    366716 |  114540   404740 |   61489   23697   294992    12.4 | 18.853 % |
c |    367475 |  114540   404740 |   67638   24456   299578    12.2 | 18.853 % |
c |    368615 |  114540   404740 |   74402   25596   309766    12.1 | 18.853 % |
c |    370324 |  114531   404709 |   81842   27303   324841    11.9 | 18.857 % |
c |    372886 |  114531   404709 |   90026   29865   367423    12.3 | 18.857 % |
c |    376730 |  114531   404709 |   99029   33709   398490    11.8 | 18.857 % |
c |    382497 |  114531   404709 |  108931   39476   704678    17.9 | 18.857 % |
c |    391147 |  114531   404709 |  119825   48126   971762    20.2 | 18.857 % |
c |    404122 |  114531   404709 |  131807   61101  1320630    21.6 | 18.857 % |
c |    423583 |  114525   404689 |  144988   80561  1876626    23.3 | 18.861 % |
c |    452777 |  114525   404689 |  159487  109755  4572914    41.7 | 18.861 % |
c |    496566 |  114516   404658 |  175436  153542  8905116    58.0 | 18.866 % |
c |    562251 |  114516   404658 |  192979   44738  2231418    49.9 | 18.866 % |
c |    660777 |  114516   404658 |  212277  143264 10062228    70.2 | 18.866 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_10 -X0_bit_9 -X0_bit_8 -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X0_bit13 -X0_bit14 -X0_bit15 -X0_bit16 -X0_bit17 -X0_bit18 -X0_bit19 -X1_bit_10 -X1_bit_9 -X1_bit_8 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X1_bit13 -X1_bit14 -X1_bit15 -X1_bit16 -X1_bit17 -X1_bit18 -X1_bit19 -X2_bit_10 -X2_bit_9 -X2_bit_8 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X2_bit13 -X2_bit14 -X2_bit15 -X2_bit16 -X2_bit17 -X2_bit18 -X2_bit19 -X3_bit_10 -X3_bit_9 -X3_bit_8 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X3_bit13 -X3_bit14 -X3_bit15 -X3_bit16 -X3_bit17 -X3_bit18 -X3_bit19 -X4_bit_10 -X4_bit_9 X4_bit_8 -X4_bit_7 X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 X4_bit_2 X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X4_bit13 -X4_bit14 -X4_bit15 -X4_bit16 -X4_bit17 -X4_bit18 -X4_bit19 -X5_bit_10 -X5_bit_9 -X5_bit_8 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X5_bit13 -X5_bit14 -X5_bit15 -X5_bit16 -X5_bit17 -X5_bit18 -X5_bit19 -X6_bit_10 -X6_bit_9 X6_bit_8 X6_bit_7 X6_bit_6 X6_bit_5 -X6_bit_4 -X6_bit_3 X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X6_bit13 -X6_bit14 -X6_bit15 -X6_bit16 -X6_bit17 -X6_bit18 -X6_bit19 -X7_bit_10 -X7_bit_9 -X7_bit_8 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 X7_bit_3 X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X7_bit13 -X7_bit14 -X7_bit15 -X7_bit16 -X7_bit17 -X7_bit18 -X7_bit19 -X8_bit_10 -X8_bit_9 -X8_bit_8 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X8_bit13 -X8_bit14 -X8_bit15 -X8_bit16 -X8_bit17 -X8_bit18 -X8_bit19 -X9_bit_10 -X9_bit_9 -X9_bit_8 -X9_bit_7 -X9_bit_6 X9_bit_5 -X9_bit_4 -X9_bit_3 X9_bit_2 -X9_bit_1 -X9_bit0 X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X9_bit13 -X9_bit14 -X9_bit15 -X9_bit16 -X9_bit17 -X9_bit18 -X9_bit19 -X10_bit_10 -X10_bit_9 -X10_bit_8 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X10_bit13 -X10_bit14 -X10_bit15 -X10_bit16 -X10_bit17 -X10_bit18 -X10_bit19 -X11_bit_10 -X11_bit_9 -X11_bit_8 -X11_bit_7 X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 X11_bit_2 -X11_bit_1 X11_bit0 -X11_bit1 X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X11_bit13 -X11_bit14 -X11_bit15 -X11_bit16 -X11_bit17 -X11_bit18 -X11_bit19 -X12_bit_10 -X12_bit_9 -X12_bit_8 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 X12_bit0 -X12_bit1 X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X12_bit13 -X12_bit14 -X12_bit15 -X12_bit16 -X12_bit17 -X12_bit18 -X12_bit19 -X13_bit_10 -X13_bit_9 -X13_bit_8 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X13_bit13 -X13_bit14 -X13_bit15 -X13_bit16 -X13_bit17 -X13_bit18 -X13_bit19 -X14_bit_10 X14_bit_9 -X14_bit_8 -X14_bit_7 X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X14_bit13 -X14_bit14 -X14_bit15 -X14_bit16 -X14_bit17 -X14_bit18 -X14_bit19 -X15_bit_10 -X15_bit_9 -X15_bit_8 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X15_bit13 -X15_bit14 -X15_bit15 -X15_bit16 -X15_bit17 -X15_bit18 -X15_bit19 -X16_bit_10 -X16_bit_9 -X16_bit_8 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X16_bit13 -X16_bit14 -X16_bit15 -X16_bit16 -X16_bit17 -X16_bit18 -X16_bit19 X17_bit_10 -X17_bit_9 X17_bit_8 -X17_bit_7 X17_bit_6 -X17_bit_5 X17_bit_4 X17_bit_3 X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X17_bit13 -X17_bit14 -X17_bit15 -X17_bit16 -X17_bit17 -X17_bit18 -X17_bit19 X18_bit_10 X18_bit_9 -X18_bit_8 -X18_bit_7 -X18_bit_6 X18_bit_5 X18_bit_4 X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X18_bit13 -X18_bit14 -X18_bit15 -X18_bit16 -X18_bit17 -X18_bit18 -X18_bit19 -X19_bit_10 -X19_bit_9 -X19_bit_8 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X19_bit13 -X19_bit14 -X19_bit15 -X19_bit16 -X19_bit17 -X19_bit18 -X19_bit19 -X20_bit_10 -X20_bit_9 -X20_bit_8 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X20_bit13 -X20_bit14 -X20_bit15 -X20_bit16 -X20_bit17 -X20_bit18 -X20_bit19 -X21_bit_10 -X21_bit_9 -X21_bit_8 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X21_bit13 -X21_bit14 -X21_bit15 -X21_bit16 -X21_bit17 -X21_bit18 -X21_bit19 -X22_bit_10 -X22_bit_9 -X22_bit_8 -X22_bit_7 -X22_bit_6 X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 X22_bit1 -X22_bit2 -X22_bit3 X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X22_bit13 -X22_bit14 -X22_bit15 -X22_bit16 -X22_bit17 -X22_bit18 -X22_bit19 -X23_bit_10 -X23_bit_9 -X23_bit_8 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X23_bit13 -X23_bit14 -X23_bit15 -X23_bit16 -X23_bit17 -X23_bit18 -X23_bit19 -X24_bit_10 X24_bit_9 X24_bit_8 -X24_bit_7 X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 X24_bit_2 -X24_bit_1 X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X24_bit13 -X24_bit14 -X24_bit15 -X24_bit16 -X24_bit17 -X24_bit18 -X24_bit19 -X25_bit_10 -X25_bit_9 -X25_bit_8 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X25_bit13 -X25_bit14 -X25_bit15 -X25_bit16 -X25_bit17 -X25_bit18 -X25_bit19 -X26_bit_10 -X26_bit_9 -X26_bit_8 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X26_bit13 -X26_bit14 -X26_bit15 -X26_bit16 -X26_bit17 -X26_bit18 -X26_bit19 -X27_bit_10 -X27_bit_9 -X27_bit_8 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X27_bit13 -X27_bit14 -X27_bit15 -X27_bit16 -X27_bit17 -X27_bit18 -X27_bit19 -X28_bit_10 -X28_bit_9 -X28_bit_8 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X28_bit13 -X28_bit14 -X28_bit15 -X28_bit16 -X28_bit17 -X28_bit18 -X28_bit19 -X29_bit_10 -X29_bit_9 -X29_bit_8 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X29_bit13 -X29_bit14 -X29_bit15 -X29_bit16 -X29_bit17 -X29_bit18 -X29_bit19 -X30_bit_10 -X30_bit_9 X30_bit_8 -X30_bit_7 -X30_bit_6 -X30_bit_5 X30_bit_4 -X30_bit_3 -X30_bit_2 X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X30_bit13 -X30_bit14 -X30_bit15 -X30_bit16 -X30_bit17 -X30_bit18 -X30_bit19 -X31_bit_10 -X31_bit_9 X31_bit_8 -X31_bit_7 -X31_bit_6 -X31_bit_5 X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X31_bit13 -X31_bit14 -X31_bit15 -X31_bit16 -X31_bit17 -X31_bit18 -X31_bit19 -X32_bit_10 -X32_bit_9 -X32_bit_8 X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 X32_bit_2 -X32_bit_1 -X32_bit0 X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X32_bit13 -X32_bit14 -X32_bit15 -X32_bit16 -X32_bit17 -X32_bit18 -X32_bit19 -X33_bit_10 -X33_bit_9 -X33_bit_8 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X33_bit13 -X33_bit14 -X33_bit15 -X33_bit16 -X33_bit17 -X33_bit18 -X33_bit19 -X34_bit_10 -X34_bit_9 -X34_bit_8 -X34_bit_7 -X34_bit_6 -X34_bit_5 -X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X34_bit13 -X34_bit14 -X34_bit15 -X34_bit16 -X34_bit17 -X34_bit18 -X34_bit19 -X35_bit_10 -X35_bit_9 -X35_bit_8 X35_bit_7 X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X35_bit13 -X35_bit14 -X35_bit15 -X35_bit16 -X35_bit17 -X35_bit18 -X35_bit19 -X36_bit_10 -X36_bit_9 -X36_bit_8 X36_bit_7 X36_bit_6 -X36_bit_5 X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X36_bit13 -X36_bit14 -X36_bit15 -X36_bit16 -X36_bit17 -X36_bit18 -X36_bit19 -X37_bit_10 -X37_bit_9 -X37_bit_8 -X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X37_bit13 -X37_bit14 -X37_bit15 -X37_bit16 -X37_bit17 -X37_bit18 -X37_bit19 -X38_bit_10 -X38_bit_9 -X38_bit_8 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X38_bit13 -X38_bit14 -X38_bit15 -X38_bit16 -X38_bit17 -X38_bit18 -X38_bit19 X39_bit_10 X39_bit_9 -X39_bit_8 -X39_bit_7 -X39_bit_6 X39_bit_5 X39_bit_4 -X39_bit_3 X39_bit_2 -X39_bit_1 X39_bit0 X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X39_bit13 -X39_bit14 -X39_bit15 -X39_bit16 -X39_bit17 -X39_bit18 -X39_bit19 -X40_bit_10 -X40_bit_9 -X40_bit_8 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X40_bit13 -X40_bit14 -X40_bit15 -X40_bit16 -X40_bit17 -X40_bit18 -X40_bit19 -X41_bit_10 -X41_bit_9 -X41_bit_8 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X41_bit13 -X41_bit14 -X41_bit15 -X41_bit16 -X41_bit17 -X41_bit18 -X41_bit19 -X42_bit_10 -X42_bit_9 -X42_bit_8 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X42_bit13 -X42_bit14 -X42_bit15 -X42_bit16 -X42_bit17 -X42_bit18 -X42_bit19 -X43_bit_10 -X43_bit_9 -X43_bit_8 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X43_bit13 -X43_bit14 -X43_bit15 -X43_bit16 -X43_bit17 -X43_bit18 -X43_bit19 X44_bit_10 X44_bit_9 -X44_bit_8 -X44_bit_7 X44_bit_6 -X44_bit_5 X44_bit_4 -X44_bit_3 X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X44_bit13 -X44_bit14 -X44_bit15 -X44_bit16 -X44_bit17 -X44_bit18 -X44_bit19 -X45_bit_10 -X45_bit_9 -X45_bit_8 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X45_bit13 -X45_bit14 -X45_bit15 -X45_bit16 -X45_bit17 -X45_bit18 -X45_bit19 X46_bit_10 -X46_bit_9 -X46_bit_8 X46_bit_7 -X46_bit_6 -X46_bit_5 X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X46_bit13 -X46_bit14 -X46_bit15 -X46_bit16 -X46_bit17 -X46_bit18 -X46_bit19 -X47_bit_10 -X47_bit_9 -X47_bit_8 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X47_bit13 -X47_bit14 -X47_bit15 -X47_bit16 -X47_bit17 -X47_bit18 -X47_bit19 X48_bit_10 -X48_bit_9 -X48_bit_8 -X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X48_bit13 -X48_bit14 -X48_bit15 -X48_bit16 -X48_bit17 -X48_bit18 -X48_bit19 -X49_bit_10 -X49_bit_9 -X49_bit_8 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X49_bit13 -X49_bit14 -X49_bit15 -X49_bit16 -X49_bit17 -X49_bit18 -X49_bit19 -X50_bit_10 -X50_bit_9 -X50_bit_8 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X50_bit13 -X50_bit14 -X50_bit15 -X50_bit16 -X50_bit17 -X50_bit18 -X50_bit19 -X51_bit_10 -X51_bit_9 -X51_bit_8 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X51_bit13 -X51_bit14 -X51_bit15 -X51_bit16 -X51_bit17 -X51_bit18 -X51_bit19 X52_bit_10 -X52_bit_9 X52_bit_8 -X52_bit_7 -X52_bit_6 X52_bit_5 X52_bit_4 -X52_bit_3 X52_bit_2 X52_bit_1 X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X52_bit13 -X52_bit14 -X52_bit15 -X52_bit16 -X52_bit17 -X52_bit18 -X52_bit19 -X53_bit_10 -X53_bit_9 -X53_bit_8 -X53_bit_7 -X53_bit_6 X53_bit_5 -X53_bit_4 -X53_bit_3 X53_bit_2 X53_bit_1 X53_bit0 -X53_bit1 -X53_bit2 X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X53_bit13 -X53_bit14 -X53_bit15 -X53_bit16 -X53_bit17 -X53_bit18 -X53_bit19 -X54_bit_10 -X54_bit_9 -X54_bit_8 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X54_bit13 -X54_bit14 -X54_bit15 -X54_bit16 -X54_bit17 -X54_bit18 -X54_bit19 -X55_bit_10 -X55_bit_9 -X55_bit_8 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X55_bit13 -X55_bit14 -X55_bit15 -X55_bit16 -X55_bit17 -X55_bit18 -X55_bit19 X56_bit_10 X56_bit_9 -X56_bit_8 X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X56_bit13 -X56_bit14 -X56_bit15 -X56_bit16 -X56_bit17 -X56_bit18 -X56_bit19 -X57_bit_10 X57_bit_9 X57_bit_8 X57_bit_7 X57_bit_6 -X57_bit_5 X57_bit_4 -X57_bit_3 X57_bit_2 X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X57_bit13 -X57_bit14 -X57_bit15 -X57_bit16 -X57_bit17 -X57_bit18 -X57_bit19 -X58_bit_10 -X58_bit_9 -X58_bit_8 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X58_bit13 -X58_bit14 -X58_bit15 -X58_bit16 -X58_bit17 -X58_bit18 -X58_bit19 X59_bit_10 -X59_bit_9 -X59_bit_8 -X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X59_bit13 -X59_bit14 -X59_bit15 -X59_bit16 -X59_bit17 -X59_bit18 -X59_bit19 -X60_bit_10 -X60_bit_9 -X60_bit_8 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X60_bit13 -X60_bit14 -X60_bit15 -X60_bit16 -X60_bit17 -X60_bit18 -X60_bit19 -X61_bit_10 -X61_bit_9 -X61_bit_8 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X61_bit13 -X61_bit14 -X61_bit15 -X61_bit16 -X61_bit17 -X61_bit18 -X61_bit19 -X62_bit_10 -X62_bit_9 -X62_bit_8 -X62_bit_7 -X62_bit_6 -X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X62_bit13 -X62_bit14 -X62_bit15 -X62_bit16 -X62_bit17 -X62_bit18 -X62_bit19 X63_bit_10 -X63_bit_9 -X63_bit_8 -X63_bit_7 X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X63_bit13 -X63_bit14 -X63_bit15 -X63_bit16 -X63_bit17 -X63_bit18 -X63_bit19 -X64_bit_10 -X64_bit_9 -X64_bit_8 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X64_bit13 -X64_bit14 -X64_bit15 -X64_bit16 -X64_bit17 -X64_bit18 -X64_bit19 -X65_bit_10 -X65_bit_9 -X65_bit_8 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X65_bit13 -X65_bit14 -X65_bit15 -X65_bit16 -X65_bit17 -X65_bit18 -X65_bit19 -X66_bit_10 -X66_bit_9 -X66_bit_8 -X66_bit_7 -X66_bit_6 -X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X66_bit13 -X66_bit14 -X66_bit15 -X66_bit16 -X66_bit17 -X66_bit18 -X66_bit19 -X67_bit_10 -X67_bit_9 -X67_bit_8 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X67_bit13 -X67_bit14 -X67_bit15 -X67_bit16 -X67_bit17 -X67_bit18 -X67_bit19 X68_bit_10 -X68_bit_9 -X68_bit_8 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 X68_bit_3 -X68_bit_2 -X68_bit_1 X68_bit0 -X68_bit1 X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X68_bit13 -X68_bit14 -X68_bit15 -X68_bit16 -X68_bit17 -X68_bit18 -X68_bit19 X69_bit_10 X69_bit_9 X69_bit_8 X69_bit_7 X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X69_bit13 -X69_bit14 -X69_bit15 -X69_bit16 -X69_bit17 -X69_bit18 -X69_bit19 -X70_bit_10 -X70_bit_9 -X70_bit_8 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X70_bit13 -X70_bit14 -X70_bit15 -X70_bit16 -X70_bit17 -X70_bit18 -X70_bit19 -X71_bit_10 -X71_bit_9 -X71_bit_8 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X71_bit13 -X71_bit14 -X71_bit15 -X71_bit16 -X71_bit17 -X71_bit18 -X71_bit19 -X72_bit_10 -X72_bit_9 -X72_bit_8 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X72_bit13 -X72_bit14 -X72_bit15 -X72_bit16 -X72_bit17 -X72_bit18 -X72_bit19 -X73_bit_10 -X73_bit_9 -X73_bit_8 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X73_bit13 -X73_bit14 -X73_bit15 -X73_bit16 -X73_bit17 -X73_bit18 -X73_bit19 X74_bit_10 -X74_bit_9 -X74_bit_8 X74_bit_7 -X74_bit_6 -X74_bit_5 X74_bit_4 -X74_bit_3 X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X74_bit13 -X74_bit14 -X74_bit15 -X74_bit16 -X74_bit17 -X74_bit18 -X74_bit19 -X75_bit_10 -X75_bit_9 -X75_bit_8 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X75_bit13 -X75_bit14 -X75_bit15 -X75_bit16 -X75_bit17 -X75_bit18 -X75_bit19 X76_bit_10 X76_bit_9 X76_bit_8 -X76_bit_7 X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X76_bit13 -X76_bit14 -X76_bit15 -X76_bit16 -X76_bit17 -X76_bit18 -X76_bit19 -X77_bit_10 -X77_bit_9 -X77_bit_8 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X77_bit13 -X77_bit14 -X77_bit15 -X77_bit16 -X77_bit17 -X77_bit18 -X77_bit19 X78_bit_10 X78_bit_9 X78_bit_8 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 X78_bit_2 -X78_bit_1 X78_bit0 X78_bit1 X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X78_bit13 -X78_bit14 -X78_bit15 -X78_bit16 -X78_bit17 -X78_bit18 -X78_bit19 X79_bit_10 X79_bit_9 -X79_bit_8 -X79_bit_7 X79_bit_6 X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 X79_bit0 X79_bit1 -X79_bit2 X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X79_bit13 -X79_bit14 -X79_bit15 -X79_bit16 -X79_bit17 -X79_bit18 -X79_bit19 -X80_bit_10 -X80_bit_9 -X80_bit_8 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X80_bit13 -X80_bit14 -X80_bit15 -X80_bit16 -X80_bit17 -X80_bit18 -X80_bit19 -X81_bit_10 -X81_bit_9 -X81_bit_8 X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X81_bit13 -X81_bit14 -X81_bit15 -X81_bit16 -X81_bit17 -X81_bit18 -X81_bit19 -X82_bit_10 -X82_bit_9 -X82_bit_8 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X82_bit13 -X82_bit14 -X82_bit15 -X82_bit16 -X82_bit17 -X82_bit18 -X82_bit19 X83_bit_10 X83_bit_9 X83_bit_8 -X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X83_bit13 -X83_bit14 -X83_bit15 -X83_bit16 -X83_bit17 -X83_bit18 -X83_bit19 -X84_bit_10 -X84_bit_9 -X84_bit_8 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X84_bit13 -X84_bit14 -X84_bit15 -X84_bit16 -X84_bit17 -X84_bit18 -X84_bit19 -X85_bit_10 X85_bit_9 X85_bit_8 X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X85_bit13 -X85_bit14 -X85_bit15 -X85_bit16 -X85_bit17 -X85_bit18 -X85_bit19 -X86_bit_10 -X86_bit_9 -X86_bit_8 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X86_bit13 -X86_bit14 -X86_bit15 -X86_bit16 -X86_bit17 -X86_bit18 -X86_bit19 -X87_bit_10 -X87_bit_9 -X87_bit_8 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X87_bit13 -X87_bit14 -X87_bit15 -X87_bit16 -X87_bit17 -X87_bit18 -X87_bit19 X88_bit_10 X88_bit_9 -X88_bit_8 -X88_bit_7 -X88_bit_6 -X88_bit_5 X88_bit_4 -X88_bit_3 -X88_bit_2 X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X88_bit13 -X88_bit14 -X88_bit15 -X88_bit16 -X88_bit17 -X88_bit18 -X88_bit19 -X89_bit_10 X89_bit_9 X89_bit_8 -X89_bit_7 -X89_bit_6 X89_bit_5 X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X89_bit13 -X89_bit14 -X89_bit15 -X89_bit16 -X89_bit17 -X89_bit18 -X89_bit19 -X90_bit_10 -X90_bit_9 -X90_bit_8 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X90_bit13 -X90_bit14 -X90_bit15 -X90_bit16 -X90_bit17 -X90_bit18 -X90_bit19 X91_bit_10 X91_bit_9 X91_bit_8 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 X91_bit_3 X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X91_bit13 -X91_bit14 -X91_bit15 -X91_bit16 -X91_bit17 -X91_bit18 -X91_bit19 -X92_bit_10 X92_bit_9 -X92_bit_8 -X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X92_bit13 -X92_bit14 -X92_bit15 -X92_bit16 -X92_bit17 -X92_bit18 -X92_bit19 -X93_bit_10 -X93_bit_9 -X93_bit_8 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X93_bit13 -X93_bit14 -X93_bit15 -X93_bit16 -X93_bit17 -X93_bit18 -X93_bit19 -X94_bit_10 -X94_bit_9 -X94_bit_8 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X94_bit13 -X94_bit14 -X94_bit15 -X94_bit16 -X94_bit17 -X94_bit18 -X94_bit19 -X95_bit_10 -X95_bit_9 X95_bit_8 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X95_bit13 -X95_bit14 -X95_bit15 -X95_bit16 -X95_bit17 -X95_bit18 -X95_bit19 -X96_bit_10 X96_bit_9 X96_bit_8 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X96_bit13 -X96_bit14 -X96_bit15 -X96_bit16 -X96_bit17 -X96_bit18 -X96_bit19 -X97_bit_10 -X97_bit_9 X97_bit_8 X97_bit_7 X97_bit_6 -X97_bit_5 X97_bit_4 X97_bit_3 -X97_bit_2 -X97_bit_1 X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X97_bit13 -X97_bit14 -X97_bit15 -X97_bit16 -X97_bit17 -X97_bit18 -X97_bit19 -X98_bit_10 -X98_bit_9 X98_bit_8 -X98_bit_7 -X98_bit_6 -X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X98_bit13 -X98_bit14 -X98_bit15 -X98_bit16 -X98_bit17 -X98_bit18 -X98_bit19 -X99_bit_10 -X99_bit_9 -X99_bit_8 -X99_bit_7 -X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X99_bit13 -X99_bit14 -X99_bit15 -X99_bit16 -X99_bit17 -X99_bit18 -X99_bit19 -X100_bit_10 -X100_bit_9 -X100_bit_8 -X100_bit_7 -X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X100_bit13 -X100_bit14 -X100_bit15 -X100_bit16 -X100_bit17 -X100_bit18 -X100_bit19 X101_bit_10 X101_bit_9 X101_bit_8 -X101_bit_7 -X101_bit_6 -X101_bit_5 -X101_bit_4 -X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X101_bit13 -X101_bit14 -X101_bit15 -X101_bit16 -X101_bit17 -X101_bit18 -X101_bit19 -X102_bit_10 X102_bit_9 X102_bit_8 -X102_bit_7 -X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X102_bit13 -X102_bit14 -X102_bit15 -X102_bit16 -X102_bit17 -X102_bit18 -X102_bit19 -X103_bit_10 -X103_bit_9 -X103_bit_8 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X103_bit13 -X103_bit14 -X103_bit15 -X103_bit16 -X103_bit17 -X103_bit18 -X103_bit19 X104_bit_10 X104_bit_9 X104_bit_8 -X104_bit_7 -X104_bit_6 -X104_bit_5 -X104_bit_4 -X104_bit_3 X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X104_bit13 -X104_bit14 -X104_bit15 -X104_bit16 -X104_bit17 -X104_bit18 -X104_bit19 X105_bit_10 -X105_bit_9 -X105_bit_8 -X105_bit_7 -X105_bit_6 -X105_bit_5 X105_bit_4 -X105_bit_3 X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 -X105_bit13 -X105_bit14 -X105_bit15 -X105_bit16 -X105_bit17 -X105_bit18 -X105_bit19 -X106_bit_10 -X106_bit_9 -X106_bit_8 -X106_bit_7 -X106_bit_6 -X106_bit_5 -X106_bit_4 -X106_bit_3 -X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X106_bit13 -X106_bit14 -X106_bit15 -X106_bit16 -X106_bit17 -X106_bit18 -X106_bit19 X107_bit_10 -X107_bit_9 -X107_bit_8 X107_bit_7 X107_bit_6 -X107_bit_5 X107_bit_4 -X107_bit_3 -X107_bit_2 -X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X107_bit13 -X107_bit14 -X107_bit15 -X107_bit16 -X107_bit17 -X107_bit18 -X107_bit19 X108_bit_10 -X108_bit_9 -X108_bit_8 -X108_bit_7 -X108_bit_6 X108_bit_5 -X108_bit_4 -X108_bit_3 -X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X108_bit13 -X108_bit14 -X108_bit15 -X108_bit16 -X108_bit17 -X108_bit18 -X108_bit19 -X109_bit_10 X109_bit_9 X109_bit_8 -X109_bit_7 -X109_bit_6 -X109_bit_5 -X109_bit_4 X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X109_bit13 -X109_bit14 -X109_bit15 -X109_bit16 -X109_bit17 -X109_bit18 -X109_bit19 -X110_bit_10 -X110_bit_9 -X110_bit_8 -X110_bit_7 -X110_bit_6 -X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 -X110_bit13 -X110_bit14 -X110_bit15 -X110_bit16 -X110_bit17 -X110_bit18 -X110_bit19 -X111_bit_10 -X111_bit_9 X111_bit_8 X111_bit_7 -X111_bit_6 -X111_bit_5 -X111_bit_4 -X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X111_bit13 -X111_bit14 -X111_bit15 -X111_bit16 -X111_bit17 -X111_bit18 -X111_bit19 -X112_bit_10 -X112_bit_9 -X112_bit_8 -X112_bit_7 -X112_bit_6 -X112_bit_5 -X112_bit_4 -X112_bit_3 -X112_bit_2 -X112_bit_1 X112_bit0 -X112_bit1 -X112_bit2 X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X112_bit13 -X112_bit14 -X112_bit15 -X112_bit16 -X112_bit17 -X112_bit18 -X112_bit19 X113_bit_10 X113_bit_9 X113_bit_8 -X113_bit_7 -X113_bit_6 -X113_bit_5 X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X113_bit13 -X113_bit14 -X113_bit15 -X113_bit16 -X113_bit17 -X113_bit18 -X113_bit19 -X114_bit_10 X114_bit_9 -X114_bit_8 -X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X114_bit13 -X114_bit14 -X114_bit15 -X114_bit16 -X114_bit17 -X114_bit18 -X114_bit19 X115_bit_10 X115_bit_9 -X115_bit_8 -X115_bit_7 -X115_bit_6 X115_bit_5 X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 -X115_bit13 -X115_bit14 -X115_bit15 -X115_bit16 -X115_bit17 -X115_bit18 -X115_bit19 -X116_bit_10 -X116_bit_9 -X116_bit_8 -X116_bit_7 -X116_bit_6 -X116_bit_5 -X116_bit_4 -X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X116_bit13 -X116_bit14 -X116_bit15 -X116_bit16 -X116_bit17 -X116_bit18 -X116_bit19 X117_bit_10 X117_bit_9 X117_bit_8 -X117_bit_7 -X117_bit_6 -X117_bit_5 X117_bit_4 X117_bit_3 X117_bit_2 -X117_bit_1 X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 -X117_bit13 -X117_bit14 -X117_bit15 -X117_bit16 -X117_bit17 -X117_bit18 -X117_bit19 -X118_bit_10 -X118_bit_9 -X118_bit_8 -X118_bit_7 -X118_bit_6 -X118_bit_5 -X118_bit_4 -X118_bit_3 -X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 -X118_bit13 -X118_bit14 -X118_bit15 -X118_bit16 -X118_bit17 -X118_bit18 -X118_bit19 -X119_bit_10 -X119_bit_9 -X119_bit_8 -X119_bit_7 -X119_bit_6 -X119_bit_5 -X119_bit_4 -X119_bit_3 -X119_bit_2 -X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 -X119_bit13 -X119_bit14 -X119_bit15 -X119_bit16 -X119_bit17 -X119_bit18 -X119_bit19 X120_bit_10 X120_bit_9 -X120_bit_8 -X120_bit_7 -X120_bit_6 -X120_bit_5 -X120_bit_4 X120_bit_3 X120_bit_2 -X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X120_bit13 -X120_bit14 -X120_bit15 -X120_bit16 -X120_bit17 -X120_bit18 -X120_bit19 -X121_bit_10 -X121_bit_9 -X121_bit_8 -X121_bit_7 -X121_bit_6 -X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X121_bit13 -X121_bit14 -X121_bit15 -X121_bit16 -X121_bit17 -X121_bit18 -X121_bit19 -X122_bit_10 -X122_bit_9 -X122_bit_8 -X122_bit_7 -X122_bit_6 -X122_bit_5 -X122_bit_4 -X122_bit_3 -X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X122_bit13 -X122_bit14 -X122_bit15 -X122_bit16 -X122_bit17 -X122_bit18 -X122_bit19 -X123_bit_10 X123_bit_9 X123_bit_8 -X123_bit_7 X123_bit_6 -X123_bit_5 X123_bit_4 X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 -X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 -X123_bit13 -X123_bit14 -X123_bit15 -X123_bit16 -X123_bit17 -X123_bit18 -X123_bit19 X124_bit_10 -X124_bit_9 X124_bit_8 -X124_bit_7 -X124_bit_6 -X124_bit_5 -X124_bit_4 -X124_bit_3 -X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 -X124_bit13 -X124_bit14 -X124_bit15 -X124_bit16 -X124_bit17 -X124_bit18 -X124_bit19 -X125_bit_10 -X125_bit_9 -X125_bit_8 -X125_bit_7 -X125_bit_6 -X125_bit_5 -X125_bit_4 -X125_bit_3 -X125_bit_2 -X125_bit_1 -X125_bit0 -X125_bit1 -X125_bit2 X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 -X125_bit13 -X125_bit14 -X125_bit15 -X125_bit16 -X125_bit17 -X125_bit18 -X125_bit19 -X126_bit_10 -X126_bit_9 -X126_bit_8 X126_bit_7 -X126_bit_6 -X126_bit_5 -X126_bit_4 -X126_bit_3 -X126_bit_2 -X126_bit_1 X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 -X126_bit13 -X126_bit14 -X126_bit15 -X126_bit16 -X126_bit17 -X126_bit18 -X126_bit19 X127_bit_10 X127_bit_9 X127_bit_8 -X127_bit_7 -X127_bit_6 -X127_bit_5 -X127_bit_4 X127_bit_3 X127_bit_2 X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X127_bit13 -X127_bit14 -X127_bit15 -X127_bit16 -X127_bit17 -X127_bit18 -X127_bit19 -X128_bit_10 -X128_bit_9 X128_bit_8 X128_bit_7 -X128_bit_6 -X128_bit_5 X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 -X128_bit13 -X128_bit14 -X128_bit15 -X128_bit16 -X128_bit17 -X128_bit18 -X128_bit19 -X129_bit_10 -X129_bit_9 -X129_bit_8 -X129_bit_7 -X129_bit_6 -X129_bit_5 -X129_bit_4 -X129_bit_3 -X129_bit_2 -X129_bit_1 -X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X129_bit13 -X129_bit14 -X129_bit15 -X129_bit16 -X129_bit17 -X129_bit18 -X129_bit19 X130_bit_10 X130_bit_9 X130_bit_8 X130_bit_7 -X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 -X130_bit_1 X130_bit0 -X130_bit1 X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X130_bit13 -X130_bit14 -X130_bit15 -X130_bit16 -X130_bit17 -X130_bit18 -X130_bit19 -X131_bit_10 -X131_bit_9 -X131_bit_8 -X131_bit_7 -X131_bit_6 -X131_bit_5 -X131_bit_4 -X131_bit_3 -X131_bit_2 -X131_bit_1 -X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 -X131_bit13 -X131_bit14 -X131_bit15 -X131_bit16 -X131_bit17 -X131_bit18 -X131_bit19 -X132_bit_10 -X132_bit_9 -X132_bit_8 -X132_bit_7 -X132_bit_6 -X132_bit_5 -X132_bit_4 -X132_bit_3 -X132_bit_2 -X132_bit_1 -X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X132_bit13 -X132_bit14 -X132_bit15 -X132_bit16 -X132_bit17 -X132_bit18 -X132_bit19 X133_bit_10 X133_bit_9 -X133_bit_8 -X133_bit_7 -X133_bit_6 -X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 -X133_bit13 -X133_bit14 -X133_bit15 -X133_bit16 -X133_bit17 -X133_bit18 -X133_bit19 -X134_bit_10 -X134_bit_9 -X134_bit_8 -X134_bit_7 -X134_bit_6 -X134_bit_5 -X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 -X134_bit13 -X134_bit14 -X134_bit15 -X134_bit16 -X134_bit17 -X134_bit18 -X134_bit19 X135_bit_10 X135_bit_9 X135_bit_8 -X135_bit_7 -X135_bit_6 -X135_bit_5 -X135_bit_4 X135_bit_3 -X135_bit_2 X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 -X135_bit13 -X135_bit14 -X135_bit15 -X135_bit16 -X135_bit17 -X135_bit18 -X135_bit19 -X136_bit_10 X136_bit_9 -X136_bit_8 X136_bit_7 -X136_bit_6 -X136_bit_5 -X136_bit_4 -X136_bit_3 -X136_bit_2 -X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 -X136_bit13 -X136_bit14 -X136_bit15 -X136_bit16 -X136_bit17 -X136_bit18 -X136_bit19 X137_bit_10 -X137_bit_9 X137_bit_8 X137_bit_7 -X137_bit_6 -X137_bit_5 -X137_bit_4 -X137_bit_3 X137_bit_2 -X137_bit_1 -X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 -X137_bit13 -X137_bit14 -X137_bit15 -X137_bit16 -X137_bit17 -X137_bit18 -X137_bit19 -X138_bit_10 -X138_bit_9 -X138_bit_8 -X138_bit_7 -X138_bit_6 -X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 -X138_bit13 -X138_bit14 -X138_bit15 -X138_bit16 -X138_bit17 -X138_bit18 -X138_bit19 X139_bit_10 -X139_bit_9 X139_bit_8 -X139_bit_7 -X139_bit_6 -X139_bit_5 -X139_bit_4 -X139_bit_3 -X139_bit_2 -X139_bit_1 -X139_bit0 -X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 -X139_bit13 -X139_bit14 -X139_bit15 -X139_bit16 -X139_bit17 -X139_bit18 -X139_bit19 -X140_bit_10 -X140_bit_9 -X140_bit_8 -X140_bit_7 -X140_bit_6 -X140_bit_5 -X140_bit_4 -X140_bit_3 -X140_bit_2 -X140_bit_1 -X140_bit0 -X140_bit1 -X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 -X140_bit13 -X140_bit14 -X140_bit15 -X140_bit16 -X140_bit17 -X140_bit18 -X140_bit19 X141_bit_10 X141_bit_9 -X141_bit_8 X141_bit_7 -X141_bit_6 -X141_bit_5 X141_bit_4 -X141_bit_3 -X141_bit_2 -X141_bit_1 -X141_bit0 X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 -X141_bit13 -X141_bit14 -X141_bit15 -X141_bit16 -X141_bit17 -X141_bit18 -X141_bit19 -X142_bit_10 -X142_bit_9 -X142_bit_8 -X142_bit_7 -X142_bit_6 -X142_bit_5 -X142_bit_4 -X142_bit_3 -X142_bit_2 -X142_bit_1 -X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 -X142_bit13 -X142_bit14 -X142_bit15 -X142_bit16 -X142_bit17 -X142_bit18 -X142_bit19 X143_bit_10 X143_bit_9 X143_bit_8 -X143_bit_7 -X143_bit_6 -X143_bit_5 X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 -X143_bit13 -X143_bit14 -X143_bit15 -X143_bit16 -X143_bit17 -X143_bit18 -X143_bit19 -X144_bit_10 X144_bit_9 X144_bit_8 X144_bit_7 -X144_bit_6 X144_bit_5 X144_bit_4 -X144_bit_3 -X144_bit_2 X144_bit_1 X144_bit0 -X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 -X144_bit13 -X144_bit14 -X144_bit15 -X144_bit16 -X144_bit17 -X144_bit18 -X144_bit19 -X145_bit_10 -X145_bit_9 -X145_bit_8 -X145_bit_7 -X145_bit_6 -X145_bit_5 -X145_bit_4 -X145_bit_3 -X145_bit_2 -X145_bit_1 X145_bit0 -X145_bit1 -X145_bit2 X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 -X145_bit13 -X145_bit14 -X145_bit15 -X145_bit16 -X145_bit17 -X145_bit18 -X145_bit19 -X146_bit_10 -X146_bit_9 -X146_bit_8 -X146_bit_7 -X146_bit_6 -X146_bit_5 -X146_bit_4 -X146_bit_3 -X146_bit_2 -X146_bit_1 -X146_bit0 -X146_bit1 -X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 -X146_bit13 -X146_bit14 -X146_bit15 -X146_bit16 -X146_bit17 -X146_bit18 -X146_bit19 -X147_bit_10 -X147_bit_9 X147_bit_8 -X147_bit_7 -X147_bit_6 -X147_bit_5 -X147_bit_4 -X147_bit_3 -X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 -X147_bit13 -X147_bit14 -X147_bit15 -X147_bit16 -X147_bit17 -X147_bit18 -X147_bit19 -X148_bit_10 X148_bit_9 X148_bit_8 X148_bit_7 -X148_bit_6 -X148_bit_5 -X148_bit_4 X148_bit_3 -X148_bit_2 X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 -X148_bit13 -X148_bit14 -X148_bit15 -X148_bit16 -X148_bit17 -X148_bit18 -X148_bit19 -X149_bit_10 -X149_bit_9 -X149_bit_8 -X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 -X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 -X149_bit13 -X149_bit14 -X149_bit15 -X149_bit16 -X149_bit17 -X149_bit18 -X149_bit19 -X150_bit_10 X150_bit_9 X150_bit_8 -X150_bit_7 -X150_bit_6 -X150_bit_5 -X150_bit_4 -X150_bit_3 X150_bit_2 -X150_bit_1 -X150_bit0 -X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X150_bit13 -X150_bit14 -X150_bit15 -X150_bit16 -X150_bit17 -X150_bit18 -X150_bit19 -X151_bit_10 -X151_bit_9 -X151_bit_8 -X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 -X151_bit_3 -X151_bit_2 -X151_bit_1 -X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X151_bit13 -X151_bit14 -X151_bit15 -X151_bit16 -X151_bit17 -X151_bit18 -X151_bit19 -X152_bit_10 X152_bit_9 -X152_bit_8 X152_bit_7 -X152_bit_6 -X152_bit_5 -X152_bit_4 -X152_bit_3 -X152_bit_2 -X152_bit_1 -X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 -X152_bit13 -X152_bit14 -X152_bit15 -X152_bit16 -X152_bit17 -X152_bit18 -X152_bit19 X153_bit_10 X153_bit_9 -X153_bit_8 -X153_bit_7 -X153_bit_6 -X153_bit_5 -X153_bit_4 X153_bit_3 X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 -X153_bit13 -X153_bit14 -X153_bit15 -X153_bit16 -X153_bit17 -X153_bit18 -X153_bit19 -X154_bit_10 X154_bit_9 X154_bit_8 -X154_bit_7 -X154_bit_6 X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 -X154_bit_1 -X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 -X154_bit13 -X154_bit14 -X154_bit15 -X154_bit16 -X154_bit17 -X154_bit18 -X154_bit19 -X155_bit_10 -X155_bit_9 -X155_bit_8 -X155_bit_7 -X155_bit_6 -X155_bit_5 -X155_bit_4 -X155_bit_3 -X155_bit_2 -X155_bit_1 -X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X155_bit13 -X155_bit14 -X155_bit15 -X155_bit16 -X155_bit17 -X155_bit18 -X155_bit19 -X156_bit_10 X156_bit_9 X156_bit_8 -X156_bit_7 -X156_bit_6 -X156_bit_5 -X156_bit_4 X156_bit_3 X156_bit_2 -X156_bit_1 -X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 -X156_bit13 -X156_bit14 -X156_bit15 -X156_bit16 -X156_bit17 -X156_bit18 -X156_bit19 -X157_bit_10 X157_bit_9 -X157_bit_8 X157_bit_7 -X157_bit_6 X157_bit_5 X157_bit_4 -X157_bit_3 -X157_bit_2 -X157_bit_1 X157_bit0 X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X157_bit13 -X157_bit14 -X157_bit15 -X157_bit16 -X157_bit17 -X157_bit18 -X157_bit19 -X158_bit_10 -X158_bit_9 -X158_bit_8 -X158_bit_7 -X158_bit_6 -X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 -X158_bit_1 -X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X158_bit13 -X158_bit14 -X158_bit15 -X158_bit16 -X158_bit17 -X158_bit18 -X158_bit19 -X159_bit_10 -X159_bit_9 -X159_bit_8 X159_bit_7 X159_bit_6 -X159_bit_5 -X159_bit_4 X159_bit_3 X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 -X159_bit13 -X159_bit14 -X159_bit15 -X159_bit16 -X159_bit17 -X159_bit18 -X159_bit19 -X160_bit_10 -X160_bit_9 -X160_bit_8 -X160_bit_7 -X160_bit_6 -X160_bit_5 -X160_bit_4 -X160_bit_3 -X160_bit_2 -X160_bit_1 -X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X160_bit13 -X160_bit14 -X160_bit15 -X160_bit16 -X160_bit17 -X160_bit18 -X160_bit19 -X161_bit_10 -X161_bit_9 -X161_bit_8 -X161_bit_7 -X161_bit_6 -X161_bit_5 -X161_bit_4 -X161_bit_3 -X161_bit_2 -X161_bit_1 -X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 -X161_bit13 -X161_bit14 -X161_bit15 -X161_bit16 -X161_bit17 -X161_bit18 -X161_bit19 -X162_bit_10 -X162_bit_9 -X162_bit_8 -X162_bit_7 -X162_bit_6 -X162_bit_5 -X162_bit_4 -X162_bit_3 -X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 -X162_bit13 -X162_bit14 -X162_bit15 -X162_bit16 -X162_bit17 -X162_bit18 -X162_bit19 -X163_bit_10 -X163_bit_9 -X163_bit_8 -X163_bit_7 -X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 -X163_bit_2 -X163_bit_1 -X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X163_bit13 -X163_bit14 -X163_bit15 -X163_bit16 -X163_bit17 -X163_bit18 -X163_bit19 -X164_bit_10 -X164_bit_9 -X164_bit_8 -X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 -X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X164_bit13 -X164_bit14 -X164_bit15 -X164_bit16 -X164_bit17 -X164_bit18 -X164_bit19 -X165_bit_10 -X165_bit_9 -X165_bit_8 -X165_bit_7 -X165_bit_6 -X165_bit_5 -X165_bit_4 -X165_bit_3 -X165_bit_2 -X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 -X165_bit13 -X165_bit14 -X165_bit15 -X165_bit16 -X165_bit17 -X165_bit18 -X165_bit19 -X166_bit_10 X166_bit_9 -X166_bit_8 -X166_bit_7 X166_bit_6 -X166_bit_5 X166_bit_4 -X166_bit_3 -X166_bit_2 -X166_bit_1 -X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 -X166_bit13 -X166_bit14 -X166_bit15 -X166_bit16 -X166_bit17 -X166_bit18 -X166_bit19 -X167_bit_10 X167_bit_9 X167_bit_8 -X167_bit_7 -X167_bit_6 X167_bit_5 -X167_bit_4 -X167_bit_3 -X167_bit_2 -X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 -X167_bit13 -X167_bit14 -X167_bit15 -X167_bit16 -X167_bit17 -X167_bit18 -X167_bit19 -X168_bit_10 -X168_bit_9 -X168_bit_8 -X168_bit_7 -X168_bit_6 -X168_bit_5 -X168_bit_4 -X168_bit_3 -X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -X168_bit13 -X168_bit14 -X168_bit15 -X168_bit16 -X168_bit17 -X168_bit18 -X168_bit19 -Y0_bit0 -Y1_bit0 -Y2_bit0 -Y3_bit0 Y4_bit0 -Y5_bit0 Y6_bit0 Y7_bit0 -Y8_bit0 Y9_bit0 -Y10_bit0 Y11_bit0 Y12_bit0 -Y13_bit0 Y14_bit0 Y15_bit0 -Y16_bit0 Y17_bit0 Y18_bit0 -Y19_bit0 -Y20_bit0 -Y21_bit0 Y22_bit0 -Y23_bit0 Y24_bit0 -Y25_bit0 -Y26_bit0 -Y27_bit0 -Y28_bit0 -Y29_bit0 Y30_bit0 Y31_bit0 Y32_bit0 -Y33_bit0 -Y34_bit0 Y35_bit0 Y36_bit0 -Y37_bit0 Y38_bit0 Y39_bit0 -Y40_bit0 -Y41_bit0 -Y42_bit0 -Y43_bit0 Y44_bit0 -Y45_bit0 Y46_bit0 -Y47_bit0 Y48_bit0 -Y49_bit0 -Y50_bit0 -Y51_bit0 Y52_bit0 Y53_bit0 -Y54_bit0 -Y55_bit0 Y56_bit0 Y57_bit0 -Y58_bit0 Y59_bit0 -Y60_bit0 -Y61_bit0 -Y62_bit0 Y63_bit0 -Y64_bit0 -Y65_bit0 -Y66_bit0 Y67_bit0 Y68_bit0 Y69_bit0 -Y70_bit0 -Y71_bit0 -Y72_bit0 Y73_bit0 Y74_bit0 -Y75_bit0 Y76_bit0 Y77_bit0 Y78_bit0 Y79_bit0 -Y80_bit0 Y81_bit0 -Y82_bit0 Y83_bit0 -Y84_bit0 Y85_bit0 -Y86_bit0 Y87_bit0 Y88_bit0 Y89_bit0 -Y90_bit0 Y91_bit0 Y92_bit0 Y93_bit0 -Y94_bit0 Y95_bit0 Y96_bit0 Y97_bit0 Y98_bit0 Y99_bit0 -Y100_bit0 Y101_bit0 Y102_bit0 -Y103_bit0 Y104_bit0 Y105_bit0 -Y106_bit0 Y107_bit0 Y108_bit0 Y109_bit0 -Y110_bit0 Y111_bit0 Y112_bit0 Y113_bit0 Y114_bit0 Y115_bit0 -Y116_bit0 Y117_bit0 -Y118_bit0 -Y119_bit0 Y120_bit0 -Y121_bit0 -Y122_bit0 Y123_bit0 Y124_bit0 Y125_bit0 Y126_bit0 Y127_bit0 Y128_bit0 -Y129_bit0 Y130_bit0 -Y131_bit0 -Y132_bit0 Y133_bit0 -Y134_bit0 Y135_bit0 Y136_bit0 Y137_bit0 -Y138_bit0 Y139_bit0 -Y140_bit0 Y141_bit0 -Y142_bit0 Y143_bit0 Y144_bit0 Y145_bit0 -Y146_bit0 Y147_bit0 Y148_bit0 -Y149_bit0 Y150_bit0 Y151_bit0 Y152_bit0 Y153_bit0 Y154_bit0 -Y155_bit0 Y156_bit0 Y157_bit0 Y158_bit0 Y159_bit0 -Y160_bit0 -Y161_bit0 -Y162_bit0 -Y163_bit0

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/12903/stat): 12903 (minisat+_script) R 12902 12903 22582 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796366916 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/12903/statm): 174 3 169 147 0 27 0
[pid=12903] 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=12904
New process pid=12905
New process pid=12906
execve syscall for /bin/sed executable
One traced child (pid=12905) 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=12906) exited with status: 0
One traced child (pid=12904) exited with status: 0
New process pid=12907
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-ran13x13.opb

[startup+10.0041 s]
Raw data (loadavg): 0.84 0.82 0.88 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 1596 0 0 0 980 7 0 0 25 0 1 0 1796366921 6889472 1583 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 1682 1583 145 145 0 1537 0
[pid=12907] vsize: 6728
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 8852

[startup+20.0047 s]
Raw data (loadavg): 0.87 0.82 0.88 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 1968 0 0 0 1974 10 0 0 25 0 1 0 1796366921 8445952 1955 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 2062 1955 145 145 0 1917 0
[pid=12907] vsize: 8248
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 10372

[startup+30.0062 s]
Raw data (loadavg): 0.89 0.83 0.88 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 2919 0 0 0 2960 17 0 0 25 0 1 0 1796366921 12414976 2906 4294967295 134512640 135094434 3221224432 3221223024 134552168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 3031 2906 145 145 0 2886 0
[pid=12907] vsize: 12124
Current children cumulated CPU time (s) 29.79
Current children cumulated vsize (Kb) 14248

[startup+40.0068 s]
Raw data (loadavg): 0.90 0.83 0.89 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 3200 0 0 0 3955 20 0 0 25 0 1 0 1796366921 13529088 3187 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 3303 3187 145 145 0 3158 0
[pid=12907] vsize: 13212
Current children cumulated CPU time (s) 39.77
Current children cumulated vsize (Kb) 15336

[startup+50.0073 s]
Raw data (loadavg): 0.92 0.84 0.89 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 3444 0 0 0 4948 22 0 0 25 0 1 0 1796366921 14491648 3431 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 3538 3431 145 145 0 3393 0
[pid=12907] vsize: 14152
Current children cumulated CPU time (s) 49.72
Current children cumulated vsize (Kb) 16276

[startup+60.0079 s]
Raw data (loadavg): 0.93 0.84 0.89 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 3842 0 0 0 5941 26 0 0 25 0 1 0 1796366921 16334848 3829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 3988 3829 145 145 0 3843 0
[pid=12907] vsize: 15952
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 18076

[startup+70.0085 s]
Raw data (loadavg): 0.94 0.85 0.89 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 4148 0 0 0 6935 29 0 0 25 0 1 0 1796366921 17551360 4135 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 4285 4135 145 145 0 4140 0
[pid=12907] vsize: 17140
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 19264

[startup+80.01 s]
Raw data (loadavg): 0.95 0.85 0.89 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 4233 0 0 0 7933 30 0 0 25 0 1 0 1796366921 17887232 4220 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 4367 4220 145 145 0 4222 0
[pid=12907] vsize: 17468
Current children cumulated CPU time (s) 79.65
Current children cumulated vsize (Kb) 19592

[startup+90.0106 s]
Raw data (loadavg): 0.96 0.86 0.89 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 4233 0 0 0 8933 30 0 0 25 0 1 0 1796366921 17887232 4220 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 4367 4220 145 145 0 4222 0
[pid=12907] vsize: 17468
Current children cumulated CPU time (s) 89.65
Current children cumulated vsize (Kb) 19592

[startup+100.011 s]
Raw data (loadavg): 0.96 0.86 0.89 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 4233 0 0 0 9933 31 0 0 25 0 1 0 1796366921 17887232 4220 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 4367 4220 145 145 0 4222 0
[pid=12907] vsize: 17468
Current children cumulated CPU time (s) 99.66
Current children cumulated vsize (Kb) 19592

[startup+110.013 s]
Raw data (loadavg): 0.97 0.87 0.89 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 4233 0 0 0 10932 31 0 0 25 0 1 0 1796366921 17887232 4220 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 4367 4220 145 145 0 4222 0
[pid=12907] vsize: 17468
Current children cumulated CPU time (s) 109.65
Current children cumulated vsize (Kb) 19592

[startup+120.013 s]
Raw data (loadavg): 0.97 0.87 0.89 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 8350 0 0 0 11909 45 0 0 25 0 1 0 1796366921 35270656 7673 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 8611 7673 145 145 0 8466 0
[pid=12907] vsize: 34444
Current children cumulated CPU time (s) 119.56
Current children cumulated vsize (Kb) 36568

[startup+130.015 s]
Raw data (loadavg): 0.98 0.87 0.89 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 8350 0 0 0 12909 46 0 0 25 0 1 0 1796366921 35270656 7673 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 8611 7673 145 145 0 8466 0
[pid=12907] vsize: 34444
Current children cumulated CPU time (s) 129.57
Current children cumulated vsize (Kb) 36568

[startup+140.016 s]
Raw data (loadavg): 0.98 0.88 0.89 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 8350 0 0 0 13909 46 0 0 25 0 1 0 1796366921 35270656 7673 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 8611 7673 145 145 0 8466 0
[pid=12907] vsize: 34444
Current children cumulated CPU time (s) 139.57
Current children cumulated vsize (Kb) 36568

[startup+150.017 s]
Raw data (loadavg): 0.98 0.88 0.90 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 8350 0 0 0 14908 46 0 0 25 0 1 0 1796366921 35270656 7673 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 8611 7673 145 145 0 8466 0
[pid=12907] vsize: 34444
Current children cumulated CPU time (s) 149.56
Current children cumulated vsize (Kb) 36568

[startup+160.019 s]
Raw data (loadavg): 0.98 0.88 0.90 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 8350 0 0 0 15908 47 0 0 25 0 1 0 1796366921 35270656 7673 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 8611 7673 145 145 0 8466 0
[pid=12907] vsize: 34444
Current children cumulated CPU time (s) 159.57
Current children cumulated vsize (Kb) 36568

[startup+170.019 s]
Raw data (loadavg): 0.99 0.89 0.90 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 8522 0 0 0 16907 48 0 0 25 0 1 0 1796366921 35389440 7722 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 8640 7722 145 145 0 8495 0
[pid=12907] vsize: 34560
Current children cumulated CPU time (s) 169.57
Current children cumulated vsize (Kb) 36684

[startup+180.02 s]
Raw data (loadavg): 0.99 0.89 0.90 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 8522 0 0 0 17906 48 0 0 25 0 1 0 1796366921 35389440 7722 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 8640 7722 145 145 0 8495 0
[pid=12907] vsize: 34560
Current children cumulated CPU time (s) 179.56
Current children cumulated vsize (Kb) 36684

[startup+190.021 s]
Raw data (loadavg): 0.99 0.89 0.90 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 8522 0 0 0 18906 49 0 0 25 0 1 0 1796366921 35389440 7722 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 8640 7722 145 145 0 8495 0
[pid=12907] vsize: 34560
Current children cumulated CPU time (s) 189.57
Current children cumulated vsize (Kb) 36684

[startup+200.022 s]
Raw data (loadavg): 0.99 0.90 0.90 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 8522 0 0 0 19906 49 0 0 25 0 1 0 1796366921 35389440 7722 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 8640 7722 145 145 0 8495 0
[pid=12907] vsize: 34560
Current children cumulated CPU time (s) 199.57
Current children cumulated vsize (Kb) 36684

[startup+210.022 s]
Raw data (loadavg): 0.99 0.90 0.90 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 8522 0 0 0 20905 49 0 0 25 0 1 0 1796366921 35389440 7722 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 8640 7722 145 145 0 8495 0
[pid=12907] vsize: 34560
Current children cumulated CPU time (s) 209.56
Current children cumulated vsize (Kb) 36684

[startup+220.024 s]
Raw data (loadavg): 0.99 0.90 0.90 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 8522 0 0 0 21905 50 0 0 25 0 1 0 1796366921 35389440 7722 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 8640 7722 145 145 0 8495 0
[pid=12907] vsize: 34560
Current children cumulated CPU time (s) 219.57
Current children cumulated vsize (Kb) 36684

[startup+230.025 s]
Raw data (loadavg): 0.99 0.91 0.90 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 8847 0 0 0 22899 52 0 0 25 0 1 0 1796366921 36720640 8047 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 8965 8047 145 145 0 8820 0
[pid=12907] vsize: 35860
Current children cumulated CPU time (s) 229.53
Current children cumulated vsize (Kb) 37984

[startup+240.026 s]
Raw data (loadavg): 0.99 0.91 0.90 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 9822 0 0 0 23881 59 0 0 25 0 1 0 1796366921 40714240 9022 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 9940 9022 145 145 0 9795 0
[pid=12907] vsize: 39760
Current children cumulated CPU time (s) 239.42
Current children cumulated vsize (Kb) 41884

[startup+250.027 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 10735 0 0 0 24867 65 0 0 25 0 1 0 1796366921 44453888 9935 4294967295 134512640 135094434 3221224432 3221223024 134557275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 10853 9935 145 145 0 10708 0
[pid=12907] vsize: 43412
Current children cumulated CPU time (s) 249.34
Current children cumulated vsize (Kb) 45536

[startup+260.028 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 11555 0 0 0 25853 71 0 0 25 0 1 0 1796366921 47812608 10755 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 11673 10755 145 145 0 11528 0
[pid=12907] vsize: 46692
Current children cumulated CPU time (s) 259.26
Current children cumulated vsize (Kb) 48816

[startup+270.029 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 12253 0 0 0 26842 75 0 0 25 0 1 0 1796366921 50663424 11453 4294967295 134512640 135094434 3221224432 3221223044 134563077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 12369 11453 145 145 0 12224 0
[pid=12907] vsize: 49476
Current children cumulated CPU time (s) 269.19
Current children cumulated vsize (Kb) 51600

[startup+280.029 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 12498 0 0 0 27839 77 0 0 25 0 1 0 1796366921 51642368 11698 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 12608 11698 145 145 0 12463 0
[pid=12907] vsize: 50432
Current children cumulated CPU time (s) 279.18
Current children cumulated vsize (Kb) 52556

[startup+290.03 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 13566 0 0 0 28822 84 0 0 25 0 1 0 1796366921 55996416 12766 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 13671 12766 145 145 0 13526 0
[pid=12907] vsize: 54684
Current children cumulated CPU time (s) 289.08
Current children cumulated vsize (Kb) 56808

[startup+300.029 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 14456 0 0 0 29807 88 0 0 25 0 1 0 1796366921 59629568 13656 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 14558 13656 145 145 0 14413 0
[pid=12907] vsize: 58232
Current children cumulated CPU time (s) 298.97
Current children cumulated vsize (Kb) 60356

[startup+310.03 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 15256 0 0 0 30792 95 0 0 18 0 1 0 1796366921 62902272 14456 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 15357 14456 145 145 0 15212 0
[pid=12907] vsize: 61428
Current children cumulated CPU time (s) 308.89
Current children cumulated vsize (Kb) 63552

[startup+320.031 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 15955 0 0 0 31780 100 0 0 25 0 1 0 1796366921 65753088 15155 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 16053 15155 145 145 0 15908 0
[pid=12907] vsize: 64212
Current children cumulated CPU time (s) 318.82
Current children cumulated vsize (Kb) 66336

[startup+330.032 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 16721 0 0 0 32767 106 0 0 25 0 1 0 1796366921 68882432 15921 4294967295 134512640 135094434 3221224432 3221222976 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 16817 15921 145 145 0 16672 0
[pid=12907] vsize: 67268
Current children cumulated CPU time (s) 328.75
Current children cumulated vsize (Kb) 69392

[startup+340.033 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 17455 0 0 0 33752 111 0 0 25 0 1 0 1796366921 71901184 16655 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 17554 16655 145 145 0 17409 0
[pid=12907] vsize: 70216
Current children cumulated CPU time (s) 338.65
Current children cumulated vsize (Kb) 72340

[startup+350.033 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 17832 0 0 0 34744 115 0 0 25 0 1 0 1796366921 73433088 17032 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 17928 17032 145 145 0 17783 0
[pid=12907] vsize: 71712
Current children cumulated CPU time (s) 348.61
Current children cumulated vsize (Kb) 73836

[startup+360.035 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18253 0 0 0 35740 117 0 0 25 0 1 0 1796366921 74502144 17285 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17285 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 358.59
Current children cumulated vsize (Kb) 74880

[startup+370.035 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18253 0 0 0 36739 117 0 0 25 0 1 0 1796366921 74502144 17285 4294967295 134512640 135094434 3221224432 3221223044 134563030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17285 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 368.58
Current children cumulated vsize (Kb) 74880

[startup+380.037 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18253 0 0 0 37739 118 0 0 25 0 1 0 1796366921 74502144 17285 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17285 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 378.59
Current children cumulated vsize (Kb) 74880

[startup+390.037 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18253 0 0 0 38739 118 0 0 25 0 1 0 1796366921 74502144 17285 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17285 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 388.59
Current children cumulated vsize (Kb) 74880

[startup+400.038 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18253 0 0 0 39738 118 0 0 25 0 1 0 1796366921 74502144 17285 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17285 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 398.58
Current children cumulated vsize (Kb) 74880

[startup+410.04 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18253 0 0 0 40738 119 0 0 25 0 1 0 1796366921 74502144 17285 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17285 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 408.59
Current children cumulated vsize (Kb) 74880

[startup+420.04 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18253 0 0 0 41738 119 0 0 25 0 1 0 1796366921 74502144 17285 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17285 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 418.59
Current children cumulated vsize (Kb) 74880

[startup+430.042 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18253 0 0 0 42738 120 0 0 25 0 1 0 1796366921 74502144 17285 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17285 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 428.6
Current children cumulated vsize (Kb) 74880

[startup+440.042 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18253 0 0 0 43738 120 0 0 25 0 1 0 1796366921 74502144 17285 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17285 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 438.6
Current children cumulated vsize (Kb) 74880

[startup+450.043 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18253 0 0 0 44737 120 0 0 25 0 1 0 1796366921 74502144 17285 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17285 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 448.59
Current children cumulated vsize (Kb) 74880

[startup+460.044 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18253 0 0 0 45737 121 0 0 25 0 1 0 1796366921 74502144 17285 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17285 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 458.6
Current children cumulated vsize (Kb) 74880

[startup+470.045 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18255 0 0 0 46737 121 0 0 25 0 1 0 1796366921 74502144 17287 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17287 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 468.6
Current children cumulated vsize (Kb) 74880

[startup+480.047 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18256 0 0 0 47737 121 0 0 25 0 1 0 1796366921 74502144 17288 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17288 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 478.6
Current children cumulated vsize (Kb) 74880

[startup+490.047 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18259 0 0 0 48736 122 0 0 25 0 1 0 1796366921 74502144 17291 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17291 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 488.6
Current children cumulated vsize (Kb) 74880

[startup+500.048 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18263 0 0 0 49736 122 0 0 25 0 1 0 1796366921 74502144 17295 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 18189 17295 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 498.6
Current children cumulated vsize (Kb) 74880

[startup+510.049 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18263 0 0 0 50736 122 0 0 25 0 1 0 1796366921 74502144 17295 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17295 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 508.6
Current children cumulated vsize (Kb) 74880

[startup+520.05 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18263 0 0 0 51736 122 0 0 25 0 1 0 1796366921 74502144 17295 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17295 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 518.6
Current children cumulated vsize (Kb) 74880

[startup+530.051 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18263 0 0 0 52737 122 0 0 25 0 1 0 1796366921 74502144 17295 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17295 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 528.61
Current children cumulated vsize (Kb) 74880

[startup+540.052 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 53736 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223024 134551421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 538.61
Current children cumulated vsize (Kb) 74880

[startup+550.052 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 54737 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 548.62
Current children cumulated vsize (Kb) 74880

[startup+560.054 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 55737 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223044 134563127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 558.62
Current children cumulated vsize (Kb) 74880

[startup+570.055 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 56737 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 568.62
Current children cumulated vsize (Kb) 74880

[startup+580.055 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 57737 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 578.62
Current children cumulated vsize (Kb) 74880

[startup+590.056 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 58737 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 588.62
Current children cumulated vsize (Kb) 74880

[startup+600.056 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 59738 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 598.63
Current children cumulated vsize (Kb) 74880

[startup+610.057 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 60738 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 608.63
Current children cumulated vsize (Kb) 74880

[startup+620.057 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 61738 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 618.63
Current children cumulated vsize (Kb) 74880

[startup+630.058 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 62738 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 628.63
Current children cumulated vsize (Kb) 74880

[startup+640.058 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 63738 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 638.63
Current children cumulated vsize (Kb) 74880

[startup+650.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 64738 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 648.63
Current children cumulated vsize (Kb) 74880

[startup+660.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 65739 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 658.64
Current children cumulated vsize (Kb) 74880

[startup+670.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 66739 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 668.64
Current children cumulated vsize (Kb) 74880

[startup+680.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 67739 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 678.64
Current children cumulated vsize (Kb) 74880

[startup+690.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18266 0 0 0 68739 123 0 0 25 0 1 0 1796366921 74502144 17298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17298 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 688.64
Current children cumulated vsize (Kb) 74880

[startup+700.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18270 0 0 0 69740 123 0 0 25 0 1 0 1796366921 74502144 17302 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18189 17302 145 145 0 18044 0
[pid=12907] vsize: 72756
Current children cumulated CPU time (s) 698.65
Current children cumulated vsize (Kb) 74880

[startup+710.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18276 0 0 0 70740 123 0 0 25 0 1 0 1796366921 75026432 17308 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18317 17308 145 145 0 18172 0
[pid=12907] vsize: 73268
Current children cumulated CPU time (s) 708.65
Current children cumulated vsize (Kb) 75392

[startup+720.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18283 0 0 0 71740 124 0 0 25 0 1 0 1796366921 75026432 17315 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18317 17315 145 145 0 18172 0
[pid=12907] vsize: 73268
Current children cumulated CPU time (s) 718.66
Current children cumulated vsize (Kb) 75392

[startup+730.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18290 0 0 0 72740 124 0 0 25 0 1 0 1796366921 75026432 17322 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18317 17322 145 145 0 18172 0
[pid=12907] vsize: 73268
Current children cumulated CPU time (s) 728.66
Current children cumulated vsize (Kb) 75392

[startup+740.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18297 0 0 0 73740 124 0 0 25 0 1 0 1796366921 75026432 17329 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18317 17329 145 145 0 18172 0
[pid=12907] vsize: 73268
Current children cumulated CPU time (s) 738.66
Current children cumulated vsize (Kb) 75392

[startup+750.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18314 0 0 0 74740 124 0 0 25 0 1 0 1796366921 75026432 17346 4294967295 134512640 135094434 3221224432 3221223056 134557653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18317 17346 145 145 0 18172 0
[pid=12907] vsize: 73268
Current children cumulated CPU time (s) 748.66
Current children cumulated vsize (Kb) 75392

[startup+760.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 18487 0 0 0 75738 126 0 0 25 0 1 0 1796366921 75714560 17519 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18485 17519 145 145 0 18340 0
[pid=12907] vsize: 73940
Current children cumulated CPU time (s) 758.66
Current children cumulated vsize (Kb) 76064

[startup+770.067 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) T 12903 12903 22582 0 -1 0 18879 0 0 0 76732 128 0 0 25 0 1 0 1796366921 77324288 17911 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/12907/statm): 18878 17911 145 145 0 18733 0
[pid=12907] vsize: 75512
Current children cumulated CPU time (s) 768.62
Current children cumulated vsize (Kb) 77636

[startup+780.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 19221 0 0 0 77727 131 0 0 25 0 1 0 1796366921 78749696 18253 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 19226 18253 145 145 0 19081 0
[pid=12907] vsize: 76904
Current children cumulated CPU time (s) 778.6
Current children cumulated vsize (Kb) 79028

[startup+790.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 19547 0 0 0 78722 134 0 0 25 0 1 0 1796366921 80064512 18579 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 19547 18579 145 145 0 19402 0
[pid=12907] vsize: 78188
Current children cumulated CPU time (s) 788.58
Current children cumulated vsize (Kb) 80312

[startup+800.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 19855 0 0 0 79718 136 0 0 25 0 1 0 1796366921 81309696 18887 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 19851 18887 145 145 0 19706 0
[pid=12907] vsize: 79404
Current children cumulated CPU time (s) 798.56
Current children cumulated vsize (Kb) 81528

[startup+810.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20145 0 0 0 80713 137 0 0 25 0 1 0 1796366921 82497536 19177 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20141 19177 145 145 0 19996 0
[pid=12907] vsize: 80564
Current children cumulated CPU time (s) 808.52
Current children cumulated vsize (Kb) 82688

[startup+820.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20463 0 0 0 81707 140 0 0 25 0 1 0 1796366921 83795968 19495 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20458 19495 145 145 0 20313 0
[pid=12907] vsize: 81832
Current children cumulated CPU time (s) 818.49
Current children cumulated vsize (Kb) 83956

[startup+830.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20534 0 0 0 82707 140 0 0 25 0 1 0 1796366921 84082688 19566 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19566 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 828.49
Current children cumulated vsize (Kb) 84236

[startup+840.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 83707 140 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 838.49
Current children cumulated vsize (Kb) 84236

[startup+850.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 84708 140 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223104 134556239 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 848.5
Current children cumulated vsize (Kb) 84236

[startup+860.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 85708 140 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 858.5
Current children cumulated vsize (Kb) 84236

[startup+870.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 86708 140 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 868.5
Current children cumulated vsize (Kb) 84236

[startup+880.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 87708 140 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 878.5
Current children cumulated vsize (Kb) 84236

[startup+890.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 88708 140 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221222896 134781514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 888.5
Current children cumulated vsize (Kb) 84236

[startup+900.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 89709 140 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 898.51
Current children cumulated vsize (Kb) 84236

[startup+910.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 90708 142 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 908.52
Current children cumulated vsize (Kb) 84236

[startup+920.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 91708 142 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 918.52
Current children cumulated vsize (Kb) 84236

[startup+930.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 92707 142 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 928.51
Current children cumulated vsize (Kb) 84236

[startup+940.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 93707 143 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221222992 134778841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 938.52
Current children cumulated vsize (Kb) 84236

[startup+950.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 94707 143 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 948.52
Current children cumulated vsize (Kb) 84236

[startup+960.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 95707 143 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 958.52
Current children cumulated vsize (Kb) 84236

[startup+970.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 96707 143 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 968.52
Current children cumulated vsize (Kb) 84236

[startup+980.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 97708 143 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 978.53
Current children cumulated vsize (Kb) 84236

[startup+990.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 98708 143 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 988.53
Current children cumulated vsize (Kb) 84236

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 99708 143 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 998.53
Current children cumulated vsize (Kb) 84236

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 100708 143 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 1008.53
Current children cumulated vsize (Kb) 84236

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 101708 144 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 1018.54
Current children cumulated vsize (Kb) 84236

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 102708 144 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 1028.54
Current children cumulated vsize (Kb) 84236

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 103708 144 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 1038.54
Current children cumulated vsize (Kb) 84236

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 104708 144 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 1048.54
Current children cumulated vsize (Kb) 84236

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20535 0 0 0 105708 144 0 0 25 0 1 0 1796366921 84082688 19567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20528 19567 145 145 0 20383 0
[pid=12907] vsize: 82112
Current children cumulated CPU time (s) 1058.54
Current children cumulated vsize (Kb) 84236

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20593 0 0 0 106707 145 0 0 25 0 1 0 1796366921 84320256 19625 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20586 19625 145 145 0 20441 0
[pid=12907] vsize: 82344
Current children cumulated CPU time (s) 1068.54
Current children cumulated vsize (Kb) 84468

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 20913 0 0 0 107701 147 0 0 25 0 1 0 1796366921 85630976 19945 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 20906 19945 145 145 0 20761 0
[pid=12907] vsize: 83624
Current children cumulated CPU time (s) 1078.5
Current children cumulated vsize (Kb) 85748

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 21294 0 0 0 108694 151 0 0 25 0 1 0 1796366921 87191552 20326 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 21287 20326 145 145 0 21142 0
[pid=12907] vsize: 85148
Current children cumulated CPU time (s) 1088.47
Current children cumulated vsize (Kb) 87272

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 21657 0 0 0 109687 154 0 0 25 0 1 0 1796366921 88686592 20689 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 21652 20689 145 145 0 21507 0
[pid=12907] vsize: 86608
Current children cumulated CPU time (s) 1098.43
Current children cumulated vsize (Kb) 88732

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 21999 0 0 0 110681 156 0 0 25 0 1 0 1796366921 90083328 21031 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12907/statm): 21993 21031 145 145 0 21848 0
[pid=12907] vsize: 87972
Current children cumulated CPU time (s) 1108.39
Current children cumulated vsize (Kb) 90096

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 22307 0 0 0 111675 158 0 0 25 0 1 0 1796366921 91353088 21339 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 22303 21339 145 145 0 22158 0
[pid=12907] vsize: 89212
Current children cumulated CPU time (s) 1118.35
Current children cumulated vsize (Kb) 91336

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 22600 0 0 0 112669 161 0 0 25 0 1 0 1796366921 92573696 21632 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 22601 21632 145 145 0 22456 0
[pid=12907] vsize: 90404
Current children cumulated CPU time (s) 1128.32
Current children cumulated vsize (Kb) 92528

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 22894 0 0 0 113664 163 0 0 25 0 1 0 1796366921 93814784 21926 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 22904 21926 145 145 0 22759 0
[pid=12907] vsize: 91616
Current children cumulated CPU time (s) 1138.29
Current children cumulated vsize (Kb) 93740

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 23188 0 0 0 114659 165 0 0 25 0 1 0 1796366921 95010816 22220 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 23196 22220 145 145 0 23051 0
[pid=12907] vsize: 92784
Current children cumulated CPU time (s) 1148.26
Current children cumulated vsize (Kb) 94908

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 23483 0 0 0 115653 168 0 0 25 0 1 0 1796366921 96256000 22515 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 23500 22515 145 145 0 23355 0
[pid=12907] vsize: 94000
Current children cumulated CPU time (s) 1158.23
Current children cumulated vsize (Kb) 96124

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 23752 0 0 0 116648 170 0 0 25 0 1 0 1796366921 97357824 22784 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 23769 22784 145 145 0 23624 0
[pid=12907] vsize: 95076
Current children cumulated CPU time (s) 1168.2
Current children cumulated vsize (Kb) 97200

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 23997 0 0 0 117643 171 0 0 25 0 1 0 1796366921 98369536 23029 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 24016 23029 145 145 0 23871 0
[pid=12907] vsize: 96064
Current children cumulated CPU time (s) 1178.16
Current children cumulated vsize (Kb) 98188

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 24202 0 0 0 118640 173 0 0 25 0 1 0 1796366921 99184640 23234 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 24215 23234 145 145 0 24070 0
[pid=12907] vsize: 96860
Current children cumulated CPU time (s) 1188.15
Current children cumulated vsize (Kb) 98984

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 24417 0 0 0 119636 175 0 0 25 0 1 0 1796366921 100077568 23449 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 24433 23449 145 145 0 24288 0
[pid=12907] vsize: 97732
Current children cumulated CPU time (s) 1198.13
Current children cumulated vsize (Kb) 99856

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 24630 0 0 0 120632 177 0 0 25 0 1 0 1796366921 100954112 23662 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 24647 23662 145 145 0 24502 0
[pid=12907] vsize: 98588
Current children cumulated CPU time (s) 1208.11
Current children cumulated vsize (Kb) 100712



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12907
Raw data (/proc/12903/stat): 12903 (minisat+_script) S 12902 12903 22582 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1796366916 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12903/statm): 531 226 485 147 0 384 0
[pid=12903] vsize: 2124
Raw data (/proc/12907/stat): 12907 (minisat+_64-bit) R 12903 12903 22582 0 -1 0 24630 0 0 0 120632 177 0 0 25 0 1 0 1796366921 100954112 23662 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12907/statm): 24647 23662 145 145 0 24502 0
[pid=12907] vsize: 98588
Current children cumulated CPU time (s) 1208.11
Current children cumulated vsize (Kb) 100712

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1208.16
CPU user time (s): 1206.34
CPU system time (s): 1.81972
CPU usage (%): 99.8342
Max. virtual memory (cumulated for all children) (Kb): 100712

Verifier Data

ERROR: no interpretation found !