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-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran12x21.opb
MD5SUM0d744fe957d41a18692933adc6be4af7
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1410122
Optimality of the best value was proved NO
Number of terms in the objective function 5292
Biggest coefficient in the objective function 5242880
Number of bits for the biggest coefficient in the objective function 23
Sum of the numbers in the objective function 1511880035
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 5242880
Number of bits of the biggest number in a constraint 23
Biggest sum of numbers in a constraint 1511880035
Number of bits of the biggest sum of numbers31
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1228.72
Number of variables5292
Total number of constraints285
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 constraints285
Minimum length of a constraint21
Maximum length of a constraint420

Trace number 6258

Launcher Data

LAUNCH ON wulflinc4 THE 2005-09-20 04:57:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3425 boxname=wulflinc4 idbench=1081 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0d744fe957d41a18692933adc6be4af7  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-ran12x21.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-ran12x21.opb
IDLAUNCH: 3425
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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		: 451.169
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:        863680 kB
Buffers:         33648 kB
Cached:         110724 kB
SwapCached:        876 kB
Active:          57512 kB
Inactive:        89448 kB
HighTotal:      131008 kB
HighFree:        22708 kB
LowTotal:       903652 kB
LowFree:        840972 kB
SwapTotal:     2097136 kB
SwapFree:      2095644 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5540 kB
Slab:            18352 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 05:17:49 (client local time) WITH STATUS 10 IN 1207.99 SECONDS
stats: 3425 7 1207.99 10

Solver Data

