PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran8x32.opb
MD5SUM	ff0017de67077abd1f68238274b64e50
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1695644
Optimality of the best value was proved	NO
Number of terms in the objective function	5376
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	1517603678
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	1517603678
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.03
Number of variables	5376
Total number of constraints	296
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	296
Minimum length of a constraint	21
Maximum length of a constraint	640
Trace number 17598

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 10:51:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19369 boxname=wulflinc29 idbench=1490 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ff0017de67077abd1f68238274b64e50  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-ran8x32.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-ran8x32.opb /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-ran8x32.opb
IDLAUNCH: 19369
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        747316 kB
Buffers:           888 kB
Cached:         262700 kB
SwapCached:        524 kB
Active:          54364 kB
Inactive:       211192 kB
HighTotal:      131008 kB
HighFree:         3248 kB
LowTotal:       903652 kB
LowFree:        744068 kB
SwapTotal:     2097892 kB
SwapFree:      2096460 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            16064 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:11:08 (client local time) WITH STATUS 10 IN 1200.35 SECONDS
stats: 19369 7 1200.35 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 336 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 334]---> BDD-cost: 9183
c ---[ 332]---> BDD-cost:11644
c ---[ 330]---> BDD-cost:12118
c ---[ 328]---> BDD-cost:11156
c ---[ 326]---> BDD-cost:10952
c ---[ 324]---> BDD-cost:10952
c ---[ 322]---> BDD-cost:11506
c ---[ 320]---> BDD-cost:12567
c ---[ 318]---> BDD-cost:  521
c ---[ 316]---> BDD-cost:  728
c ---[ 314]---> BDD-cost:  655
c ---[ 312]---> BDD-cost:  903
c ---[ 310]---> BDD-cost:  818
c ---[ 308]---> BDD-cost:  711
c ---[ 306]---> BDD-cost:  705
c ---[ 304]---> BDD-cost:  666
c ---[ 302]---> BDD-cost:  724
c ---[ 300]---> BDD-cost:  429
c ---[ 298]---> BDD-cost:  801
c ---[ 296]---> BDD-cost:  613
c ---[ 294]---> BDD-cost:  907
c ---[ 292]---> BDD-cost:  563
c ---[ 290]---> BDD-cost:  632
c ---[ 288]---> BDD-cost:  666
c ---[ 286]---> BDD-cost:  848
c ---[ 284]---> BDD-cost:  711
c ---[ 282]---> BDD-cost:  521
c ---[ 280]---> BDD-cost:  655
c ---[ 278]---> BDD-cost:  655
c ---[ 276]---> BDD-cost:  884
c ---[ 274]---> BDD-cost:  711
c ---[ 272]---> BDD-cost:  563
c ---[ 270]---> BDD-cost:  711
c ---[ 268]---> BDD-cost:  749
c ---[ 266]---> BDD-cost:  801
c ---[ 264]---> BDD-cost:  666
c ---[ 262]---> BDD-cost:  521
c ---[ 260]---> BDD-cost:  801
c ---[ 258]---> BDD-cost:  758
c ---[ 256]---> BDD-cost:  711
c ---[ 255]---> BDD-cost:   10
c ---[ 254]---> BDD-cost:   15
c ---[ 253]---> BDD-cost:   12
c ---[ 252]---> BDD-cost:   16
c ---[ 251]---> BDD-cost:   13
c ---[ 250]---> BDD-cost:   10
c ---[ 249]---> BDD-cost:   16
c ---[ 248]---> BDD-cost:   14
c ---[ 247]---> BDD-cost:   15
c ---[ 246]---> BDD-cost:   12
c ---[ 245]---> BDD-cost:   16
c ---[ 244]---> BDD-cost:   16
c ---[ 243]---> BDD-cost:   15
c ---[ 242]---> BDD-cost:   15
c ---[ 241]---> BDD-cost:   12
c ---[ 240]---> BDD-cost:   13
c ---[ 239]---> BDD-cost:   14
c ---[ 238]---> BDD-cost:    9
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:   11
c ---[ 235]---> BDD-cost:   11
c ---[ 234]---> BDD-cost:   13
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   15
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   10
c ---[ 228]---> BDD-cost:   12
c ---[ 227]---> BDD-cost:   12
c ---[ 226]---> BDD-cost:   18
c ---[ 225]---> BDD-cost:   15
c ---[ 224]---> BDD-cost:   15
c ---[ 223]---> BDD-cost:   15
c ---[ 222]---> BDD-cost:   10
c ---[ 221]---> BDD-cost:   15
c ---[ 220]---> BDD-cost:   15
c ---[ 219]---> BDD-cost:   17
c ---[ 218]---> BDD-cost:   11
c ---[ 217]---> BDD-cost:   16
c ---[ 216]---> BDD-cost:   13
c ---[ 215]---> BDD-cost:   10
c ---[ 214]---> BDD-cost:   16
c ---[ 213]---> BDD-cost:   14
c ---[ 212]---> BDD-cost:   15
c ---[ 211]---> BDD-cost:   12
c ---[ 210]---> BDD-cost:   17
c ---[ 209]---> BDD-cost:   12
c ---[ 208]---> BDD-cost:   16
c ---[ 207]---> BDD-cost:   15
c ---[ 206]---> BDD-cost:   12
c ---[ 205]---> BDD-cost:   13
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:    9
c ---[ 202]---> BDD-cost:   16
c ---[ 201]---> BDD-cost:   11
c ---[ 200]---> BDD-cost:   11
c ---[ 199]---> BDD-cost:   13
c ---[ 198]---> BDD-cost:   13
c ---[ 197]---> BDD-cost:   13
c ---[ 196]---> BDD-cost:   17
c ---[ 195]---> BDD-cost:   15
c ---[ 194]---> BDD-cost:   10
c ---[ 193]---> BDD-cost:   12
c ---[ 192]---> BDD-cost:   12
c ---[ 191]---> BDD-cost:   18
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   15
c ---[ 187]---> BDD-cost:   14
c ---[ 186]---> BDD-cost:   10
c ---[ 185]---> BDD-cost:   15
c ---[ 184]---> BDD-cost:   17
c ---[ 183]---> BDD-cost:   11
c ---[ 182]---> BDD-cost:   16
c ---[ 181]---> BDD-cost:   13
c ---[ 180]---> BDD-cost:   10
c ---[ 179]---> BDD-cost:   16
c ---[ 178]---> BDD-cost:   14
c ---[ 177]---> BDD-cost:   15
c ---[ 176]---> BDD-cost:    9
c ---[ 175]---> BDD-cost:   12
c ---[ 174]---> BDD-cost:   17
c ---[ 173]---> BDD-cost:   16
c ---[ 172]---> BDD-cost:   15
c ---[ 171]---> BDD-cost:   12
c ---[ 170]---> BDD-cost:   13
c ---[ 169]---> BDD-cost:   14
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:   16
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   15
c ---[ 164]---> BDD-cost:   11
c ---[ 163]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 161]---> BDD-cost:   17
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   10
c ---[ 158]---> BDD-cost:   12
c ---[ 157]---> BDD-cost:   12
c ---[ 156]---> BDD-cost:   18
c ---[ 155]---> BDD-cost:   15
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:   15
c ---[ 152]---> BDD-cost:   15
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:   15
c ---[ 149]---> BDD-cost:   17
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:   16
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:   16
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   14
c ---[ 140]---> BDD-cost:   15
c ---[ 139]---> BDD-cost:   12
c ---[ 138]---> BDD-cost:   19
c ---[ 137]---> BDD-cost:   16
c ---[ 136]---> BDD-cost:   15
c ---[ 135]---> BDD-cost:   12
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   14
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   16
c ---[ 129]---> BDD-cost:   11
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   13
c ---[ 125]---> BDD-cost:   17
c ---[ 124]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   10
c ---[ 122]---> BDD-cost:   12
c ---[ 121]---> BDD-cost:   12
c ---[ 120]---> BDD-cost:   13
c ---[ 119]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:   15
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   10
c ---[ 114]---> BDD-cost:   15
c ---[ 113]---> BDD-cost:   17
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   16
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   15
c ---[ 108]---> BDD-cost:   10
c ---[ 107]---> BDD-cost:   16
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   15
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   19
c ---[ 102]---> BDD-cost:   16
c ---[ 101]---> BDD-cost:   15
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   14
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   16
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   13
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   10
c ---[  86]---> BDD-cost:   12
c ---[  85]---> BDD-cost:   12
c ---[  84]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   15
c ---[  80]---> BDD-cost:   12
c ---[  79]---> BDD-cost:   12
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   10
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   16
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   10
c ---[  66]---> BDD-cost:   16
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   14
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   12
c ---[  61]---> BDD-cost:   19
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   12
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   16
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   15
c ---[  46]---> BDD-cost:   10
c ---[  45]---> BDD-cost:   12
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   18
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   10
c ---[  37]---> BDD-cost:   15
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   16
c ---[  33]---> BDD-cost:   13
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   16
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   12
c ---[  26]---> BDD-cost:   19
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   15
c ---[  23]---> BDD-cost:   12
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:   16
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   17
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   10
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   12
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   18
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   15
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  332220   976299 |  110740       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 5856164[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:534074     Base: 2 2 2 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        27 | 1821483  4452446 |  607161      27      716    26.5 |  0.000 % |
c |       127 | 1821483  4452446 |  667877     127     1573    12.4 |  0.427 % |
c |       278 | 1821483  4452446 |  734664     278     2579     9.3 |  0.427 % |
c |       503 | 1821483  4452446 |  808131     503     4374     8.7 |  0.427 % |
c |       841 | 1821347  4452140 |  888944     839     6176     7.4 |  0.432 % |
c |      1347 | 1821327  4452095 |  977838    1344    16389    12.2 |  0.433 % |
c |      2106 | 1821327  4452095 | 1075622    2103    23570    11.2 |  0.433 % |
c |      3245 | 1821227  4451870 | 1183185    3240    33336    10.3 |  0.437 % |
c |      4954 | 1821160  4451718 | 1301503    4948    71512    14.5 |  0.440 % |
c |      7516 | 1821160  4451718 | 1431653    7510    93138    12.4 |  0.440 % |
c |     11361 | 1821160  4451718 | 1574819   11355   340505    30.0 |  0.440 % |
c |     17128 | 1821160  4451718 | 1732301   17122   409294    23.9 |  0.440 % |
c |     25778 | 1821160  4451718 | 1905531   25772   618080    24.0 |  0.440 % |
c |     38752 | 1821160  4451718 | 2096084   38746   916713    23.7 |  0.440 % |
c |     58213 | 1820646  4450552 | 2305692   58199  1501721    25.8 |  0.463 % |
c |     87406 | 1820646  4450552 | 2536262   87392  2580321    29.5 |  0.463 % |
c |    131196 | 1820597  4450442 | 2789888  131181  3931246    30.0 |  0.465 % |
c ==============================================================================
c [1mFound solution: 3975939[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    135021 | 1826718  4467004 |  608906  135005  4004088    29.7 |  0.465 % |
c |    135123 | 1826718  4467004 |  669796  135107  4004654    29.6 |  0.466 % |
c |    135273 | 1826718  4467004 |  736776  135257  4005516    29.6 |  0.466 % |
c |    135498 | 1826718  4467004 |  810453  135482  4007251    29.6 |  0.466 % |
c |    135836 | 1826718  4467004 |  891499  135820  4013113    29.5 |  0.466 % |
c |    136342 | 1826446  4466386 |  980649  136324  4019480    29.5 |  0.478 % |
c |    137102 | 1825946  4465259 | 1078714  137079  4029645    29.4 |  0.499 % |
c |    138243 | 1825946  4465259 | 1186585  138220  4049081    29.3 |  0.499 % |
c |    139951 | 1825946  4465259 | 1305244  139928  4138732    29.6 |  0.499 % |
c ==============================================================================
c [1mFound solution: 3387544[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    140877 | 1826434  4466537 |  608811  140854  4211156    29.9 |  0.499 % |
c |    140977 | 1826434  4466537 |  669692  140954  4212159    29.9 |  0.499 % |
c |    141127 | 1826434  4466537 |  736661  141104  4214244    29.9 |  0.499 % |
c |    141352 | 1826024  4465603 |  810327  141325  4218635    29.9 |  0.517 % |
c |    141689 | 1825845  4465190 |  891360  141661  4222404    29.8 |  0.526 % |
c |    142195 | 1825543  4464507 |  980496  142153  4231426    29.8 |  0.540 % |
c |    142954 | 1825543  4464507 | 1078545  142912  4246935    29.7 |  0.540 % |
c |    144093 | 1825543  4464507 | 1186400  144051  4267871    29.6 |  0.540 % |
c |    145801 | 1824731  4462657 | 1305040  145719  4327406    29.7 |  0.576 % |
c |    148363 | 1824731  4462657 | 1435544  148281  4393429    29.6 |  0.576 % |
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 X252_bit_7 X252_bit_6 X252_bit_5 X252_bit_4 X252_bit_3 X252_bit_2 X252_bit_1 X252_bit0 X252_bit1 X252_bit2 -X252_bit3 -X252_bit4 -X252_bit5 -X252_bit6 -X252_bit7 -X252_bit8 -X252_bit9 -X252_bit10 -X252_bit11 -X252_bit12 X253_bit_7 -X253_bit_6 -X253_bit_5 X253_bit_4 X253_bit_3 X253_bit_2 X253_bit_1 -X253_bit0 -X253_bit1 -X253_bit2 -X253_bit3 -X253_bit4 -X253_bit5 -X253_bit6 -X253_bit7 -X253_bit8 -X253_bit9 -X253_bit10 -X253_bit11 -X253_bit12 -X254_bit_7 -X254_bit_6 -X254_bit_5 -X254_bit_4 -X254_bit_3 -X254_bit_2 -X254_bit_1 -X254_bit0 -X254_bit1 -X254_bit2 -X254_bit3 -X254_bit4 -X254_bit5 -X254_bit6 -X254_bit7 -X254_bit8 -X254_bit9 -X254_bit10 -X254_bit11 -X254_bit12 X255_bit_7 X255_bit_6 X255_bit_5 -X255_bit_4 X255_bit_3 X255_bit_2 X255_bit_1 -X255_bit0 X255_bit1 -X255_bit2 -X255_bit3 -X255_bit4 -X255_bit5 -X255_bit6 -X255_bit7 -X255_bit8 -X255_bit9 -X255_bit10 -X255_bit11 -X255_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 -Y1#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.92 2/54 30115
Raw data (stat): 30115 (runsolver) R 30114 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544493956 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99989 s]
Raw data (loadavg): 0.92 0.95 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 47710 0 0 0 893 106 0 0 25 0 1 0 544493956 231649280 46088 4294967295 134512640 134672761 3221224528 3221175968 134555539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56555 46088 603 41 0 56514 0
vsize: 226220
[startup+20.0066 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 51779 0 0 0 1883 116 0 0 25 0 1 0 544493956 245977088 50157 4294967295 134512640 134672761 3221224528 3221223744 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60053 50157 603 41 0 60012 0
vsize: 240212
[startup+30.0073 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 51816 0 0 0 2883 116 0 0 25 0 1 0 544493956 246112256 50194 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60086 50194 603 41 0 60045 0
vsize: 240344
[startup+40.0072 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 51964 0 0 0 3882 117 0 0 25 0 1 0 544493956 246382592 50342 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60152 50342 603 41 0 60111 0
vsize: 240608
[startup+50.008 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 52065 0 0 0 4882 118 0 0 25 0 1 0 544493956 246644736 50443 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60216 50443 603 41 0 60175 0
vsize: 240864
[startup+60.0078 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 52216 0 0 0 5881 118 0 0 25 0 1 0 544493956 246943744 50594 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60289 50594 603 41 0 60248 0
vsize: 241156
[startup+70.0156 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 52466 0 0 0 6881 119 0 0 25 0 1 0 544493956 247746560 50844 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60485 50844 603 41 0 60444 0
vsize: 241940
[startup+80.0164 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 52569 0 0 0 7880 120 0 0 25 0 1 0 544493956 248344576 50947 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60631 50947 603 41 0 60590 0
vsize: 242524
[startup+90.016 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 52608 0 0 0 8880 120 0 0 25 0 1 0 544493956 248475648 50986 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60663 50986 603 41 0 60622 0
vsize: 242652
[startup+100.016 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 52745 0 0 0 9880 121 0 0 25 0 1 0 544493956 249008128 51123 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60793 51123 603 41 0 60752 0
vsize: 243172
[startup+110.016 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 52795 0 0 0 10880 121 0 0 25 0 1 0 544493956 249139200 51173 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60825 51173 603 41 0 60784 0
vsize: 243300
[startup+120.015 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 52854 0 0 0 11879 122 0 0 25 0 1 0 544493956 249409536 51232 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60891 51232 603 41 0 60850 0
vsize: 243564
[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 52936 0 0 0 12880 122 0 0 25 0 1 0 544493956 249679872 51314 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60957 51314 603 41 0 60916 0
vsize: 243828
[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 52967 0 0 0 13879 122 0 0 25 0 1 0 544493956 249815040 51345 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60990 51345 603 41 0 60949 0
vsize: 243960
[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 52988 0 0 0 14879 122 0 0 25 0 1 0 544493956 249946112 51366 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61022 51366 603 41 0 60981 0
vsize: 244088
[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 53080 0 0 0 15879 122 0 0 25 0 1 0 544493956 250347520 51458 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61120 51458 603 41 0 61079 0
vsize: 244480
[startup+170.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 53174 0 0 0 16879 123 0 0 25 0 1 0 544493956 250744832 51552 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61217 51552 603 41 0 61176 0
vsize: 244868
[startup+180.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 53247 0 0 0 17879 123 0 0 25 0 1 0 544493956 251150336 51625 4294967295 134512640 134672761 3221224528 3221223744 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61316 51625 603 41 0 61275 0
vsize: 245264
[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 53378 0 0 0 18879 123 0 0 25 0 1 0 544493956 251682816 51756 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61446 51756 603 41 0 61405 0
vsize: 245784
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 53503 0 0 0 19879 124 0 0 25 0 1 0 544493956 252088320 51881 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61545 51881 603 41 0 61504 0
vsize: 246180
[startup+210.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 53712 0 0 0 20878 125 0 0 25 0 1 0 544493956 252891136 52090 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61741 52090 603 41 0 61700 0
vsize: 246964
[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 53907 0 0 0 21877 125 0 0 25 0 1 0 544493956 253693952 52285 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61937 52285 603 41 0 61896 0
vsize: 247748
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 53932 0 0 0 22877 125 0 0 25 0 1 0 544493956 253829120 52310 4294967295 134512640 134672761 3221224528 3221223716 134556676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61970 52310 603 41 0 61929 0
vsize: 247880
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 53966 0 0 0 23877 126 0 0 25 0 1 0 544493956 253964288 52344 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62003 52344 603 41 0 61962 0
vsize: 248012
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54012 0 0 0 24877 126 0 0 25 0 1 0 544493956 254099456 52390 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62036 52390 603 41 0 61995 0
vsize: 248144
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54086 0 0 0 25877 126 0 0 25 0 1 0 544493956 254496768 52464 4294967295 134512640 134672761 3221224528 3221223680 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62133 52464 603 41 0 62092 0
vsize: 248532
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54184 0 0 0 26877 127 0 0 25 0 1 0 544493956 255029248 52562 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62263 52562 603 41 0 62222 0
vsize: 249052
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54224 0 0 0 27877 127 0 0 25 0 1 0 544493956 255299584 52602 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62329 52602 603 41 0 62288 0
vsize: 249316
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54253 0 0 0 28877 127 0 0 25 0 1 0 544493956 255299584 52631 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62329 52631 603 41 0 62288 0
vsize: 249316
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54283 0 0 0 29877 127 0 0 25 0 1 0 544493956 255434752 52661 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62362 52661 603 41 0 62321 0
vsize: 249448
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54313 0 0 0 30877 127 0 0 25 0 1 0 544493956 255623168 52691 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62408 52691 603 41 0 62367 0
vsize: 249632
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54367 0 0 0 31877 127 0 0 25 0 1 0 544493956 255893504 52745 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62474 52745 603 41 0 62433 0
vsize: 249896
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54474 0 0 0 32877 127 0 0 25 0 1 0 544493956 256294912 52852 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62572 52852 603 41 0 62531 0
vsize: 250288
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54548 0 0 0 33877 128 0 0 25 0 1 0 544493956 256557056 52926 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62636 52926 603 41 0 62595 0
vsize: 250544
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54636 0 0 0 34877 128 0 0 25 0 1 0 544493956 256954368 53014 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62733 53014 603 41 0 62692 0
vsize: 250932
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54733 0 0 0 35877 128 0 0 25 0 1 0 544493956 257355776 53111 4294967295 134512640 134672761 3221224528 3221223664 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62831 53111 603 41 0 62790 0
vsize: 251324
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54834 0 0 0 36877 128 0 0 25 0 1 0 544493956 257761280 53212 4294967295 134512640 134672761 3221224528 3221223632 134559974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62930 53212 603 41 0 62889 0
vsize: 251720
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 54924 0 0 0 37876 129 0 0 25 0 1 0 544493956 258031616 53302 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62996 53302 603 41 0 62955 0
vsize: 251984
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55024 0 0 0 38876 130 0 0 25 0 1 0 544493956 258428928 53402 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63093 53402 603 41 0 63052 0
vsize: 252372
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55149 0 0 0 39876 130 0 0 25 0 1 0 544493956 258965504 53527 4294967295 134512640 134672761 3221224528 3221223728 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63224 53527 603 41 0 63183 0
vsize: 252896
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55286 0 0 0 40875 131 0 0 25 0 1 0 544493956 259497984 53664 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63354 53664 603 41 0 63313 0
vsize: 253416
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55346 0 0 0 41875 131 0 0 25 0 1 0 544493956 259768320 53724 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63420 53724 603 41 0 63379 0
vsize: 253680
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55389 0 0 0 42875 131 0 0 25 0 1 0 544493956 259903488 53767 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63453 53767 603 41 0 63412 0
vsize: 253812
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55461 0 0 0 43875 131 0 0 25 0 1 0 544493956 260173824 53839 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63519 53839 603 41 0 63478 0
vsize: 254076
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55536 0 0 0 44874 132 0 0 25 0 1 0 544493956 260444160 53914 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63585 53914 603 41 0 63544 0
vsize: 254340
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55598 0 0 0 45874 132 0 0 25 0 1 0 544493956 260710400 53976 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63650 53976 603 41 0 63609 0
vsize: 254600
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55615 0 0 0 46874 132 0 0 25 0 1 0 544493956 260710400 53993 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63650 53993 603 41 0 63609 0
vsize: 254600
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55645 0 0 0 47874 132 0 0 25 0 1 0 544493956 260841472 54023 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63682 54023 603 41 0 63641 0
vsize: 254728
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55681 0 0 0 48874 132 0 0 25 0 1 0 544493956 260972544 54059 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63714 54059 603 41 0 63673 0
vsize: 254856
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55724 0 0 0 49874 133 0 0 25 0 1 0 544493956 261107712 54102 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63747 54102 603 41 0 63706 0
vsize: 254988
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55755 0 0 0 50874 133 0 0 25 0 1 0 544493956 261238784 54133 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63779 54133 603 41 0 63738 0
vsize: 255116
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55776 0 0 0 51874 133 0 0 25 0 1 0 544493956 261369856 54154 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63811 54154 603 41 0 63770 0
vsize: 255244
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30115
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55803 0 0 0 52874 133 0 0 25 0 1 0 544493956 261505024 54181 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63844 54181 603 41 0 63803 0
vsize: 255376
[startup+540.017 s]
Raw data (loadavg): 1.07 0.99 0.93 2/58 30149
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55827 0 0 0 53875 133 0 0 25 0 1 0 544493956 261640192 54205 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63877 54205 603 41 0 63836 0
vsize: 255508
[startup+550.021 s]
Raw data (loadavg): 1.14 1.00 0.93 2/54 30168
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55861 0 0 0 54875 133 0 0 25 0 1 0 544493956 261771264 54239 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63909 54239 603 41 0 63868 0
vsize: 255636
[startup+560.021 s]
Raw data (loadavg): 1.11 1.00 0.93 2/54 30168
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55878 0 0 0 55874 134 0 0 25 0 1 0 544493956 261771264 54256 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63909 54256 603 41 0 63868 0
vsize: 255636
[startup+570.021 s]
Raw data (loadavg): 1.10 1.00 0.93 2/54 30168
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55898 0 0 0 56874 135 0 0 25 0 1 0 544493956 261906432 54276 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63942 54276 603 41 0 63901 0
vsize: 255768
[startup+580.022 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 30168
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55918 0 0 0 57874 135 0 0 25 0 1 0 544493956 261906432 54296 4294967295 134512640 134672761 3221224528 3221223728 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63942 54296 603 41 0 63901 0
vsize: 255768
[startup+590.023 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 30168
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55939 0 0 0 58873 136 0 0 25 0 1 0 544493956 262041600 54317 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63975 54317 603 41 0 63934 0
vsize: 255900
[startup+600.023 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 30168
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55964 0 0 0 59873 136 0 0 25 0 1 0 544493956 262176768 54342 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64008 54342 603 41 0 63967 0
vsize: 256032
[startup+610.024 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 30168
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 55986 0 0 0 60873 136 0 0 25 0 1 0 544493956 262176768 54364 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64008 54364 603 41 0 63967 0
vsize: 256032
[startup+620.024 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56011 0 0 0 61872 137 0 0 25 0 1 0 544493956 262311936 54389 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64041 54389 603 41 0 64000 0
vsize: 256164
[startup+630.025 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56033 0 0 0 62873 137 0 0 25 0 1 0 544493956 262443008 54411 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64073 54411 603 41 0 64032 0
vsize: 256292
[startup+640.025 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56057 0 0 0 63873 137 0 0 25 0 1 0 544493956 262443008 54435 4294967295 134512640 134672761 3221224528 3221223712 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64073 54435 603 41 0 64032 0
vsize: 256292
[startup+650.025 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56080 0 0 0 64873 137 0 0 25 0 1 0 544493956 262578176 54458 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64106 54458 603 41 0 64065 0
vsize: 256424
[startup+660.025 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56105 0 0 0 65873 137 0 0 25 0 1 0 544493956 262709248 54483 4294967295 134512640 134672761 3221224528 3221223684 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64138 54483 603 41 0 64097 0
vsize: 256552
[startup+670.025 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56125 0 0 0 66873 137 0 0 25 0 1 0 544493956 262709248 54503 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64138 54503 603 41 0 64097 0
vsize: 256552
[startup+680.026 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56149 0 0 0 67873 137 0 0 25 0 1 0 544493956 262844416 54527 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64171 54527 603 41 0 64130 0
vsize: 256684
[startup+690.026 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56173 0 0 0 68873 137 0 0 25 0 1 0 544493956 262975488 54551 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64203 54551 603 41 0 64162 0
vsize: 256812
[startup+700.026 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56200 0 0 0 69873 137 0 0 25 0 1 0 544493956 263114752 54578 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64237 54578 603 41 0 64196 0
vsize: 256948
[startup+710.026 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56217 0 0 0 70873 138 0 0 25 0 1 0 544493956 263114752 54595 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64237 54595 603 41 0 64196 0
vsize: 256948
[startup+720.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56233 0 0 0 71873 138 0 0 25 0 1 0 544493956 263249920 54611 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64270 54611 603 41 0 64229 0
vsize: 257080
[startup+730.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56249 0 0 0 72873 138 0 0 25 0 1 0 544493956 263249920 54627 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64270 54627 603 41 0 64229 0
vsize: 257080
[startup+740.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56289 0 0 0 73873 138 0 0 25 0 1 0 544493956 263380992 54667 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64302 54667 603 41 0 64261 0
vsize: 257208
[startup+750.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56420 0 0 0 74873 138 0 0 25 0 1 0 544493956 263909376 54798 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64431 54798 603 41 0 64390 0
vsize: 257724
[startup+760.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56552 0 0 0 75873 139 0 0 25 0 1 0 544493956 264450048 54930 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64563 54930 603 41 0 64522 0
vsize: 258252
[startup+770.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56574 0 0 0 76873 139 0 0 25 0 1 0 544493956 264585216 54952 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64596 54952 603 41 0 64555 0
vsize: 258384
[startup+780.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56592 0 0 0 77873 139 0 0 25 0 1 0 544493956 264585216 54970 4294967295 134512640 134672761 3221224528 3221223728 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64596 54970 603 41 0 64555 0
vsize: 258384
[startup+790.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56658 0 0 0 78873 139 0 0 25 0 1 0 544493956 264855552 55036 4294967295 134512640 134672761 3221224528 3221223728 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64662 55036 603 41 0 64621 0
vsize: 258648
[startup+800.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56735 0 0 0 79873 140 0 0 25 0 1 0 544493956 265125888 55113 4294967295 134512640 134672761 3221224528 3221223664 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64728 55113 603 41 0 64687 0
vsize: 258912
[startup+810.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56782 0 0 0 80873 140 0 0 25 0 1 0 544493956 265392128 55160 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64793 55160 603 41 0 64752 0
vsize: 259172
[startup+820.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56827 0 0 0 81873 140 0 0 25 0 1 0 544493956 265527296 55205 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64826 55205 603 41 0 64785 0
vsize: 259304
[startup+830.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56871 0 0 0 82872 140 0 0 25 0 1 0 544493956 265793536 55249 4294967295 134512640 134672761 3221224528 3221223688 134565025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64891 55250 603 41 0 64850 0
vsize: 259564
[startup+840.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56903 0 0 0 83872 140 0 0 25 0 1 0 544493956 265793536 55281 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64891 55281 603 41 0 64850 0
vsize: 259564
[startup+850.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 56951 0 0 0 84872 140 0 0 25 0 1 0 544493956 266063872 55329 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64957 55329 603 41 0 64916 0
vsize: 259828
[startup+860.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 57009 0 0 0 85873 140 0 0 25 0 1 0 544493956 266850304 55387 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65149 55387 603 41 0 65108 0
vsize: 260596
[startup+870.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 57037 0 0 0 86872 140 0 0 25 0 1 0 544493956 266977280 55415 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65180 55415 603 41 0 65139 0
vsize: 260720
[startup+880.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30170
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 57053 0 0 0 87872 140 0 0 25 0 1 0 544493956 266977280 55431 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65180 55431 603 41 0 65139 0
vsize: 260720
[startup+890.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 57098 0 0 0 88872 140 0 0 25 0 1 0 544493956 267108352 55476 4294967295 134512640 134672761 3221224528 3221223680 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65212 55476 603 41 0 65171 0
vsize: 260848
[startup+900.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58105 0 0 0 89871 142 0 0 25 0 1 0 544493956 271056896 56363 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66176 56363 603 41 0 66135 0
vsize: 264704
[startup+910.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58132 0 0 0 90871 142 0 0 25 0 1 0 544493956 271187968 56390 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66208 56390 603 41 0 66167 0
vsize: 264832
[startup+920.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58180 0 0 0 91871 142 0 0 25 0 1 0 544493956 271454208 56438 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66273 56438 603 41 0 66232 0
vsize: 265092
[startup+930.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58255 0 0 0 92871 142 0 0 25 0 1 0 544493956 271728640 56513 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66340 56513 603 41 0 66299 0
vsize: 265360
[startup+940.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58276 0 0 0 93871 142 0 0 25 0 1 0 544493956 271863808 56534 4294967295 134512640 134672761 3221224528 3221223664 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66373 56534 603 41 0 66332 0
vsize: 265492
[startup+950.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58358 0 0 0 94872 143 0 0 25 0 1 0 544493956 272125952 56616 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66437 56616 603 41 0 66396 0
vsize: 265748
[startup+960.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58528 0 0 0 95873 143 0 0 25 0 1 0 544493956 272220160 56665 4294967295 134512640 134672761 3221224528 3221223700 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66460 56665 603 41 0 66419 0
vsize: 265840
[startup+970.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58528 0 0 0 96874 143 0 0 25 0 1 0 544493956 272220160 56665 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66460 56665 603 41 0 66419 0
vsize: 265840
[startup+980.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58553 0 0 0 97874 143 0 0 25 0 1 0 544493956 272351232 56690 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66492 56690 603 41 0 66451 0
vsize: 265968
[startup+990.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58572 0 0 0 98874 143 0 0 25 0 1 0 544493956 272486400 56709 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66525 56709 603 41 0 66484 0
vsize: 266100
[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58593 0 0 0 99874 143 0 0 25 0 1 0 544493956 272486400 56730 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66525 56730 603 41 0 66484 0
vsize: 266100
[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58615 0 0 0 100874 143 0 0 25 0 1 0 544493956 272621568 56752 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66558 56752 603 41 0 66517 0
vsize: 266232
[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58650 0 0 0 101874 144 0 0 25 0 1 0 544493956 272752640 56787 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66590 56787 603 41 0 66549 0
vsize: 266360
[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58686 0 0 0 102874 144 0 0 25 0 1 0 544493956 272887808 56823 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66623 56823 603 41 0 66582 0
vsize: 266492
[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58715 0 0 0 103874 144 0 0 25 0 1 0 544493956 273022976 56852 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66656 56852 603 41 0 66615 0
vsize: 266624
[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58741 0 0 0 104874 144 0 0 25 0 1 0 544493956 273158144 56878 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66689 56878 603 41 0 66648 0
vsize: 266756
[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58847 0 0 0 105874 144 0 0 25 0 1 0 544493956 273580032 56978 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66792 56978 603 41 0 66751 0
vsize: 267168
[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58895 0 0 0 106874 144 0 0 25 0 1 0 544493956 273838080 57026 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66855 57026 603 41 0 66814 0
vsize: 267420
[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 58954 0 0 0 107874 144 0 0 25 0 1 0 544493956 274092032 57085 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66917 57085 603 41 0 66876 0
vsize: 267668
[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 59033 0 0 0 108874 145 0 0 25 0 1 0 544493956 274382848 57164 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66988 57164 603 41 0 66947 0
vsize: 267952
[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 59102 0 0 0 109875 145 0 0 25 0 1 0 544493956 274644992 57233 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67052 57233 603 41 0 67011 0
vsize: 268208
[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 59190 0 0 0 110875 145 0 0 25 0 1 0 544493956 274984960 57321 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67135 57321 603 41 0 67094 0
vsize: 268540
[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 59281 0 0 0 111875 145 0 0 25 0 1 0 544493956 275382272 57412 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67232 57412 603 41 0 67191 0
vsize: 268928
[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 59309 0 0 0 112875 145 0 0 25 0 1 0 544493956 275521536 57440 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67266 57440 603 41 0 67225 0
vsize: 269064
[startup+1140.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 59383 0 0 0 113875 145 0 0 25 0 1 0 544493956 275795968 57514 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67333 57514 603 41 0 67292 0
vsize: 269332
[startup+1150.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 59495 0 0 0 114875 145 0 0 25 0 1 0 544493956 276201472 57626 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67432 57626 603 41 0 67391 0
vsize: 269728
[startup+1160.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 59589 0 0 0 115876 145 0 0 25 0 1 0 544493956 276582400 57720 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67525 57720 603 41 0 67484 0
vsize: 270100
[startup+1170.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 59666 0 0 0 116876 145 0 0 25 0 1 0 544493956 276930560 57797 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67610 57797 603 41 0 67569 0
vsize: 270440
[startup+1180.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 59782 0 0 0 117875 145 0 0 25 0 1 0 544493956 277336064 57913 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67709 57913 603 41 0 67668 0
vsize: 270836
[startup+1190.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 59882 0 0 0 118875 146 0 0 25 0 1 0 544493956 277757952 58013 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67812 58013 603 41 0 67771 0
vsize: 271248
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30172
Raw data (stat): 30115 (minisat+) R 30114 27222 27221 0 -1 0 59987 0 0 0 119875 146 0 0 25 0 1 0 544493956 278175744 58118 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67914 58118 603 41 0 67873 0
vsize: 271656
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 30172
Raw data (stat): 30115 (minisat+) Z 30114 27222 27221 0 -1 12 59990 0 0 0 119876 158 0 0 25 0 1 0 544493956 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.2
CPU time (s): 1200.35
CPU user time (s): 1198.77
CPU system time (s): 1.58076
CPU usage (%): 100.013
Max. virtual memory (Kb): 271656
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####