c Parsing PB file...
c Converting 318 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 316]---> Adder-cost: 428   maxlim: 44523   bits: 16/16
c ---[ 314]---> Adder-cost: 428   maxlim: 45163   bits: 16/16
c ---[ 312]---> Adder-cost: 434   maxlim: 55787   bits: 16/16
c ---[ 310]---> Adder-cost: 428   maxlim: 44395   bits: 16/16
c ---[ 308]---> Adder-cost: 428   maxlim: 43627   bits: 16/16
c ---[ 306]---> Adder-cost: 428   maxlim: 43755   bits: 16/16
c ---[ 304]---> Adder-cost: 428   maxlim: 44267   bits: 16/16
c ---[ 302]---> Adder-cost: 412   maxlim: 29419   bits: 15/15
c ---[ 300]---> Adder-cost: 428   maxlim: 44651   bits: 16/16
c ---[ 298]---> Adder-cost: 428   maxlim: 45035   bits: 16/16
c ---[ 296]---> Adder-cost: 434   maxlim: 51819   bits: 16/16
c ---[ 294]---> Adder-cost: 412   maxlim: 29547   bits: 15/15
c ---[ 292]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 290]---> Adder-cost: 242   maxlim: 23540   bits: 15/15
c ---[ 288]---> Adder-cost: 198   maxlim: 5748   bits: 13/13
c ---[ 286]---> Adder-cost: 262   maxlim: 42356   bits: 16/16
c ---[ 284]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 282]---> Adder-cost: 262   maxlim: 41332   bits: 16/16
c ---[ 280]---> Adder-cost: 220   maxlim: 11636   bits: 14/14
c ---[ 278]---> Adder-cost: 266   maxlim: 46836   bits: 16/16
c ---[ 276]---> Adder-cost: 242   maxlim: 23412   bits: 15/15
c ---[ 274]---> Adder-cost: 220   maxlim: 11380   bits: 14/14
c ---[ 272]---> Adder-cost: 262   maxlim: 41588   bits: 16/16
c ---[ 270]---> Adder-cost: 220   maxlim: 11380   bits: 14/14
c ---[ 268]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 266]---> Adder-cost: 262   maxlim: 41588   bits: 16/16
c ---[ 264]---> Adder-cost: 198   maxlim: 5748   bits: 13/13
c ---[ 262]---> Adder-cost: 262   maxlim: 42612   bits: 16/16
c ---[ 260]---> Adder-cost: 220   maxlim: 11636   bits: 14/14
c ---[ 258]---> Adder-cost: 242   maxlim: 22644   bits: 15/15
c ---[ 256]---> Adder-cost: 266   maxlim: 48372   bits: 16/16
c ---[ 254]---> Adder-cost: 266   maxlim: 49140   bits: 16/16
c ---[ 252]---> Adder-cost: 242   maxlim: 23412   bits: 15/15
c ---[ 251]---> BDD-cost:   10
c ---[ 250]---> BDD-cost:   12
c ---[ 249]---> BDD-cost:   11
c ---[ 248]---> BDD-cost:   15
c ---[ 247]---> BDD-cost:   13
c ---[ 246]---> BDD-cost:   16
c ---[ 245]---> BDD-cost:   13
c ---[ 244]---> BDD-cost:   16
c ---[ 243]---> BDD-cost:   10
c ---[ 242]---> BDD-cost:   12
c ---[ 241]---> BDD-cost:   10
c ---[ 240]---> BDD-cost:   11
c ---[ 239]---> BDD-cost:   14
c ---[ 238]---> BDD-cost:   17
c ---[ 237]---> BDD-cost:   13
c ---[ 236]---> BDD-cost:   14
c ---[ 235]---> BDD-cost:   14
c ---[ 234]---> BDD-cost:   14
c ---[ 233]---> BDD-cost:   15
c ---[ 232]---> BDD-cost:   11
c ---[ 231]---> BDD-cost:   14
c ---[ 230]---> BDD-cost:   10
c ---[ 229]---> BDD-cost:   14
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   10
c ---[ 226]---> BDD-cost:   14
c ---[ 225]---> BDD-cost:   15
c ---[ 224]---> BDD-cost:   13
c ---[ 223]---> BDD-cost:   14
c ---[ 222]---> BDD-cost:   13
c ---[ 221]---> BDD-cost:   14
c ---[ 220]---> BDD-cost:   10
c ---[ 219]---> BDD-cost:   12
c ---[ 218]---> BDD-cost:   10
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   14
c ---[ 215]---> BDD-cost:   17
c ---[ 214]---> BDD-cost:   13
c ---[ 213]---> BDD-cost:   15
c ---[ 212]---> BDD-cost:   17
c ---[ 211]---> BDD-cost:   17
c ---[ 210]---> BDD-cost:   15
c ---[ 209]---> BDD-cost:   11
c ---[ 208]---> BDD-cost:   17
c ---[ 207]---> BDD-cost:   10
c ---[ 206]---> BDD-cost:   17
c ---[ 205]---> BDD-cost:   13
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   17
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   13
c ---[ 200]---> BDD-cost:   17
c ---[ 199]---> BDD-cost:   13
c ---[ 198]---> BDD-cost:   17
c ---[ 197]---> BDD-cost:   10
c ---[ 196]---> BDD-cost:   12
c ---[ 195]---> BDD-cost:   10
c ---[ 194]---> BDD-cost:   14
c ---[ 193]---> BDD-cost:   11
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   13
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   15
c ---[ 187]---> BDD-cost:   15
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   15
c ---[ 184]---> BDD-cost:   10
c ---[ 183]---> BDD-cost:   15
c ---[ 182]---> BDD-cost:   15
c ---[ 181]---> BDD-cost:   13
c ---[ 180]---> BDD-cost:   15
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   13
c ---[ 177]---> BDD-cost:   15
c ---[ 176]---> BDD-cost:   13
c ---[ 175]---> BDD-cost:   15
c ---[ 174]---> BDD-cost:   10
c ---[ 173]---> BDD-cost:   12
c ---[ 172]---> BDD-cost:   13
c ---[ 171]---> BDD-cost:   10
c ---[ 170]---> BDD-cost:   11
c ---[ 169]---> BDD-cost:   17
c ---[ 168]---> BDD-cost:   13
c ---[ 167]---> BDD-cost:   15
c ---[ 166]---> BDD-cost:   18
c ---[ 165]---> BDD-cost:   14
c ---[ 164]---> BDD-cost:   15
c ---[ 163]---> BDD-cost:   11
c ---[ 162]---> BDD-cost:   17
c ---[ 161]---> BDD-cost:   14
c ---[ 160]---> BDD-cost:   10
c ---[ 159]---> BDD-cost:   17
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   18
c ---[ 156]---> BDD-cost:   15
c ---[ 155]---> BDD-cost:   13
c ---[ 154]---> BDD-cost:   17
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   17
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:   13
c ---[ 149]---> BDD-cost:   12
c ---[ 148]---> BDD-cost:   10
c ---[ 147]---> BDD-cost:   11
c ---[ 146]---> BDD-cost:   15
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   15
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   15
c ---[ 141]---> BDD-cost:   15
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:   10
c ---[ 138]---> BDD-cost:   14
c ---[ 137]---> BDD-cost:   15
c ---[ 136]---> BDD-cost:   10
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   15
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   15
c ---[ 127]---> BDD-cost:   10
c ---[ 126]---> BDD-cost:   10
c ---[ 125]---> BDD-cost:   12
c ---[ 124]---> BDD-cost:   10
c ---[ 123]---> BDD-cost:   11
c ---[ 122]---> BDD-cost:   17
c ---[ 121]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   14
c ---[ 118]---> BDD-cost:   14
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   12
c ---[ 115]---> BDD-cost:   11
c ---[ 114]---> BDD-cost:   17
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:   17
c ---[ 111]---> BDD-cost:   13
c ---[ 110]---> BDD-cost:   14
c ---[ 109]---> BDD-cost:   15
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   17
c ---[ 106]---> BDD-cost:   13
c ---[ 105]---> BDD-cost:   10
c ---[ 104]---> BDD-cost:   17
c ---[ 103]---> BDD-cost:   10
c ---[ 102]---> BDD-cost:   12
c ---[ 101]---> BDD-cost:   10
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   17
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   17
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   15
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   17
c ---[  90]---> BDD-cost:   10
c ---[  89]---> BDD-cost:   17
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   17
c ---[  86]---> BDD-cost:   15
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   17
c ---[  80]---> BDD-cost:   13
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   17
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   11
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   13
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   13
c ---[  63]---> BDD-cost:   17
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   12
c ---[  60]---> BDD-cost:   10
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   17
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   15
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   17
c ---[  52]---> BDD-cost:   15
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   10
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   13
c ---[  43]---> BDD-cost:   15
c ---[  42]---> BDD-cost:   17
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   17
c ---[  39]---> BDD-cost:   10
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   14
c ---[  31]---> BDD-cost:   16
c ---[  30]---> BDD-cost:   16
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   17
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   16
c ---[  22]---> BDD-cost:   15
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   17
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   71899   250207 |   23966       0        0     nan |  0.000 % |
c |       100 |   71775   249789 |   26362      90      285     3.2 | 21.316 % |
c |       250 |   71661   249395 |   28998     222      730     3.3 | 21.427 % |
c |       475 |   71389   248441 |   31898     415     1374     3.3 | 21.702 % |
c |       812 |   71264   248026 |   35088     735     2410     3.3 | 21.825 % |
c |      1318 |   71004   247136 |   38597    1202     3888     3.2 | 22.088 % |
c |      2077 |   70497   245373 |   42457    1895     6183     3.3 | 22.586 % |
c |      3216 |   70137   244145 |   46702    2980    10121     3.4 | 22.949 % |
c |      4925 |   69876   243270 |   51373    4655    17540     3.8 | 23.212 % |
c |      7487 |   69792   242992 |   56510    7205    34484     4.8 | 23.300 % |
c |     11331 |   69708   242704 |   62161   11037    63037     5.7 | 23.388 % |
c |     17098 |   69601   242349 |   68377   16789   106394     6.3 | 23.505 % |
c |     25748 |   69551   242177 |   75215   25433   223628     8.8 | 23.551 % |
c |     38722 |   69475   241927 |   82737   38397   380709     9.9 | 23.633 % |
c |     58183 |   69343   241469 |   91010   57843  1285226    22.2 | 23.774 % |
c |     87375 |   69164   240876 |  100111   87009  2085575    24.0 | 23.967 % |
c |    131164 |   69034   240442 |  110123   45548  1563875    34.3 | 24.113 % |
c |    196848 |   68908   240028 |  121135  111213  5777081    51.9 | 24.254 % |
c |    295374 |   68811   239711 |  133248  107600 10096080    93.8 | 24.359 % |
c ==============================================================================
c Found solution: 5164114
c ---[   0]---> Adder-cost: 10758   maxlim: 3198225   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    427438 |  143942   508081 |   47980  119798  4552772    38.0 | 24.359 % |
c |    427538 |  143942   508081 |   52778   24290   324994    13.4 | 15.026 % |
c |    427688 |  143942   508081 |   58055   24440   325740    13.3 | 15.026 % |
c |    427913 |  143942   508081 |   63861   24665   326932    13.3 | 15.026 % |
c |    428250 |  143942   508081 |   70247   25002   328801    13.2 | 15.026 % |
c |    428756 |  143942   508081 |   77272   25508   331681    13.0 | 15.026 % |
c |    429516 |  143942   508081 |   84999   26268   336986    12.8 | 15.026 % |
c |    430655 |  143942   508081 |   93499   27407   347060    12.7 | 15.026 % |
c |    432363 |  143942   508081 |  102849   29115   361638    12.4 | 15.026 % |
c |    434925 |  143942   508081 |  113134   31677   383141    12.1 | 15.026 % |
c |    438769 |  143942   508081 |  124447   35521   424339    11.9 | 15.026 % |
c |    444535 |  143942   508081 |  136892   41287   504502    12.2 | 15.026 % |
c |    453184 |  143942   508081 |  150581   49936   608101    12.2 | 15.026 % |
c |    466158 |  143933   508052 |  165639   62909   799784    12.7 | 15.033 % |
c ==============================================================================
c Found solution: 4993470
c ---[   0]---> Adder-cost: 0   maxlim: 3368869   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    476252 |  143940   508206 |   47980   72998   976904    13.4 | 15.033 % |
c |    476352 |  143940   508206 |   52778   24029   244358    10.2 | 15.081 % |
c |    476502 |  143940   508206 |   58055   24179   245061    10.1 | 15.081 % |
c |    476727 |  143924   508154 |   63861   24402   246268    10.1 | 15.092 % |
c |    477064 |  143924   508154 |   70247   24739   248093    10.0 | 15.092 % |
c |    477570 |  143924   508154 |   77272   25245   251148     9.9 | 15.092 % |
c |    478329 |  143924   508154 |   84999   26004   255844     9.8 | 15.092 % |
c |    479468 |  143924   508154 |   93499   27143   263557     9.7 | 15.092 % |
c |    481176 |  143924   508154 |  102849   28851   277168     9.6 | 15.092 % |
c |    483738 |  143924   508154 |  113134   31413   298331     9.5 | 15.092 % |
c |    487582 |  143924   508154 |  124447   35257   338015     9.6 | 15.092 % |
c |    493348 |  143924   508154 |  136892   41023   411370    10.0 | 15.092 % |
c |    501998 |  143924   508154 |  150581   49673   636684    12.8 | 15.092 % |
c |    514973 |  143924   508154 |  165639   62648  1548001    24.7 | 15.092 % |
c |    534435 |  143860   507938 |  182203   82102  2556226    31.1 | 15.135 % |
c ==============================================================================
c Found solution: 4969533
c ---[   0]---> Adder-cost: 0   maxlim: 3392806   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    548957 |  143830   507947 |   47943   96618  2800047    29.0 | 15.135 % |
c |    549057 |  143830   507947 |   52737   25841   259182    10.0 | 15.189 % |
c |    549207 |  143830   507947 |   58011   25991   259927    10.0 | 15.189 % |
c |    549432 |  143821   507918 |   63812   26215   260957    10.0 | 15.196 % |
c |    549769 |  143821   507918 |   70193   26552   264038     9.9 | 15.196 % |
c |    550275 |  143821   507918 |   77212   27058   267170     9.9 | 15.196 % |
c |    551035 |  143812   507889 |   84933   27817   271481     9.8 | 15.203 % |
c |    552174 |  143812   507889 |   93427   28956   278220     9.6 | 15.203 % |
c |    553882 |  143812   507889 |  102770   30664   290985     9.5 | 15.203 % |
c |    556444 |  143812   507889 |  113047   33226   313156     9.4 | 15.203 % |
c |    560288 |  143812   507889 |  124351   37070   349921     9.4 | 15.203 % |
c |    566054 |  143806   507869 |  136786   42835   412129     9.6 | 15.207 % |
c |    574703 |  143806   507869 |  150465   51484   506204     9.8 | 15.207 % |
c |    587677 |  143806   507869 |  165512   64458   684691    10.6 | 15.207 % |
c |    607139 |  143806   507869 |  182063   83920  1024750    12.2 | 15.207 % |
c ==============================================================================
c Found solution: 4948528
c ---[   0]---> Adder-cost: 0   maxlim: 3413811   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    619345 |  143802   507952 |   47934   96122  1210531    12.6 | 15.207 % |
c |    619445 |  143802   507952 |   52727   28426   249561     8.8 | 15.244 % |
c |    619596 |  143802   507952 |   58000   28577   250180     8.8 | 15.244 % |
c |    619821 |  143802   507952 |   63800   28802   251367     8.7 | 15.244 % |
c |    620158 |  143802   507952 |   70180   29139   254413     8.7 | 15.244 % |
c |    620664 |  143793   507921 |   77198   29644   257915     8.7 | 15.247 % |
c |    621423 |  143793   507921 |   84918   30403   263542     8.7 | 15.247 % |
c |    622562 |  143793   507921 |   93409   31542   270551     8.6 | 15.247 % |
c |    624270 |  143793   507921 |  102750   33250   287436     8.6 | 15.247 % |
c |    626832 |  143793   507921 |  113025   35812   307607     8.6 | 15.247 % |
c |    630676 |  143793   507921 |  124328   39656   343499     8.7 | 15.247 % |
c |    636443 |  143793   507921 |  136761   45423   403695     8.9 | 15.247 % |
c |    645093 |  143793   507921 |  150437   54073   506666     9.4 | 15.247 % |
c |    658067 |  143793   507921 |  165481   67047   772495    11.5 | 15.247 % |
c |    677528 |  143781   507881 |  182029   86504  1175225    13.6 | 15.254 % |
c |    706720 |  143781   507881 |  200232  115696  1691943    14.6 | 15.254 % |
c |    750510 |  143775   507861 |  220255  159485  2508041    15.7 | 15.258 % |
c |    816194 |  143748   507768 |  242280  225165  9373381    41.6 | 15.272 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -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 -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 -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 -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 -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 -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 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 -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 -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 -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 -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 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 -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 -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 -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 -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 -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 -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 -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 -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 -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 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 -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 -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 -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 -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 -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 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 -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 -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 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 -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 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 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 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 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 -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 -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 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 -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 -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 -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 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 -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 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 -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 -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 -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 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 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 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 -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 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 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 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 -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 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 -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 -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 -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 -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 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 -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 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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 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 -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 -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 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 -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 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 -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 -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 -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 -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 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 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 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 -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 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 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 -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 -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 -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 -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 -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 -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 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 -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 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 -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 -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 -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 -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 -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 -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 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 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 -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 -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 -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 -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 -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 -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 -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 -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 -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 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 -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 -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 -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 -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 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 -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 -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 -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 -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 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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -X169_bit_7 X169_bit_6 X169_bit_5 -X169_bit_4 X169_bit_3 X169_bit_2 -X169_bit_1 -X169_bit0 -X169_bit1 X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 -X170_bit_7 -X170_bit_6 X170_bit_5 -X170_bit_4 -X170_bit_3 -X170_bit_2 -X170_bit_1 -X170_bit0 -X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 -X171_bit_7 -X171_bit_6 -X171_bit_5 -X171_bit_4 -X171_bit_3 X171_bit_2 -X171_bit_1 X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 -X172_bit_6 -X172_bit_5 -X172_bit_4 -X172_bit_3 X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 -X172_bit2 X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 -X173_bit_7 -X173_bit_6 -X173_bit_5 X173_bit_4 -X173_bit_3 -X173_bit_2 -X173_bit_1 -X173_bit0 -X173_bit1 -X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 X174_bit_7 X174_bit_6 X174_bit_5 -X174_bit_4 -X174_bit_3 X174_bit_2 X174_bit_1 -X174_bit0 -X174_bit1 X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 X175_bit_7 -X175_bit_6 -X175_bit_5 -X175_bit_4 -X175_bit_3 -X175_bit_2 X175_bit_1 -X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 -X176_bit_7 X176_bit_6 -X176_bit_5 -X176_bit_4 -X176_bit_3 X176_bit_2 X176_bit_1 -X176_bit0 -X176_bit1 X176_bit2 X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 -X177_bit_7 -X177_bit_6 X177_bit_5 -X177_bit_4 -X177_bit_3 -X177_bit_2 -X177_bit_1 -X177_bit0 X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 -X178_bit_7 -X178_bit_6 -X178_bit_5 -X178_bit_4 X178_bit_3 X178_bit_2 X178_bit_1 -X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 X179_bit_7 X179_bit_6 X179_bit_5 -X179_bit_4 -X179_bit_3 X179_bit_2 -X179_bit_1 -X179_bit0 -X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 -X180_bit_7 X180_bit_6 -X180_bit_5 -X180_bit_4 -X180_bit_3 -X180_bit_2 X180_bit_1 -X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 -X181_bit_7 -X181_bit_6 -X181_bit_5 -X181_bit_4 -X181_bit_3 -X181_bit_2 X181_bit_1 -X181_bit0 -X181_bit1 X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 -X182_bit_7 -X182_bit_6 -X182_bit_5 -X182_bit_4 -X182_bit_3 -X182_bit_2 X182_bit_1 -X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 -X183_bit_7 X183_bit_6 -X183_bit_5 X183_bit_4 -X183_bit_3 -X183_bit_2 X183_bit_1 -X183_bit0 -X183_bit1 -X183_bit2 -X183_bit3 X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 -X184_bit_7 -X184_bit_6 -X184_bit_5 -X184_bit_4 -X184_bit_3 -X184_bit_2 -X184_bit_1 -X184_bit0 -X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 -X185_bit_7 X185_bit_6 -X185_bit_5 X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 X186_bit_7 -X186_bit_6 -X186_bit_5 -X186_bit_4 -X186_bit_3 X186_bit_2 -X186_bit_1 X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 -X187_bit_7 -X187_bit_6 -X187_bit_5 -X187_bit_4 -X187_bit_3 X187_bit_2 X187_bit_1 X187_bit0 -X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 -X188_bit_7 -X188_bit_6 -X188_bit_5 -X188_bit_4 -X188_bit_3 -X188_bit_2 X188_bit_1 X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 X189_bit_7 X189_bit_6 X189_bit_5 -X189_bit_4 -X189_bit_3 X189_bit_2 -X189_bit_1 -X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -X190_bit_7 X190_bit_6 X190_bit_5 -X190_bit_4 X190_bit_3 X190_bit_2 -X190_bit_1 -X190_bit0 -X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 X191_bit_7 -X191_bit_6 -X191_bit_5 -X191_bit_4 -X191_bit_3 -X191_bit_2 X191_bit_1 -X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 -X192_bit_7 X192_bit_6 X192_bit_5 X192_bit_4 X192_bit_3 -X192_bit_2 -X192_bit_1 -X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 X193_bit_6 X193_bit_5 -X193_bit_4 -X193_bit_3 -X193_bit_2 -X193_bit_1 X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 -X194_bit_7 X194_bit_6 -X194_bit_5 X194_bit_4 -X194_bit_3 -X194_bit_2 -X194_bit_1 X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 X195_bit_7 X195_bit_6 X195_bit_5 X195_bit_4 X195_bit_3 X195_bit_2 -X195_bit_1 -X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 X196_bit_7 -X196_bit_6 X196_bit_5 -X196_bit_4 -X196_bit_3 X196_bit_2 X196_bit_1 X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 -X197_bit_7 -X197_bit_6 X197_bit_5 X197_bit_4 X197_bit_3 -X197_bit_2 -X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 X198_bit_7 X198_bit_6 -X198_bit_5 -X198_bit_4 -X198_bit_3 -X198_bit_2 -X198_bit_1 -X198_bit0 -X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 X199_bit_7 -X199_bit_6 -X199_bit_5 -X199_bit_4 -X199_bit_3 -X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 X200_bit_7 X200_bit_6 -X200_bit_5 -X200_bit_4 -X200_bit_3 -X200_bit_2 -X200_bit_1 -X200_bit0 -X200_bit1 -X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 -X201_bit_7 X201_bit_6 X201_bit_5 -X201_bit_4 -X201_bit_3 -X201_bit_2 X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 X202_bit_7 -X202_bit_6 -X202_bit_5 -X202_bit_4 -X202_bit_3 -X202_bit_2 -X202_bit_1 -X202_bit0 -X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 X203_bit_7 -X203_bit_6 X203_bit_5 -X203_bit_4 X203_bit_3 X203_bit_2 -X203_bit_1 -X203_bit0 -X203_bit1 -X203_bit2 -X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 -X204_bit_6 X204_bit_5 X204_bit_4 -X204_bit_3 X204_bit_2 -X204_bit_1 -X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 -X205_bit_7 X205_bit_6 X205_bit_5 -X205_bit_4 X205_bit_3 X205_bit_2 X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 -X206_bit_7 X206_bit_6 X206_bit_5 -X206_bit_4 X206_bit_3 X206_bit_2 -X206_bit_1 -X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 X207_bit_7 X207_bit_6 -X207_bit_5 X207_bit_4 -X207_bit_3 X207_bit_2 -X207_bit_1 X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 -X208_bit_7 -X208_bit_6 X208_bit_5 X208_bit_4 -X208_bit_3 X208_bit_2 X208_bit_1 -X208_bit0 -X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 -X209_bit_7 X209_bit_6 -X209_bit_5 -X209_bit_4 -X209_bit_3 -X209_bit_2 -X209_bit_1 -X209_bit0 X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 -X210_bit_7 -X210_bit_6 X210_bit_5 -X210_bit_4 X210_bit_3 -X210_bit_2 -X210_bit_1 -X210_bit0 -X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 X211_bit_7 X211_bit_6 -X211_bit_5 -X211_bit_4 X211_bit_3 -X211_bit_2 -X211_bit_1 -X211_bit0 -X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 X212_bit_7 -X212_bit_6 -X212_bit_5 -X212_bit_4 -X212_bit_3 -X212_bit_2 X212_bit_1 -X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 -X213_bit_7 -X213_bit_6 X213_bit_5 -X213_bit_4 X213_bit_3 -X213_bit_2 -X213_bit_1 -X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 X214_bit_7 -X214_bit_6 X214_bit_5 -X214_bit_4 X214_bit_3 -X214_bit_2 -X214_bit_1 X214_bit0 -X214_bit1 -X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 -X215_bit_7 X215_bit_6 -X215_bit_5 -X215_bit_4 -X215_bit_3 X215_bit_2 -X215_bit_1 -X215_bit0 -X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 X216_bit_7 X216_bit_6 X216_bit_5 -X216_bit_4 X216_bit_3 -X216_bit_2 -X216_bit_1 -X216_bit0 -X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 X217_bit_7 -X217_bit_6 X217_bit_5 X217_bit_4 -X217_bit_3 -X217_bit_2 -X217_bit_1 X217_bit0 -X217_bit1 -X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 X218_bit_7 X218_bit_6 X218_bit_5 X218_bit_4 X218_bit_3 X218_bit_2 -X218_bit_1 -X218_bit0 X218_bit1 -X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 -X219_bit_7 -X219_bit_6 X219_bit_5 -X219_bit_4 -X219_bit_3 -X219_bit_2 -X219_bit_1 -X219_bit0 -X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 X220_bit_7 -X220_bit_6 -X220_bit_5 X220_bit_4 -X220_bit_3 -X220_bit_2 -X220_bit_1 -X220_bit0 -X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 X221_bit_7 -X221_bit_6 -X221_bit_5 X221_bit_4 -X221_bit_3 -X221_bit_2 -X221_bit_1 -X221_bit0 X221_bit1 -X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 X222_bit_7 -X222_bit_6 -X222_bit_5 X222_bit_4 -X222_bit_3 -X222_bit_2 X222_bit_1 -X222_bit0 -X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 -X223_bit_6 -X223_bit_5 -X223_bit_4 -X223_bit_3 -X223_bit_2 -X223_bit_1 -X223_bit0 -X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 -X224_bit_7 -X224_bit_6 -X224_bit_5 -X224_bit_4 -X224_bit_3 -X224_bit_2 X224_bit_1 -X224_bit0 -X224_bit1 -X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 -X225_bit_7 -X225_bit_6 X225_bit_5 -X225_bit_4 -X225_bit_3 -X225_bit_2 -X225_bit_1 X225_bit0 -X225_bit1 X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 -X226_bit_7 X226_bit_6 -X226_bit_5 X226_bit_4 X226_bit_3 X226_bit_2 -X226_bit_1 -X226_bit0 -X226_bit1 -X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 -X227_bit_7 -X227_bit_6 -X227_bit_5 -X227_bit_4 X227_bit_3 X227_bit_2 -X227_bit_1 X227_bit0 -X227_bit1 -X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 X228_bit_7 -X228_bit_6 -X228_bit_5 -X228_bit_4 X228_bit_3 X228_bit_2 -X228_bit_1 X228_bit0 X228_bit1 X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 X229_bit_7 X229_bit_6 X229_bit_5 -X229_bit_4 -X229_bit_3 X229_bit_2 X229_bit_1 -X229_bit0 -X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 X230_bit_7 -X230_bit_6 X230_bit_5 -X230_bit_4 -X230_bit_3 -X230_bit_2 X230_bit_1 X230_bit0 X230_bit1 X230_bit2 -X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 -X231_bit_7 X231_bit_6 X231_bit_5 -X231_bit_4 X231_bit_3 X231_bit_2 -X231_bit_1 -X231_bit0 -X231_bit1 -X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 X232_bit_7 X232_bit_6 -X232_bit_5 -X232_bit_4 X232_bit_3 -X232_bit_2 -X232_bit_1 -X232_bit0 -X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 X233_bit_7 X233_bit_6 X233_bit_5 X233_bit_4 -X233_bit_3 -X233_bit_2 -X233_bit_1 -X233_bit0 -X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 -X234_bit_7 X234_bit_6 X234_bit_5 X234_bit_4 -X234_bit_3 X234_bit_2 -X234_bit_1 -X234_bit0 -X234_bit1 -X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 X235_bit_7 -X235_bit_6 X235_bit_5 -X235_bit_4 X235_bit_3 -X235_bit_2 -X235_bit_1 -X235_bit0 -X235_bit1 -X235_bit2 -X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 -X236_bit_7 X236_bit_6 -X236_bit_5 -X236_bit_4 -X236_bit_3 X236_bit_2 -X236_bit_1 X236_bit0 -X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 X237_bit_7 X237_bit_6 X237_bit_5 X237_bit_4 -X237_bit_3 X237_bit_2 -X237_bit_1 -X237_bit0 -X237_bit1 -X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 X238_bit_7 -X238_bit_6 -X238_bit_5 X238_bit_4 -X238_bit_3 X238_bit_2 X238_bit_1 -X238_bit0 -X238_bit1 -X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 -X239_bit_6 -X239_bit_5 -X239_bit_4 -X239_bit_3 -X239_bit_2 -X239_bit_1 -X239_bit0 X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 X240_bit_7 X240_bit_6 X240_bit_5 -X240_bit_4 -X240_bit_3 -X240_bit_2 -X240_bit_1 -X240_bit0 -X240_bit1 -X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 X241_bit_7 X241_bit_6 -X241_bit_5 X241_bit_4 -X241_bit_3 -X241_bit_2 -X241_bit_1 -X241_bit0 -X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 X242_bit_7 X242_bit_6 -X242_bit_5 X242_bit_4 -X242_bit_3 -X242_bit_2 -X242_bit_1 -X242_bit0 X242_bit1 -X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 X243_bit_7 X243_bit_6 -X243_bit_5 -X243_bit_4 -X243_bit_3 -X243_bit_2 -X243_bit_1 -X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 -X244_bit_7 -X244_bit_6 X244_bit_5 -X244_bit_4 -X244_bit_3 X244_bit_2 X244_bit_1 -X244_bit0 X244_bit1 -X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 X245_bit_7 X245_bit_6 X245_bit_5 -X245_bit_4 X245_bit_3 X245_bit_2 X245_bit_1 -X245_bit0 -X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 -X246_bit_7 X246_bit_6 X246_bit_5 X246_bit_4 -X246_bit_3 -X246_bit_2 -X246_bit_1 -X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 -X247_bit_7 X247_bit_6 -X247_bit_5 X247_bit_4 X247_bit_3 X247_bit_2 X247_bit_1 -X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 X248_bit_7 X248_bit_6 X248_bit_5 -X248_bit_4 -X248_bit_3 -X248_bit_2 -X248_bit_1 -X248_bit0 -X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 X249_bit_7 X249_bit_6 X249_bit_5 X249_bit_4 -X249_bit_3 -X249_bit_2 X249_bit_1 -X249_bit0 X249_bit1 X249_bit2 -X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 X250_bit_7 X250_bit_6 -X250_bit_5 X250_bit_4 -X250_bit_3 -X250_bit_2 -X250_bit_1 -X250_bit0 -X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 X251_bit_7 X251_bit_6 X251_bit_5 -X251_bit_4 -X251_bit_3 -X251_bit_2 X251_bit_1 X251_bit0 -X251_bit1 X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 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 Y164_bit0 Y165_bit0 Y166_bit0 Y167_bit0 Y168_bit0 Y169_bit0 Y170_bit0 Y171_bit0 Y172_bit0 Y173_bit0 Y174_bit0 Y175_bit0 Y176_bit0 Y177_bit0 Y178_bit0 Y179_bit0 Y180_bit0 Y181_bit0 Y182_bit0 Y183_bit0 -Y184_bit0 Y185_bit0 Y186_bit0 Y187_bit0 Y188_bit0 Y189_bit0 Y190_bit0 Y191_bit0 Y192_bit0 Y193_bit0 Y194_bit0 Y195_bit0 Y196_bit0 Y197_bit0 Y198_bit0 Y199_bit0 Y200_bit0 Y201_bit0 Y202_bit0 Y203_bit0 Y204_bit0 Y205_bit0 Y206_bit0 Y207_bit0 Y208_bit0 Y209_bit0 Y210_bit0 Y211_bit0 Y212_bit0 Y213_bit0 Y214_bit0 Y215_bit0 Y216_bit0 Y217_bit0 Y218_bit0 Y219_bit0 Y220_bit0 Y221_bit0 Y222_bit0 -Y223_

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/9516/stat): 9516 (minisat+_script) R 9515 9516 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797591455 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/9516/statm): 174 3 169 147 0 27 0
[pid=9516] 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=9517
New process pid=9518
New process pid=9519
execve syscall for /bin/sed executable
One traced child (pid=9518) 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=9519) exited with status: 0
One traced child (pid=9517) exited with status: 0
New process pid=9520
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-ran12x21.opb

[startup+10.0044 s]
Raw data (loadavg): 0.96 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 1771 0 0 0 980 8 0 0 25 0 1 0 1797591460 8667136 1751 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 2116 1751 145 145 0 1971 0
[pid=9520] vsize: 8464
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 10588

[startup+20.0062 s]
Raw data (loadavg): 0.97 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 1850 0 0 0 1978 8 0 0 25 0 1 0 1797591460 9019392 1830 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 2202 1830 145 145 0 2057 0
[pid=9520] vsize: 8808
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 10932

[startup+30.0071 s]
Raw data (loadavg): 0.97 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 2010 0 0 0 2975 9 0 0 25 0 1 0 1797591460 9707520 1990 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 2370 1990 145 145 0 2225 0
[pid=9520] vsize: 9480
Current children cumulated CPU time (s) 29.84
Current children cumulated vsize (Kb) 11604

[startup+40.008 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 2300 0 0 0 3970 12 0 0 25 0 1 0 1797591460 10850304 2280 4294967295 134512640 135094434 3221224432 3221223152 134558439 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 2649 2280 145 145 0 2504 0
[pid=9520] vsize: 10596
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 12720

[startup+50.0088 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 2620 0 0 0 4965 13 0 0 25 0 1 0 1797591460 12242944 2600 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 2989 2600 145 145 0 2844 0
[pid=9520] vsize: 11956
Current children cumulated CPU time (s) 49.78
Current children cumulated vsize (Kb) 14080

[startup+60.0097 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 3653 0 0 0 5950 20 0 0 25 0 1 0 1797591460 16412672 3633 4294967295 134512640 135094434 3221224432 3221223072 134562149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 4007 3633 145 145 0 3862 0
[pid=9520] vsize: 16028
Current children cumulated CPU time (s) 59.7
Current children cumulated vsize (Kb) 18152

[startup+70.0125 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 4143 0 0 0 6941 24 0 0 25 0 1 0 1797591460 18632704 4123 4294967295 134512640 135094434 3221224432 3221223060 134562984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 4549 4123 145 145 0 4404 0
[pid=9520] vsize: 18196
Current children cumulated CPU time (s) 69.65
Current children cumulated vsize (Kb) 20320

[startup+80.0134 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 4612 0 0 0 7933 28 0 0 25 0 1 0 1797591460 20516864 4592 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 5009 4592 145 145 0 4864 0
[pid=9520] vsize: 20036
Current children cumulated CPU time (s) 79.61
Current children cumulated vsize (Kb) 22160

[startup+90.0143 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 4809 0 0 0 8927 29 0 0 25 0 1 0 1797591460 21295104 4789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 5199 4789 145 145 0 5054 0
[pid=9520] vsize: 20796
Current children cumulated CPU time (s) 89.56
Current children cumulated vsize (Kb) 22920

[startup+100.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 4968 0 0 0 9924 31 0 0 25 0 1 0 1797591460 21917696 4948 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 5351 4948 145 145 0 5206 0
[pid=9520] vsize: 21404
Current children cumulated CPU time (s) 99.55
Current children cumulated vsize (Kb) 23528

[startup+110.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 5270 0 0 0 10919 33 0 0 25 0 1 0 1797591460 23121920 5250 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 5645 5250 145 145 0 5500 0
[pid=9520] vsize: 22580
Current children cumulated CPU time (s) 109.52
Current children cumulated vsize (Kb) 24704

[startup+120.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 5581 0 0 0 11915 34 0 0 25 0 1 0 1797591460 24371200 5561 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 5950 5561 145 145 0 5805 0
[pid=9520] vsize: 23800
Current children cumulated CPU time (s) 119.49
Current children cumulated vsize (Kb) 25924

[startup+130.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 5581 0 0 0 12916 34 0 0 25 0 1 0 1797591460 24371200 5561 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 5950 5561 145 145 0 5805 0
[pid=9520] vsize: 23800
Current children cumulated CPU time (s) 129.5
Current children cumulated vsize (Kb) 25924

[startup+140.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 5581 0 0 0 13915 35 0 0 25 0 1 0 1797591460 24371200 5561 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 5950 5561 145 145 0 5805 0
[pid=9520] vsize: 23800
Current children cumulated CPU time (s) 139.5
Current children cumulated vsize (Kb) 25924

[startup+150.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 5581 0 0 0 14916 35 0 0 25 0 1 0 1797591460 24371200 5561 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 5950 5561 145 145 0 5805 0
[pid=9520] vsize: 23800
Current children cumulated CPU time (s) 149.51
Current children cumulated vsize (Kb) 25924

[startup+160.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 5581 0 0 0 15916 35 0 0 25 0 1 0 1797591460 24371200 5561 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 5950 5561 145 145 0 5805 0
[pid=9520] vsize: 23800
Current children cumulated CPU time (s) 159.51
Current children cumulated vsize (Kb) 25924

[startup+170.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 5581 0 0 0 16916 35 0 0 25 0 1 0 1797591460 24371200 5561 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 5950 5561 145 145 0 5805 0
[pid=9520] vsize: 23800
Current children cumulated CPU time (s) 169.51
Current children cumulated vsize (Kb) 25924

[startup+180.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) T 9516 9516 6847 0 -1 0 6468 0 0 0 17903 40 0 0 25 0 1 0 1797591460 28012544 6448 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9520/statm): 6839 6448 145 145 0 6694 0
[pid=9520] vsize: 27356
Current children cumulated CPU time (s) 179.43
Current children cumulated vsize (Kb) 29480

[startup+190.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 7990 0 0 0 18880 49 0 0 25 0 1 0 1797591460 34254848 7970 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 8363 7970 145 145 0 8218 0
[pid=9520] vsize: 33452
Current children cumulated CPU time (s) 189.29
Current children cumulated vsize (Kb) 35576

[startup+200.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 9054 0 0 0 19865 55 0 0 25 0 1 0 1797591460 38600704 9034 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 9424 9034 145 145 0 9279 0
[pid=9520] vsize: 37696
Current children cumulated CPU time (s) 199.2
Current children cumulated vsize (Kb) 39820

[startup+210.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 9236 0 0 0 20861 57 0 0 25 0 1 0 1797591460 39321600 9216 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 9600 9216 145 145 0 9455 0
[pid=9520] vsize: 38400
Current children cumulated CPU time (s) 209.18
Current children cumulated vsize (Kb) 40524

[startup+220.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 9384 0 0 0 21858 57 0 0 25 0 1 0 1797591460 39903232 9364 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 9742 9364 145 145 0 9597 0
[pid=9520] vsize: 38968
Current children cumulated CPU time (s) 219.15
Current children cumulated vsize (Kb) 41092

[startup+230.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 9519 0 0 0 22856 59 0 0 25 0 1 0 1797591460 40443904 9499 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 9874 9499 145 145 0 9729 0
[pid=9520] vsize: 39496
Current children cumulated CPU time (s) 229.15
Current children cumulated vsize (Kb) 41620

[startup+240.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 9519 0 0 0 23856 59 0 0 25 0 1 0 1797591460 40443904 9499 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 9874 9499 145 145 0 9729 0
[pid=9520] vsize: 39496
Current children cumulated CPU time (s) 239.15
Current children cumulated vsize (Kb) 41620

[startup+250.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 9519 0 0 0 24856 59 0 0 25 0 1 0 1797591460 40443904 9499 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 9874 9499 145 145 0 9729 0
[pid=9520] vsize: 39496
Current children cumulated CPU time (s) 249.15
Current children cumulated vsize (Kb) 41620

[startup+260.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 9519 0 0 0 25856 59 0 0 25 0 1 0 1797591460 40443904 9499 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 9874 9499 145 145 0 9729 0
[pid=9520] vsize: 39496
Current children cumulated CPU time (s) 259.15
Current children cumulated vsize (Kb) 41620

[startup+270.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 9519 0 0 0 26856 59 0 0 25 0 1 0 1797591460 40443904 9499 4294967295 134512640 135094434 3221224432 3221223104 134555563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 9874 9499 145 145 0 9729 0
[pid=9520] vsize: 39496
Current children cumulated CPU time (s) 269.15
Current children cumulated vsize (Kb) 41620

[startup+280.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 9762 0 0 0 27852 60 0 0 25 0 1 0 1797591460 41439232 9742 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 10117 9742 145 145 0 9972 0
[pid=9520] vsize: 40468
Current children cumulated CPU time (s) 279.12
Current children cumulated vsize (Kb) 42592

[startup+290.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 10465 0 0 0 28840 65 0 0 25 0 1 0 1797591460 44367872 10445 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 10832 10445 145 145 0 10687 0
[pid=9520] vsize: 43328
Current children cumulated CPU time (s) 289.05
Current children cumulated vsize (Kb) 45452

[startup+300.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 11239 0 0 0 29829 70 0 0 25 0 1 0 1797591460 47575040 11219 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 11615 11219 145 145 0 11470 0
[pid=9520] vsize: 46460
Current children cumulated CPU time (s) 298.99
Current children cumulated vsize (Kb) 48584

[startup+310.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 12347 0 0 0 30809 77 0 0 25 0 1 0 1797591460 52178944 12327 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 12739 12327 145 145 0 12594 0
[pid=9520] vsize: 50956
Current children cumulated CPU time (s) 308.86
Current children cumulated vsize (Kb) 53080

[startup+320.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 13299 0 0 0 31792 85 0 0 25 0 1 0 1797591460 56094720 13279 4294967295 134512640 135094434 3221224432 3221222960 134780607 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 13695 13279 145 145 0 13550 0
[pid=9520] vsize: 54780
Current children cumulated CPU time (s) 318.77
Current children cumulated vsize (Kb) 56904

[startup+330.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 14019 0 0 0 32780 90 0 0 25 0 1 0 1797591460 59146240 13999 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 14440 13999 145 145 0 14295 0
[pid=9520] vsize: 57760
Current children cumulated CPU time (s) 328.7
Current children cumulated vsize (Kb) 59884

[startup+340.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 14217 0 0 0 33778 91 0 0 25 0 1 0 1797591460 60002304 14197 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 14649 14197 145 145 0 14504 0
[pid=9520] vsize: 58596
Current children cumulated CPU time (s) 338.69
Current children cumulated vsize (Kb) 60720

[startup+350.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 14344 0 0 0 34776 92 0 0 25 0 1 0 1797591460 60592128 14324 4294967295 134512640 135094434 3221224432 3221223044 134563134 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 14793 14324 145 145 0 14648 0
[pid=9520] vsize: 59172
Current children cumulated CPU time (s) 348.68
Current children cumulated vsize (Kb) 61296

[startup+360.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 14430 0 0 0 35775 93 0 0 25 0 1 0 1797591460 60948480 14410 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 14880 14410 145 145 0 14735 0
[pid=9520] vsize: 59520
Current children cumulated CPU time (s) 358.68
Current children cumulated vsize (Kb) 61644

[startup+370.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 15514 0 0 0 36759 100 0 0 25 0 1 0 1797591460 65892352 15494 4294967295 134512640 135094434 3221224432 3221222208 134562757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 16087 15494 145 145 0 15942 0
[pid=9520] vsize: 64348
Current children cumulated CPU time (s) 368.59
Current children cumulated vsize (Kb) 66472

[startup+380.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 15514 0 0 0 37759 100 0 0 25 0 1 0 1797591460 65892352 15494 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 16087 15494 145 145 0 15942 0
[pid=9520] vsize: 64348
Current children cumulated CPU time (s) 378.59
Current children cumulated vsize (Kb) 66472

[startup+390.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 15514 0 0 0 38759 100 0 0 25 0 1 0 1797591460 65892352 15494 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 16087 15494 145 145 0 15942 0
[pid=9520] vsize: 64348
Current children cumulated CPU time (s) 388.59
Current children cumulated vsize (Kb) 66472

[startup+400.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 15514 0 0 0 39759 100 0 0 25 0 1 0 1797591460 65892352 15494 4294967295 134512640 135094434 3221224432 3221223088 134558238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 16087 15494 145 145 0 15942 0
[pid=9520] vsize: 64348
Current children cumulated CPU time (s) 398.59
Current children cumulated vsize (Kb) 66472

[startup+410.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 15514 0 0 0 40759 100 0 0 25 0 1 0 1797591460 65892352 15494 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 16087 15494 145 145 0 15942 0
[pid=9520] vsize: 64348
Current children cumulated CPU time (s) 408.59
Current children cumulated vsize (Kb) 66472

[startup+420.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 15514 0 0 0 41760 100 0 0 25 0 1 0 1797591460 65892352 15494 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 16087 15494 145 145 0 15942 0
[pid=9520] vsize: 64348
Current children cumulated CPU time (s) 418.6
Current children cumulated vsize (Kb) 66472

[startup+430.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 15514 0 0 0 42760 100 0 0 25 0 1 0 1797591460 65892352 15494 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 16087 15494 145 145 0 15942 0
[pid=9520] vsize: 64348
Current children cumulated CPU time (s) 428.6
Current children cumulated vsize (Kb) 66472

[startup+440.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 15514 0 0 0 43760 100 0 0 25 0 1 0 1797591460 65892352 15494 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 16087 15494 145 145 0 15942 0
[pid=9520] vsize: 64348
Current children cumulated CPU time (s) 438.6
Current children cumulated vsize (Kb) 66472

[startup+450.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 15514 0 0 0 44760 100 0 0 25 0 1 0 1797591460 65892352 15494 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 16087 15494 145 145 0 15942 0
[pid=9520] vsize: 64348
Current children cumulated CPU time (s) 448.6
Current children cumulated vsize (Kb) 66472

[startup+460.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 15514 0 0 0 45761 100 0 0 25 0 1 0 1797591460 65892352 15494 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 16087 15494 145 145 0 15942 0
[pid=9520] vsize: 64348
Current children cumulated CPU time (s) 458.61
Current children cumulated vsize (Kb) 66472

[startup+470.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 15514 0 0 0 46760 100 0 0 25 0 1 0 1797591460 65892352 15494 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 16087 15494 145 145 0 15942 0
[pid=9520] vsize: 64348
Current children cumulated CPU time (s) 468.6
Current children cumulated vsize (Kb) 66472

[startup+480.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 15514 0 0 0 47761 100 0 0 25 0 1 0 1797591460 65892352 15494 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 16087 15494 145 145 0 15942 0
[pid=9520] vsize: 64348
Current children cumulated CPU time (s) 478.61
Current children cumulated vsize (Kb) 66472

[startup+490.046 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18822 0 0 0 48752 108 0 0 25 0 1 0 1797591460 78188544 18101 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 19089 18101 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 488.6
Current children cumulated vsize (Kb) 78480

[startup+500.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18828 0 0 0 49752 109 0 0 25 0 1 0 1797591460 78188544 18107 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18107 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 498.61
Current children cumulated vsize (Kb) 78480

[startup+510.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18830 0 0 0 50752 109 0 0 25 0 1 0 1797591460 78188544 18109 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18109 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 508.61
Current children cumulated vsize (Kb) 78480

[startup+520.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18830 0 0 0 51752 109 0 0 25 0 1 0 1797591460 78188544 18109 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18109 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 518.61
Current children cumulated vsize (Kb) 78480

[startup+530.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18831 0 0 0 52753 109 0 0 25 0 1 0 1797591460 78188544 18110 4294967295 134512640 135094434 3221224432 3221223104 134556528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18110 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 528.62
Current children cumulated vsize (Kb) 78480

[startup+540.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18832 0 0 0 53753 109 0 0 25 0 1 0 1797591460 78188544 18111 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18111 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 538.62
Current children cumulated vsize (Kb) 78480

[startup+550.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18832 0 0 0 54753 109 0 0 25 0 1 0 1797591460 78188544 18111 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18111 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 548.62
Current children cumulated vsize (Kb) 78480

[startup+560.053 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18832 0 0 0 55753 109 0 0 25 0 1 0 1797591460 78188544 18111 4294967295 134512640 135094434 3221224432 3221223104 134556552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18111 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 558.62
Current children cumulated vsize (Kb) 78480

[startup+570.054 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18832 0 0 0 56753 109 0 0 25 0 1 0 1797591460 78188544 18111 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18111 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 568.62
Current children cumulated vsize (Kb) 78480

[startup+580.053 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18865 0 0 0 57753 109 0 0 25 0 1 0 1797591460 78188544 18144 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18144 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 578.62
Current children cumulated vsize (Kb) 78480

[startup+590.054 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18865 0 0 0 58753 109 0 0 25 0 1 0 1797591460 78188544 18144 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18144 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 588.62
Current children cumulated vsize (Kb) 78480

[startup+600.055 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18865 0 0 0 59754 109 0 0 25 0 1 0 1797591460 78188544 18144 4294967295 134512640 135094434 3221224432 3221223184 134559178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18144 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 598.63
Current children cumulated vsize (Kb) 78480

[startup+610.056 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18865 0 0 0 60754 109 0 0 25 0 1 0 1797591460 78188544 18144 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18144 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 608.63
Current children cumulated vsize (Kb) 78480

[startup+620.057 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18865 0 0 0 61754 109 0 0 25 0 1 0 1797591460 78188544 18144 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18144 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 618.63
Current children cumulated vsize (Kb) 78480

[startup+630.057 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18865 0 0 0 62754 110 0 0 25 0 1 0 1797591460 78188544 18144 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18144 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 628.64
Current children cumulated vsize (Kb) 78480

[startup+640.058 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18865 0 0 0 63754 110 0 0 25 0 1 0 1797591460 78188544 18144 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18144 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 638.64
Current children cumulated vsize (Kb) 78480

[startup+650.059 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18865 0 0 0 64754 110 0 0 25 0 1 0 1797591460 78188544 18144 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18144 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 648.64
Current children cumulated vsize (Kb) 78480

[startup+660.059 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18865 0 0 0 65753 111 0 0 25 0 1 0 1797591460 78188544 18144 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18144 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 658.64
Current children cumulated vsize (Kb) 78480

[startup+670.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18865 0 0 0 66752 111 0 0 25 0 1 0 1797591460 78188544 18144 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18144 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 668.63
Current children cumulated vsize (Kb) 78480

[startup+680.061 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 67752 112 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 678.64
Current children cumulated vsize (Kb) 78480

[startup+690.062 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 68752 112 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 688.64
Current children cumulated vsize (Kb) 78480

[startup+700.063 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 69752 113 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 698.65
Current children cumulated vsize (Kb) 78480

[startup+710.065 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 70752 113 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 708.65
Current children cumulated vsize (Kb) 78480

[startup+720.066 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 71752 113 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 718.65
Current children cumulated vsize (Kb) 78480

[startup+730.066 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 72752 113 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 728.65
Current children cumulated vsize (Kb) 78480

[startup+740.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 73752 113 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 738.65
Current children cumulated vsize (Kb) 78480

[startup+750.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 74753 113 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 748.66
Current children cumulated vsize (Kb) 78480

[startup+760.069 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 75753 113 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 758.66
Current children cumulated vsize (Kb) 78480

[startup+770.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 76753 113 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 768.66
Current children cumulated vsize (Kb) 78480

[startup+780.071 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 77753 113 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 778.66
Current children cumulated vsize (Kb) 78480

[startup+790.072 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 78753 113 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 788.66
Current children cumulated vsize (Kb) 78480

[startup+800.072 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 79753 114 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 798.67
Current children cumulated vsize (Kb) 78480

[startup+810.074 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 80753 114 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 808.67
Current children cumulated vsize (Kb) 78480

[startup+820.075 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 81753 114 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 818.67
Current children cumulated vsize (Kb) 78480

[startup+830.076 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 82754 114 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 828.68
Current children cumulated vsize (Kb) 78480

[startup+840.077 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 83754 114 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 838.68
Current children cumulated vsize (Kb) 78480

[startup+850.078 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 84754 114 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 848.68
Current children cumulated vsize (Kb) 78480

[startup+860.079 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 85754 114 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 858.68
Current children cumulated vsize (Kb) 78480

[startup+870.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 86754 114 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 868.68
Current children cumulated vsize (Kb) 78480

[startup+880.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 87755 114 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 878.69
Current children cumulated vsize (Kb) 78480

[startup+890.081 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 88755 115 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 888.7
Current children cumulated vsize (Kb) 78480

[startup+900.082 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 89755 115 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 898.7
Current children cumulated vsize (Kb) 78480

[startup+910.084 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 90755 115 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 908.7
Current children cumulated vsize (Kb) 78480

[startup+920.085 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 91755 115 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 918.7
Current children cumulated vsize (Kb) 78480

[startup+930.085 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 92756 115 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 928.71
Current children cumulated vsize (Kb) 78480

[startup+940.086 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 93756 115 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 938.71
Current children cumulated vsize (Kb) 78480

[startup+950.087 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18867 0 0 0 94756 115 0 0 25 0 1 0 1797591460 78188544 18146 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18146 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 948.71
Current children cumulated vsize (Kb) 78480

[startup+960.087 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18868 0 0 0 95756 115 0 0 25 0 1 0 1797591460 78188544 18147 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18147 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 958.71
Current children cumulated vsize (Kb) 78480

[startup+970.088 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18875 0 0 0 96756 115 0 0 25 0 1 0 1797591460 78188544 18154 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18154 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 968.71
Current children cumulated vsize (Kb) 78480

[startup+980.089 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18880 0 0 0 97756 115 0 0 25 0 1 0 1797591460 78188544 18159 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18159 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 978.71
Current children cumulated vsize (Kb) 78480

[startup+990.09 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18884 0 0 0 98757 115 0 0 25 0 1 0 1797591460 78188544 18163 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18163 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 988.72
Current children cumulated vsize (Kb) 78480

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18891 0 0 0 99757 115 0 0 25 0 1 0 1797591460 78188544 18170 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18170 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 998.72
Current children cumulated vsize (Kb) 78480

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18896 0 0 0 100757 115 0 0 25 0 1 0 1797591460 78188544 18175 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18175 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 1008.72
Current children cumulated vsize (Kb) 78480

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18903 0 0 0 101757 115 0 0 25 0 1 0 1797591460 78188544 18182 4294967295 134512640 135094434 3221224432 3221223120 134554705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18182 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 1018.72
Current children cumulated vsize (Kb) 78480

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18907 0 0 0 102757 115 0 0 25 0 1 0 1797591460 78188544 18186 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18186 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 1028.72
Current children cumulated vsize (Kb) 78480

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18911 0 0 0 103758 115 0 0 25 0 1 0 1797591460 78188544 18190 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18190 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 1038.73
Current children cumulated vsize (Kb) 78480

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18916 0 0 0 104758 115 0 0 25 0 1 0 1797591460 78188544 18195 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18195 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 1048.73
Current children cumulated vsize (Kb) 78480

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18924 0 0 0 105758 115 0 0 25 0 1 0 1797591460 78188544 18203 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18203 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 1058.73
Current children cumulated vsize (Kb) 78480

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18933 0 0 0 106758 116 0 0 25 0 1 0 1797591460 78188544 18212 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18212 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 1068.74
Current children cumulated vsize (Kb) 78480

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18938 0 0 0 107758 116 0 0 25 0 1 0 1797591460 78188544 18217 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18217 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 1078.74
Current children cumulated vsize (Kb) 78480

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 18942 0 0 0 108759 116 0 0 25 0 1 0 1797591460 78188544 18221 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19089 18221 145 145 0 18944 0
[pid=9520] vsize: 76356
Current children cumulated CPU time (s) 1088.75
Current children cumulated vsize (Kb) 78480

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 19465 0 0 0 109750 118 0 0 25 0 1 0 1797591460 80318464 18744 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 19609 18744 145 145 0 19464 0
[pid=9520] vsize: 78436
Current children cumulated CPU time (s) 1098.68
Current children cumulated vsize (Kb) 80560

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 20209 0 0 0 110737 124 0 0 25 0 1 0 1797591460 83357696 19488 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 20351 19488 145 145 0 20206 0
[pid=9520] vsize: 81404
Current children cumulated CPU time (s) 1108.61
Current children cumulated vsize (Kb) 83528

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 20927 0 0 0 111725 129 0 0 25 0 1 0 1797591460 86298624 20206 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 21069 20206 145 145 0 20924 0
[pid=9520] vsize: 84276
Current children cumulated CPU time (s) 1118.54
Current children cumulated vsize (Kb) 86400

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 21495 0 0 0 112713 133 0 0 25 0 1 0 1797591460 88616960 20774 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 21635 20774 145 145 0 21490 0
[pid=9520] vsize: 86540
Current children cumulated CPU time (s) 1128.46
Current children cumulated vsize (Kb) 88664

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) T 9516 9516 6847 0 -1 0 22131 0 0 0 113703 138 0 0 25 0 1 0 1797591460 91201536 21410 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9520/statm): 22266 21410 145 145 0 22121 0
[pid=9520] vsize: 89064
Current children cumulated CPU time (s) 1138.41
Current children cumulated vsize (Kb) 91188

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 23015 0 0 0 114689 143 0 0 25 0 1 0 1797591460 94806016 22294 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 23146 22294 145 145 0 23001 0
[pid=9520] vsize: 92584
Current children cumulated CPU time (s) 1148.32
Current children cumulated vsize (Kb) 94708

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 23838 0 0 0 115675 150 0 0 25 0 1 0 1797591460 98160640 23117 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 23965 23117 145 145 0 23820 0
[pid=9520] vsize: 95860
Current children cumulated CPU time (s) 1158.25
Current children cumulated vsize (Kb) 97984

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 24602 0 0 0 116663 154 0 0 25 0 1 0 1797591460 101277696 23881 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 24726 23881 145 145 0 24581 0
[pid=9520] vsize: 98904
Current children cumulated CPU time (s) 1168.17
Current children cumulated vsize (Kb) 101028

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 25313 0 0 0 117652 159 0 0 25 0 1 0 1797591460 104177664 24592 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9520/statm): 25434 24592 145 145 0 25289 0
[pid=9520] vsize: 101736
Current children cumulated CPU time (s) 1178.11
Current children cumulated vsize (Kb) 103860

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 25963 0 0 0 118641 164 0 0 25 0 1 0 1797591460 106835968 25242 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 26083 25242 145 145 0 25938 0
[pid=9520] vsize: 104332
Current children cumulated CPU time (s) 1188.05
Current children cumulated vsize (Kb) 106456

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) R 9516 9516 6847 0 -1 0 26629 0 0 0 119629 169 0 0 25 0 1 0 1797591460 109555712 25908 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9520/statm): 26747 25908 145 145 0 26602 0
[pid=9520] vsize: 106988
Current children cumulated CPU time (s) 1197.98
Current children cumulated vsize (Kb) 109112

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.91 1/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) T 9516 9516 6847 0 -1 0 27259 0 0 0 120617 174 0 0 25 0 1 0 1797591460 112136192 26538 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9520/statm): 27377 26538 145 145 0 27232 0
[pid=9520] vsize: 109508
Current children cumulated CPU time (s) 1207.91
Current children cumulated vsize (Kb) 111632



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.91 1/57 9520
Raw data (/proc/9516/stat): 9516 (minisat+_script) S 9515 9516 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797591455 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9516/statm): 531 226 485 147 0 384 0
[pid=9516] vsize: 2124
Raw data (/proc/9520/stat): 9520 (minisat+_64-bit) T 9516 9516 6847 0 -1 0 27259 0 0 0 120617 174 0 0 25 0 1 0 1797591460 112136192 26538 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9520/statm): 27377 26538 145 145 0 27232 0
[pid=9520] vsize: 109508
Current children cumulated CPU time (s) 1207.91
Current children cumulated vsize (Kb) 111632

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

Child status: 10
Real time (s): 1210.18
CPU time (s): 1207.99
CPU user time (s): 1206.19
CPU system time (s): 1.79973
CPU usage (%): 99.8188
Max. virtual memory (cumulated for all children) (Kb): 111632

Verifier Data

ERROR: no interpretation found !