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/MIPLIB/miplib2003/normalized-mps-v2-13-7-rout.opb
MD5SUM	46c175563919d1fe493ed3da6f49d52f
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1251872
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	33812000
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	166074535
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1585.77
Number of variables	5151
Total number of constraints	606
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	314
Number of constraints which are nor clauses,nor cardinality constraints	292
Minimum length of a constraint	1
Maximum length of a constraint	617
Trace number 15303

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-21 03:49:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17990 boxname=wulflinc24 idbench=1384 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  46c175563919d1fe493ed3da6f49d52f  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-rout.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-rout.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-rout.opb
IDLAUNCH: 17990
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        893176 kB
Buffers:          2200 kB
Cached:         112084 kB
SwapCached:        432 kB
Active:          22148 kB
Inactive:        94284 kB
HighTotal:      131008 kB
HighFree:        19600 kB
LowTotal:       903652 kB
LowFree:        873576 kB
SwapTotal:     2097892 kB
SwapFree:      2096708 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5932 kB
Slab:            19396 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 04:09:11 (client local time) WITH STATUS 10 IN 1200.42 SECONDS
stats: 17990 7 1200.42 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 337 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############################
c   -- Clauses(.)/Splits(s): ...............
c ---[ 320]---> Adder-cost: 3854   maxlim: 97129415   bits: 27/27
c ---[ 319]---> BDD-cost:   37
c ---[ 318]---> BDD-cost:   13
c ---[ 317]---> BDD-cost:   13
c ---[ 316]---> BDD-cost:   25
c ---[ 315]---> BDD-cost:   25
c ---[ 314]---> BDD-cost:   25
c ---[ 313]---> BDD-cost:   25
c ---[ 312]---> BDD-cost:   25
c ---[ 311]---> BDD-cost:   25
c ---[ 310]---> BDD-cost:   25
c ---[ 309]---> BDD-cost:   25
c ---[ 308]---> BDD-cost:   37
c ---[ 307]---> BDD-cost:   25
c ---[ 306]---> BDD-cost:   25
c ---[ 305]---> BDD-cost:   13
c ---[ 304]---> BDD-cost:   13
c ---[ 303]---> BDD-cost:   13
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 299]---> BDD-cost:   13
c ---[ 298]---> BDD-cost:   13
c ---[ 297]---> BDD-cost:   37
c ---[ 296]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 293]---> BDD-cost:   13
c ---[ 292]---> BDD-cost:   13
c ---[ 291]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   13
c ---[ 289]---> BDD-cost:   13
c ---[ 288]---> BDD-cost:   13
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   37
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 281]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 275]---> BDD-cost:   37
c ---[ 274]---> BDD-cost:   13
c ---[ 273]---> BDD-cost:   13
c ---[ 272]---> BDD-cost:   13
c ---[ 271]---> BDD-cost:   13
c ---[ 270]---> BDD-cost:   13
c ---[ 269]---> BDD-cost:   13
c ---[ 268]---> BDD-cost:   13
c ---[ 267]---> BDD-cost:   13
c ---[ 266]---> BDD-cost:   13
c ---[ 265]---> BDD-cost:   13
c ---[ 264]---> BDD-cost:   37
c ---[ 263]---> BDD-cost:   13
c ---[ 262]---> BDD-cost:   13
c ---[ 261]---> BDD-cost:   13
c ---[ 260]---> BDD-cost:   13
c ---[ 259]---> BDD-cost:   13
c ---[ 258]---> BDD-cost:   13
c ---[ 257]---> BDD-cost:   13
c ---[ 256]---> BDD-cost:   13
c ---[ 255]---> BDD-cost:   13
c ---[ 254]---> BDD-cost:   13
c ---[ 253]---> BDD-cost:   37
c ---[ 252]---> BDD-cost:   13
c ---[ 251]---> BDD-cost:   13
c ---[ 250]---> BDD-cost:   13
c ---[ 249]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:   13
c ---[ 247]---> BDD-cost:   13
c ---[ 246]---> BDD-cost:   13
c ---[ 245]---> BDD-cost:   13
c ---[ 244]---> BDD-cost:   13
c ---[ 243]---> BDD-cost:   13
c ---[ 242]---> BDD-cost:   37
c ---[ 241]---> BDD-cost:   13
c ---[ 240]---> BDD-cost:   13
c ---[ 239]---> BDD-cost:   13
c ---[ 238]---> BDD-cost:   13
c ---[ 237]---> BDD-cost:   13
c ---[ 236]---> BDD-cost:   13
c ---[ 235]---> BDD-cost:   13
c ---[ 234]---> BDD-cost:   13
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   13
c ---[ 231]---> BDD-cost:   37
c ---[ 230]---> BDD-cost:   13
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   13
c ---[ 226]---> BDD-cost:   13
c ---[ 225]---> BDD-cost:   13
c ---[ 224]---> BDD-cost:   13
c ---[ 223]---> BDD-cost:   13
c ---[ 222]---> BDD-cost:   13
c ---[ 221]---> BDD-cost:   13
c ---[ 220]---> BDD-cost:   37
c ---[ 219]---> BDD-cost:   13
c ---[ 218]---> BDD-cost:   13
c ---[ 217]---> BDD-cost:   13
c ---[ 216]---> BDD-cost:   13
c ---[ 215]---> BDD-cost:   13
c ---[ 214]---> BDD-cost:   13
c ---[ 213]---> BDD-cost:   13
c ---[ 212]---> BDD-cost:   13
c ---[ 211]---> BDD-cost:   13
c ---[ 210]---> BDD-cost:   13
c ---[ 209]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 208]---> BDD-cost:   37
c ---[ 207]---> BDD-cost:   13
c ---[ 206]---> BDD-cost:   13
c ---[ 205]---> BDD-cost:   13
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   13
c ---[ 202]---> BDD-cost:   13
c ---[ 201]---> BDD-cost:   13
c ---[ 200]---> BDD-cost:   13
c ---[ 199]---> BDD-cost:   13
c ---[ 198]---> BDD-cost:   13
c ---[ 197]---> BDD-cost:   37
c ---[ 196]---> BDD-cost:   13
c ---[ 195]---> BDD-cost:   13
c ---[ 194]---> BDD-cost:   13
c ---[ 193]---> BDD-cost:   13
c ---[ 192]---> BDD-cost:   13
c ---[ 191]---> BDD-cost:   13
c ---[ 190]---> BDD-cost:   13
c ---[ 189]---> BDD-cost:   13
c ---[ 188]---> BDD-cost:   13
c ---[ 187]---> BDD-cost:   13
c ---[ 185]---> Sorter-cost:  441     Base: 2
c ---[ 184]---> BDD-cost:   13
c ---[ 183]---> BDD-cost:   13
c ---[ 182]---> BDD-cost:   13
c ---[ 181]---> BDD-cost:   13
c ---[ 180]---> BDD-cost:   13
c ---[ 179]---> BDD-cost:   13
c ---[ 178]---> BDD-cost:   13
c ---[ 177]---> BDD-cost:   13
c ---[ 176]---> BDD-cost:   13
c ---[ 175]---> BDD-cost:   13
c ---[ 173]---> Sorter-cost:  441     Base: 2
c ---[ 172]---> BDD-cost:   13
c ---[ 171]---> BDD-cost:   13
c ---[ 170]---> BDD-cost:   13
c ---[ 169]---> BDD-cost:   13
c ---[ 168]---> BDD-cost:   13
c ---[ 167]---> BDD-cost:   13
c ---[ 166]---> BDD-cost:   13
c ---[ 165]---> BDD-cost:   13
c ---[ 164]---> BDD-cost:   13
c ---[ 163]---> BDD-cost:   13
c ---[ 161]---> Sorter-cost:  441     Base: 2
c ---[ 160]---> BDD-cost:   13
c ---[ 159]---> BDD-cost:   13
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   13
c ---[ 156]---> BDD-cost:   13
c ---[ 155]---> BDD-cost:   13
c ---[ 154]---> BDD-cost:   13
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   13
c ---[ 151]---> BDD-cost:   13
c ---[ 149]---> Sorter-cost:  441     Base: 2
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   13
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   13
c ---[ 143]---> BDD-cost:   13
c ---[ 142]---> BDD-cost:   13
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:   13
c ---[ 139]---> BDD-cost:   13
c ---[ 137]---> Sorter-cost:  441     Base: 2
c ---[ 136]---> BDD-cost:   13
c ---[ 135]---> BDD-cost:   13
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   13
c ---[ 132]---> BDD-cost:   13
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   13
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   13
c ---[ 127]---> BDD-cost:   13
c ---[ 125]---> Sorter-cost:  347     Base: 2
c ---[ 124]---> BDD-cost:   13
c ---[ 123]---> BDD-cost:   13
c ---[ 122]---> BDD-cost:   13
c ---[ 121]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   13
c ---[ 119]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   13
c ---[ 113]---> Sorter-cost:  347     Base: 2
c ---[ 112]---> BDD-cost:   13
c ---[ 111]---> BDD-cost:   13
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   13
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   13
c ---[ 103]---> BDD-cost:   13
c ---[ 101]---> Sorter-cost:  347     Base: 2
c ---[ 100]---> BDD-cost:   13
c ---[  99]---> BDD-cost:   13
c ---[  98]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  96]---> Sorter-cost:  347     Base: 2
c ---[  94]---> Sorter-cost:  347     Base: 2
c ---[  92]---> Sorter-cost:  515     Base: 2
c ---[  90]---> Sorter-cost:  515     Base: 2
c ---[  88]---> Sorter-cost:  515     Base: 2
c ---[  86]---> Sorter-cost:  515     Base: 2
c ---[  84]---> Sorter-cost:  515     Base: 2
c ---[  82]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[  80]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[  78]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[  77]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  75]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[  73]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[  71]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[  69]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[  67]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[  65]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[  63]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[  61]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  59]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  57]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  56]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  54]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  52]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  51]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   13
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   13
c ---[  45]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   13
c ---[  43]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  42]---> BDD-cost:   13
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   13
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   13
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   13
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   13
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   13
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   13
c ---[  16]---> BDD-cost:   13
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   84
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   13
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  126296   425585 |   37888       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24269          
c   -- var.elim.:  2000/24269          
c   -- var.elim.:  3000/24269          
c   -- var.elim.:  4000/24269          
c   -- var.elim.:  5000/24269          
c   -- var.elim.:  6000/24269          
c   -- var.elim.:  7000/24269          
c   -- var.elim.:  8000/24269          
c   -- var.elim.:  9000/24269          
c   -- var.elim.:  10000/24269          
c   -- var.elim.:  11000/24269          
c   -- var.elim.:  12000/24269          
c   -- var.elim.:  13000/24269          
c   -- var.elim.:  14000/24269          
c   -- var.elim.:  15000/24269          
c   -- var.elim.:  16000/24269          
c   -- var.elim.:  17000/24269          
c   -- var.elim.:  18000/24269          
c   -- var.elim.:  19000/24269          
c   -- var.elim.:  20000/24269          
c   -- var.elim.:  21000/24269          
c   -- var.elim.:  22000/24269          
c   -- var.elim.:  23000/24269          
c   -- var.elim.:  24000/24269          
c   -- var.elim.:  24269/24269          
c   -- var.elim.:  1000/5473          
c   -- var.elim.:  2000/5473          
c   -- var.elim.:  3000/5473          
c   -- var.elim.:  4000/5473          
c   -- var.elim.:  5000/5473          
c   -- var.elim.:  5473/5473          
c   -- var.elim.:  145/145          
c   -- subsuming                       
c   -- var.elim.:  1000/2127          
c   -- var.elim.:  2000/2127          
c   -- var.elim.:  2127/2127          
c   -- var.elim.:  1000/1452          
c   -- var.elim.:  1452/1452          
c   -- subsuming                       
c   -- var.elim.:  230/230          
c   -- var.elim.:  70/70          
c |         0 |  119705   411866 |      --       0       --      -- |     --   | -4982/-5033
c |         0 |  119705   411866 |   47882       0        0     nan |  0.000 % |
c |       100 |  119487   411160 |   52574      89      575     6.5 | 15.028 % |
c |       250 |  119245   410392 |   57714     224     6687    29.9 | 15.200 % |
c |       476 |  119245   410392 |   63486     450    12875    28.6 | 15.200 % |
c |       813 |  118917   409337 |   69642     736    19484    26.5 | 15.433 % |
c |      1320 |  118917   409337 |   76606    1243    47231    38.0 | 15.433 % |
c |      2079 |  118804   408972 |   84187    1999    63096    31.6 | 15.515 % |
c |      3218 |  118746   408757 |   92560    3134    99895    31.9 | 15.540 % |
c |      4927 |  118746   408757 |  101817    4843   289733    59.8 | 15.540 % |
c |      7490 |  117737   405516 |  111047    7366   594677    80.7 | 16.249 % |
c |     11335 |  116864   402234 |  121246   11051   874928    79.2 | 16.597 % |
c ==============================================================================
c (current CPU-time: 39.521 s)
c ==============================================================================
c [1mFound solution: 1269376[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     12608 |  116877   402268 |   35063   12324  1077926    87.5 | 16.597 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1247          
c   -- var.elim.:  1247/1247          
c   -- var.elim.:  518/518          
c   -- var.elim.:  77/77          
c   -- var.elim.:  18/18          
c   -- subsuming                       
c   -- var.elim.:  57/57          
c   -- var.elim.:  7/7          
c |     12608 |  116609   401633 |      --   12324       --      -- |     --   | -268/-634
c |     12608 |  116609   401633 |   46643   10518   651552    61.9 | 16.597 % |
c |     12708 |  116569   401499 |   51290   10616   652480    61.5 | 16.759 % |
c |     12859 |  116450   401110 |   56361   10764   660524    61.4 | 16.837 % |
c |     13086 |  116409   400962 |   61976   10975   670627    61.1 | 16.862 % |
c |     13423 |  116409   400962 |   68173   11312   699633    61.8 | 16.862 % |
c |     13929 |  116177   400181 |   74841   11800   718177    60.9 | 17.002 % |
c |     14688 |  116177   400181 |   82325   12559   770788    61.4 | 17.002 % |
c |     15827 |  116163   400122 |   90547   13686   807109    59.0 | 17.006 % |
c |     17535 |  115677   398613 |   99185   15380   949093    61.7 | 17.376 % |
c |     20098 |  115605   398370 |  109036   17897  1041001    58.2 | 17.422 % |
c |     23943 |  115605   398370 |  119939   21742  1623188    74.7 | 17.422 % |
c |     29714 |  115409   397717 |  131710   27503  1932357    70.3 | 17.549 % |
c |     38365 |  115058   396571 |  144440   36131  3019374    83.6 | 17.797 % |
c ==============================================================================
c (current CPU-time: 90.8182 s)
c ==============================================================================
c [1mFound solution: 1268352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     44501 |  114541   394578 |   34362   42202  3519196    83.4 | 17.797 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1228          
c   -- var.elim.:  1228/1228          
c   -- var.elim.:  500/500          
c   -- var.elim.:  23/23          
c   -- subsuming                       
c   -- var.elim.:  81/81          
c   -- var.elim.:  37/37          
c |     44501 |  114384   394267 |      --   42202       --      -- |     --   | -157/-310
c |     44501 |  114384   394267 |   45753   32950  1996700    60.6 | 17.797 % |
c |     44602 |  114344   394105 |   50311   33049  2000255    60.5 | 18.073 % |
c |     44753 |  114344   394105 |   55342   33200  2020581    60.9 | 18.073 % |
c |     44979 |  114344   394105 |   60876   33426  2047258    61.2 | 18.073 % |
c |     45320 |  114189   393602 |   66873   33759  2056246    60.9 | 18.172 % |
c |     45827 |  114189   393602 |   73561   34266  2074565    60.5 | 18.172 % |
c |     46587 |  114189   393602 |   80917   35026  2107861    60.2 | 18.172 % |
c |     47730 |  114158   393470 |   88984   36159  2228376    61.6 | 18.177 % |
c ==============================================================================
c (current CPU-time: 99.2199 s)
c ==============================================================================
c [1mFound solution: 1265824[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   15
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     48457 |  114177   393514 |   34253   36886  2280122    61.8 | 18.177 % |
c   -- subsuming                       
c   -- var.elim.:  207/207          
c   -- var.elim.:  96/96          
c   -- subsuming                       
c   -- var.elim.:  17/17          
c   -- var.elim.:  9/9          
c |     48457 |  114133   393410 |      --   36886       --      -- |     --   | -44/-103
c |     48457 |  114133   393410 |   45653   36499  2222667    60.9 | 18.177 % |
c |     48559 |  114075   393219 |   50193   36599  2224868    60.8 | 18.231 % |
c |     48709 |  114075   393219 |   55212   36749  2229531    60.7 | 18.231 % |
c |     48936 |  113991   392906 |   60688   36973  2236055    60.5 | 18.276 % |
c |     49273 |  113991   392906 |   66757   37310  2273133    60.9 | 18.276 % |
c |     49782 |  113991   392906 |   73433   37819  2308509    61.0 | 18.276 % |
c |     50544 |  113991   392906 |   80776   38581  2411059    62.5 | 18.276 % |
c |     51683 |  113657   391591 |   88594   39685  2493268    62.8 | 18.355 % |
c |     53391 |  113638   391525 |   97437   41378  2691896    65.1 | 18.363 % |
c |     55953 |  112446   387008 |  106056   43727  2807923    64.2 | 18.810 % |
c |     59797 |  112437   386975 |  116653   47530  3581630    75.4 | 18.814 % |
c ==============================================================================
c (current CPU-time: 139.859 s)
c ==============================================================================
c [1mFound solution: 1244736[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   14
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     64046 |  112244   386293 |   33673   51745  4290185    82.9 | 18.814 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1096          
c   -- var.elim.:  1096/1096          
c   -- var.elim.:  461/461          
c   -- var.elim.:  8/8          
c   -- subsuming                       
c   -- var.elim.:  60/60          
c   -- var.elim.:  43/43          
c |     64046 |  112044   385568 |      --   51745       --      -- |     --   | -200/-724
c |     64046 |  112044   385568 |   44817   45418  2648974    58.3 | 18.814 % |
c |     64146 |  112037   385549 |   49296   45517  2656990    58.4 | 19.033 % |
c |     64297 |  112037   385549 |   54225   45668  2672308    58.5 | 19.033 % |
c |     64522 |  112037   385549 |   59648   45893  2691628    58.7 | 19.033 % |
c |     64859 |  111993   385394 |   65587   46226  2697542    58.4 | 19.058 % |
c |     65370 |  111993   385394 |   72146   46737  2811160    60.1 | 19.058 % |
c |     66130 |  111993   385394 |   79360   47497  2864055    60.3 | 19.058 % |
c |     67269 |  111993   385394 |   87297   48636  2912248    59.9 | 19.058 % |
c |     68977 |  111805   384682 |   95865   50335  3430421    68.2 | 19.116 % |
c |     71539 |  111615   383943 |  105272   52869  3794221    71.8 | 19.179 % |
c |     75385 |  111568   383762 |  115751   56635  4649078    82.1 | 19.195 % |
c |     81151 |  111568   383762 |  127326   62401  5069383    81.2 | 19.195 % |
c |     89801 |  111551   383699 |  140037   71047  6901408    97.1 | 19.204 % |
c |    102776 |  111270   382726 |  153653   83927 11309515   134.8 | 19.341 % |
c |    122239 |  111002   381714 |  168611  103322 16200282   156.8 | 19.441 % |
c |    151431 |  110417   379575 |  184495  132130 26719575   202.2 | 19.694 % |
c ==============================================================================
c (current CPU-time: 499.606 s)
c ==============================================================================
c [1mFound solution: 1235424[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   15
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    164287 |  109933   377764 |   32979  144876 30476097   210.4 | 19.694 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1143          
c   -- var.elim.:  1143/1143          
c   -- var.elim.:  574/574          
c   -- subsuming                       
c   -- var.elim.:  79/79          
c   -- var.elim.:  35/35          
c |    164287 |  109688   376998 |      --  144876       --      -- |     --   | -245/-765
c |    164287 |  109688   376998 |   43875  114696 10175317    88.7 | 19.694 % |
c |    164389 |  109656   376869 |   48248   20682  1033513    50.0 | 20.044 % |
c |    164539 |  109656   376869 |   53073   20832  1035514    49.7 | 20.044 % |
c |    164764 |  109656   376869 |   58380   21057  1046404    49.7 | 20.044 % |
c |    165102 |  109656   376869 |   64218   21395  1241406    58.0 | 20.044 % |
c |    165608 |  109656   376869 |   70640   21901  1309233    59.8 | 20.044 % |
c |    166367 |  109416   375941 |   77534   22647  1376047    60.8 | 20.127 % |
c |    167506 |  109298   375500 |   85196   23749  1533377    64.6 | 20.161 % |
c |    169216 |  109298   375500 |   93715   25459  1608180    63.2 | 20.161 % |
c |    171778 |  109132   374869 |  102931   27999  2047359    73.1 | 20.211 % |
c |    175623 |  109132   374869 |  113224   31844  2837453    89.1 | 20.211 % |
c |    181390 |  109075   374652 |  124481   37601  4546209   120.9 | 20.232 % |
c |    190040 |  108990   374354 |  136822   46226  6616704   143.1 | 20.274 % |
c |    203014 |  108849   373835 |  150310   59193 10413530   175.9 | 20.336 % |
c |    222475 |  108488   372667 |  164793   78409 17113322   218.3 | 20.596 % |
c |    251668 |  108279   371893 |  180923  107574 27073643   251.7 | 20.675 % |
c |    295462 |  108265   371834 |  198989  151364 42288745   279.4 | 20.679 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -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 x241_bit13 -x242_bit0 -x243_bit0 x244_bit0 -x245_bit0 x246_bit0 x247_bit0 x248_bit0 -x249_bit0 -x250_bit0 -x251_bit0 -x252_bit0 -x253_bit0 -x254_bit0 x255_bit0 -x256_bit0 -x257_bit0 -x258_bit0 x259_bit0 -x260_bit0 -x261_bit0 -x262_bit0 -x263_bit0 -x264_bit0 -x265_bit0 -x266_bit0 -x267_bit0 -x268_bit0 -x269_bit0 -x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 -x275_bit0 -x276_bit0 -x277_bit0 -x278_bit0 -x279_bit0 -x280_bit0 -x281_bit0 -x282_bit0 -x283_bit0 -x284_bit0 -x285_bit0 -x286_bit0 -x287_bit0 x288_bit0 -x289_bit0 -x290_bit0 -x291_bit0 -x292_bit0 -x293_bit0 -x294_bit0 -x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 -x299_bit0 -x300_bit0 -x301_bit0 -x302_bit0 -x302_bit1 -x303_bit0 -x303_bit1 -x304_bit0 -x304_bit1 -x305_bit0 -x305_bit1 -x306_bit0 -x306_bit1 -x307_bit0 -x307_bit1 -x308_bit0 -x308_bit1 -x309_bit0 -x309_bit1 -x310_bit0 -x310_bit1 -x311_bit0 -x311_bit1 -x312_bit0 -x312_bit1 -x313_bit0 -x313_bit1 x314_bit0 -x314_bit1 -x315_bit0 -x315_bit1 -x316_bit0 -x316_bit1 -x317_bit0 -x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 -x333_bit0 -x334_bit0 x335_bit0 -x336_bit0 -x337_bit0 -x338_bit0 -x339_bit0 -x340_bit0 -x341_bit0 -x342_bit0 -x343_bit0 -x344_bit0 -x345_bit0 -x346_bit0 -x347_bit0 -x348_bit0 -x349_bit0 -x350_bit0 -x351_bit0 -x352_bit0 -x353_bit0 -x354_bit0 x355_bit0 -x356_bit0 x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 -x366_bit0 -x367_bit0 -x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 -x373_bit0 -x374_bit0 -x375_bit0 -x376_bit0 -x377_bit0 -x378_bit0 -x379_bit0 -x380_bit0 -x381_bit0 -x382_bit0 x383_bit0 -x384_bit0 -x385_bit0 -x386_bit0 -x387_bit0 -x388_bit0 -x389_bit0 -x390_bit0 -x391_bit0 -x392_bit0 -x393_bit0 -x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 -x399_bit0 -x400_bit0 -x401_bit0 -x402_bit0 -x403_bit0 -x404_bit0 -x405_bit0 -x406_bit0 -x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0 x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 -x416_bit0 -x417_bit0 -x418_bit0 -x419_bit0 -x420_bit0 -x421_bit0 -x422_bit0 -x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x427_bit0 -x428_bit0 -x429_bit0 -x430_bit0 -x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 -x436_bit0 -x437_bit0 -x438_bit0 -x439_bit0 -x440_bit0 x441_bit0 -x442_bit0 -x443_bit0 -x444_bit0 -x445_bit0 -x446_bit0 -x447_bit0 -x448_bit0 -x449_bit0 -x450_bit0 -x451_bit0 -x452_bit0 -x453_bit0 -x454_bit0 -x455_bit0 -x456_bit0 -x457_bit0 -x458_bit0 -x459_bit0 -x460_bit0 -x461_bit0 -x462_bit0 -x463_bit0 -x464_bit0 -x465_bit0 -x466_bit0 -x467_bit0 -x468_bit0 -x469_bit0 -x470_bit0 -x471_bit0 -x472_bit0 -x473_bit0 -x474_bit0 -x475_bit0 x476_bit0 -x477_bit0 -x478_bit0 -x479_bit0 -x480_bit0 -x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 -x485_bit0 x486_bit0 -x487_bit0 -x488_bit0 -x489_bit0 -x490_bit0 -x491_bit0 -x492_bit0 -x493_bit0 -x494_bit0 -x495_bit0 -x496_bit0 -x497_bit0 x498_bit0 -x499_bit0 -x500_bit0 -x501_bit0 -x502_bit0 -x503_bit0 -x504_bit0 -x505_bit0 -x506_bit0 -x507_bit0 -x508_bit0 -x509_bit0 -x510_bit0 -x511_bit0 -x512_bit0 -x513_bit0 -x514_bit0 -x515_bit0 -x516_bit0 -x517_bit0 -x518_bit0 -x519_bit0 -x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 -x524_bit0 -x525_bit0 -x526_bit0 -x527_bit0 -x528_bit0 -x529_bit0 -x530_bit0 -x531_bit0 -x532_bit0 -x533_bit0 x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 x540_bit0 -x541_bit0 -x542_bit0 -x543_bit0 -x544_bit0 -x545_bit0 -x546_bit0 -x547_bit0 -x548_bit0 -x549_bit0 -x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 -x556_bit0 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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#### 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.84 0.94 0.90 2/54 23848
Raw data (stat): 23848 (runsolver) R 23847 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541961434 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 1138 0 0 0 996 3 0 0 25 0 1 0 541961434 5230592 826 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1277 826 603 41 0 1236 0
vsize: 5108
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 6402 0 0 0 1982 16 0 0 25 0 1 0 541961434 23928832 5241 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5842 5241 603 41 0 5801 0
vsize: 23368
[startup+30.0012 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 6918 0 0 0 2981 17 0 0 25 0 1 0 541961434 26050560 5757 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6360 5757 603 41 0 6319 0
vsize: 25440
[startup+40.0005 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 8437 0 0 0 3977 22 0 0 25 0 1 0 541961434 30105600 6716 4294967295 134512640 134672761 3221224544 3221222816 134565566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7350 6716 603 41 0 7309 0
vsize: 29400
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 8571 0 0 0 4977 22 0 0 25 0 1 0 541961434 30105600 6721 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7350 6721 603 41 0 7309 0
vsize: 29400
[startup+60.0012 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 8946 0 0 0 5976 23 0 0 25 0 1 0 541961434 31539200 7096 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7700 7096 603 41 0 7659 0
vsize: 30800
[startup+70.0006 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 9388 0 0 0 6974 25 0 0 25 0 1 0 541961434 33390592 7538 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8152 7538 603 41 0 8111 0
vsize: 32608
[startup+80.0017 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 10248 0 0 0 7972 27 0 0 25 0 1 0 541961434 36954112 8398 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9022 8398 603 41 0 8981 0
vsize: 36088
[startup+90.0013 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 10863 0 0 0 8971 29 0 0 25 0 1 0 541961434 39469056 9013 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9636 9013 603 41 0 9595 0
vsize: 38544
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 13036 0 0 0 9964 35 0 0 25 0 1 0 541961434 41017344 9408 4294967295 134512640 134672761 3221224544 3221223800 134616132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10014 9408 603 41 0 9973 0
vsize: 40056
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 13036 0 0 0 10965 35 0 0 25 0 1 0 541961434 41017344 9408 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10014 9408 603 41 0 9973 0
vsize: 40056
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 13041 0 0 0 11965 35 0 0 25 0 1 0 541961434 41017344 9413 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10014 9413 603 41 0 9973 0
vsize: 40056
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 13137 0 0 0 12965 35 0 0 25 0 1 0 541961434 41398272 9509 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10107 9509 603 41 0 10066 0
vsize: 40428
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 13646 0 0 0 13964 37 0 0 25 0 1 0 541961434 43483136 10018 4294967295 134512640 134672761 3221224544 3221223536 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10616 10018 603 41 0 10575 0
vsize: 42464
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 14957 0 0 0 14960 40 0 0 25 0 1 0 541961434 44584960 10288 4294967295 134512640 134672761 3221224544 3221223584 134612978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10885 10288 603 41 0 10844 0
vsize: 43540
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 14959 0 0 0 15960 40 0 0 25 0 1 0 541961434 44584960 10290 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10885 10290 603 41 0 10844 0
vsize: 43540
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 15132 0 0 0 16960 41 0 0 25 0 1 0 541961434 45367296 10463 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11076 10463 603 41 0 11035 0
vsize: 44304
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 15677 0 0 0 17959 41 0 0 25 0 1 0 541961434 47476736 11008 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11591 11008 603 41 0 11550 0
vsize: 46364
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 16743 0 0 0 18958 43 0 0 25 0 1 0 541961434 52154368 12074 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12733 12074 603 41 0 12692 0
vsize: 50932
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 17633 0 0 0 19956 45 0 0 25 0 1 0 541961434 55840768 12964 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13633 12964 603 41 0 13592 0
vsize: 54532
[startup+210.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 18812 0 0 0 20954 48 0 0 25 0 1 0 541961434 60620800 14143 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14800 14143 603 41 0 14759 0
vsize: 59200
[startup+220.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 20205 0 0 0 21951 51 0 0 25 0 1 0 541961434 66318336 15536 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16191 15536 603 41 0 16150 0
vsize: 64764
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 20653 0 0 0 22950 52 0 0 25 0 1 0 541961434 68161536 15984 4294967295 134512640 134672761 3221224544 3221223584 134614348 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16641 15984 603 41 0 16600 0
vsize: 66564
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 21360 0 0 0 23948 54 0 0 25 0 1 0 541961434 71045120 16691 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17345 16691 603 41 0 17304 0
vsize: 69380
[startup+250.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 22404 0 0 0 24948 56 0 0 25 0 1 0 541961434 75239424 17735 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18369 17735 603 41 0 18328 0
vsize: 73476
[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 23568 0 0 0 25946 59 0 0 25 0 1 0 541961434 79953920 18899 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19520 18899 603 41 0 19479 0
vsize: 78080
[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 24650 0 0 0 26944 61 0 0 25 0 1 0 541961434 84393984 19981 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20604 19981 603 41 0 20563 0
vsize: 82416
[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 25469 0 0 0 27942 63 0 0 25 0 1 0 541961434 87797760 20800 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21435 20800 603 41 0 21394 0
vsize: 85740
[startup+290.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 25985 0 0 0 28941 64 0 0 25 0 1 0 541961434 89845760 21316 4294967295 134512640 134672761 3221224544 3221223688 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21935 21316 603 41 0 21894 0
vsize: 87740
[startup+300.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 26574 0 0 0 29941 66 0 0 25 0 1 0 541961434 92217344 21905 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22514 21905 603 41 0 22473 0
vsize: 90056
[startup+310.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 27167 0 0 0 30939 68 0 0 25 0 1 0 541961434 94683136 22498 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23116 22498 603 41 0 23075 0
vsize: 92464
[startup+320.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 27864 0 0 0 31938 70 0 0 25 0 1 0 541961434 97566720 23195 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23820 23195 603 41 0 23779 0
vsize: 95280
[startup+330.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 28238 0 0 0 32938 71 0 0 25 0 1 0 541961434 99020800 23569 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24175 23569 603 41 0 24134 0
vsize: 96700
[startup+340.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 28941 0 0 0 33937 72 0 0 25 0 1 0 541961434 101871616 24272 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24871 24272 603 41 0 24830 0
vsize: 99484
[startup+350.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 29379 0 0 0 34936 73 0 0 25 0 1 0 541961434 103714816 24710 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25321 24710 603 41 0 25280 0
vsize: 101284
[startup+360.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 30169 0 0 0 35935 76 0 0 25 0 1 0 541961434 106991616 25500 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26121 25500 603 41 0 26080 0
vsize: 104484
[startup+370.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 31232 0 0 0 36933 78 0 0 25 0 1 0 541961434 111239168 26563 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27158 26563 603 41 0 27117 0
vsize: 108632
[startup+380.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 32392 0 0 0 37930 81 0 0 25 0 1 0 541961434 115994624 27723 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28319 27723 603 41 0 28278 0
vsize: 113276
[startup+390.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 33728 0 0 0 38927 83 0 0 25 0 1 0 541961434 121548800 29059 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29675 29059 603 41 0 29634 0
vsize: 118700
[startup+400.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 34390 0 0 0 39927 85 0 0 25 0 1 0 541961434 124203008 29721 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30323 29721 603 41 0 30282 0
vsize: 121292
[startup+410.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 35351 0 0 0 40926 86 0 0 25 0 1 0 541961434 128090112 30682 4294967295 134512640 134672761 3221224544 3221223552 134522368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31272 30682 603 41 0 31231 0
vsize: 125088
[startup+420.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 36714 0 0 0 41923 89 0 0 25 0 1 0 541961434 133685248 32045 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32638 32045 603 41 0 32597 0
vsize: 130552
[startup+430.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 37430 0 0 0 42921 91 0 0 25 0 1 0 541961434 137109504 32761 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33474 32761 603 41 0 33433 0
vsize: 133896
[startup+440.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 37923 0 0 0 43919 93 0 0 25 0 1 0 541961434 139198464 33254 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33984 33254 603 41 0 33943 0
vsize: 135936
[startup+450.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 38390 0 0 0 44919 94 0 0 25 0 1 0 541961434 141041664 33721 4294967295 134512640 134672761 3221224544 3221223584 134614258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34434 33721 603 41 0 34393 0
vsize: 137736
[startup+460.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 39002 0 0 0 45917 95 0 0 25 0 1 0 541961434 143532032 34333 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35042 34333 603 41 0 35001 0
vsize: 140168
[startup+470.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 39255 0 0 0 46917 96 0 0 25 0 1 0 541961434 144556032 34586 4294967295 134512640 134672761 3221224544 3221223688 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35292 34586 603 41 0 35251 0
vsize: 141168
[startup+480.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 39750 0 0 0 47916 97 0 0 25 0 1 0 541961434 146640896 35081 4294967295 134512640 134672761 3221224544 3221223688 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35801 35081 603 41 0 35760 0
vsize: 143204
[startup+490.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 40624 0 0 0 48914 100 0 0 25 0 1 0 541961434 150228992 35955 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36677 35955 603 41 0 36636 0
vsize: 146708
[startup+500.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 41593 0 0 0 49911 102 0 0 25 0 1 0 541961434 154222592 36924 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37652 36924 603 41 0 37611 0
vsize: 150608
[startup+510.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43072 0 0 0 50906 107 0 0 25 0 1 0 541961434 155947008 37357 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38073 37357 603 41 0 38032 0
vsize: 152292
[startup+520.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43072 0 0 0 51905 107 0 0 25 0 1 0 541961434 155947008 37357 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38073 37357 603 41 0 38032 0
vsize: 152292
[startup+530.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43072 0 0 0 52905 107 0 0 25 0 1 0 541961434 155947008 37357 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37357 603 41 0 38032 0
vsize: 152292
[startup+540.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43072 0 0 0 53905 107 0 0 25 0 1 0 541961434 155947008 37357 4294967295 134512640 134672761 3221224544 3221223704 134614477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37357 603 41 0 38032 0
vsize: 152292
[startup+550.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 54905 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+560.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 55906 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+570.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 56906 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+580.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 57906 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+590.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 58906 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+600.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 59906 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223584 134612885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+610.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 60906 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+620.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 61907 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223688 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+630.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 62907 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+640.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 63907 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223496 1075347133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+650.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23848
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 64907 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223720 134615853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+660.078 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 23901
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 65907 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+670.079 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 23901
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 66907 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+680.08 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 23901
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 67907 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+690.079 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 23901
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 68907 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+700.08 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 23901
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 69907 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+710.081 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 23901
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 70908 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+720.08 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 23901
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 71908 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+730.081 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 72908 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223688 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+740.081 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 73908 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+750.082 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 74909 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+760.082 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 75909 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+770.082 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 76909 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+780.082 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 77909 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+790.082 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 78909 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223688 134616178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+800.083 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 79909 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+810.084 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 80910 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+820.084 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43073 0 0 0 81910 107 0 0 25 0 1 0 541961434 155947008 37358 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37358 603 41 0 38032 0
vsize: 152292
[startup+830.084 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 43916 0 0 0 82908 109 0 0 25 0 1 0 541961434 159477760 38201 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38935 38201 603 41 0 38894 0
vsize: 155740
[startup+840.084 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 44904 0 0 0 83906 112 0 0 25 0 1 0 541961434 163524608 39189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39923 39189 603 41 0 39882 0
vsize: 159692
[startup+850.084 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 45756 0 0 0 84904 114 0 0 25 0 1 0 541961434 167051264 40041 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40784 40041 603 41 0 40743 0
vsize: 163136
[startup+860.084 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 46641 0 0 0 85902 116 0 0 25 0 1 0 541961434 170610688 40926 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41653 40926 603 41 0 41612 0
vsize: 166612
[startup+870.084 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 47098 0 0 0 86900 118 0 0 25 0 1 0 541961434 172453888 41383 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42103 41383 603 41 0 42062 0
vsize: 168412
[startup+880.085 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 47555 0 0 0 87898 120 0 0 25 0 1 0 541961434 174440448 41840 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42588 41840 603 41 0 42547 0
vsize: 170352
[startup+890.085 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 48312 0 0 0 88896 122 0 0 25 0 1 0 541961434 177463296 42597 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43326 42597 603 41 0 43285 0
vsize: 173304
[startup+900.091 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 49251 0 0 0 89895 124 0 0 25 0 1 0 541961434 181334016 43536 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44271 43536 603 41 0 44230 0
vsize: 177084
[startup+910.091 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 49915 0 0 0 90894 126 0 0 25 0 1 0 541961434 184074240 44200 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44940 44200 603 41 0 44899 0
vsize: 179760
[startup+920.091 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 50800 0 0 0 91892 128 0 0 25 0 1 0 541961434 187707392 45085 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45827 45085 603 41 0 45786 0
vsize: 183308
[startup+930.092 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 51529 0 0 0 92890 130 0 0 25 0 1 0 541961434 190709760 45814 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46560 45814 603 41 0 46519 0
vsize: 186240
[startup+940.092 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 52219 0 0 0 93888 132 0 0 25 0 1 0 541961434 193449984 46504 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47229 46504 603 41 0 47188 0
vsize: 188916
[startup+950.091 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 53114 0 0 0 94886 134 0 0 25 0 1 0 541961434 197201920 47399 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48145 47399 603 41 0 48104 0
vsize: 192580
[startup+960.092 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 54381 0 0 0 95884 137 0 0 25 0 1 0 541961434 202379264 48666 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49409 48666 603 41 0 49368 0
vsize: 197636
[startup+970.093 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 54705 0 0 0 96883 138 0 0 25 0 1 0 541961434 203698176 48990 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49731 48990 603 41 0 49690 0
vsize: 198924
[startup+980.093 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 55454 0 0 0 97881 140 0 0 25 0 1 0 541961434 206675968 49739 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50458 49739 603 41 0 50417 0
vsize: 201832
[startup+990.093 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 55940 0 0 0 98880 141 0 0 25 0 1 0 541961434 208654336 50225 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50941 50225 603 41 0 50900 0
vsize: 203764
[startup+1000.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 57314 0 0 0 99877 144 0 0 25 0 1 0 541961434 214302720 51599 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52320 51599 603 41 0 52279 0
vsize: 209280
[startup+1010.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 58710 0 0 0 100874 148 0 0 25 0 1 0 541961434 220012544 52995 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53714 52995 603 41 0 53673 0
vsize: 214856
[startup+1020.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23903
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 60211 0 0 0 101871 151 0 0 25 0 1 0 541961434 226160640 54496 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55215 54496 603 41 0 55174 0
vsize: 220860
[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 61281 0 0 0 102869 153 0 0 25 0 1 0 541961434 230563840 55566 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56290 55566 603 41 0 56249 0
vsize: 225160
[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 62432 0 0 0 103865 157 0 0 25 0 1 0 541961434 235298816 56717 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57446 56717 603 41 0 57405 0
vsize: 229784
[startup+1050.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 63291 0 0 0 104863 159 0 0 25 0 1 0 541961434 238804992 57576 4294967295 134512640 134672761 3221224544 3221223552 134522542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58302 57576 603 41 0 58261 0
vsize: 233208
[startup+1060.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 64469 0 0 0 105862 161 0 0 25 0 1 0 541961434 243519488 58754 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59453 58754 603 41 0 59412 0
vsize: 237812
[startup+1070.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 65150 0 0 0 106860 163 0 0 25 0 1 0 541961434 246378496 59435 4294967295 134512640 134672761 3221224544 3221223728 134615734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60151 59435 603 41 0 60110 0
vsize: 240604
[startup+1080.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 65967 0 0 0 107858 165 0 0 25 0 1 0 541961434 249683968 60252 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60958 60252 603 41 0 60917 0
vsize: 243832
[startup+1090.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 66705 0 0 0 108857 166 0 0 25 0 1 0 541961434 252755968 60990 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61708 60990 603 41 0 61667 0
vsize: 246832
[startup+1100.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 67753 0 0 0 109855 168 0 0 25 0 1 0 541961434 257048576 62038 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62756 62038 603 41 0 62715 0
vsize: 251024
[startup+1110.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 68887 0 0 0 110854 170 0 0 25 0 1 0 541961434 261595136 63172 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63866 63172 603 41 0 63825 0
vsize: 255464
[startup+1120.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 70173 0 0 0 111851 173 0 0 25 0 1 0 541961434 266870784 64458 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65154 64458 603 41 0 65113 0
vsize: 260616
[startup+1130.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 71050 0 0 0 112849 175 0 0 25 0 1 0 541961434 270442496 65335 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66026 65335 603 41 0 65985 0
vsize: 264104
[startup+1140.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 71804 0 0 0 113848 176 0 0 25 0 1 0 541961434 273547264 66089 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66784 66089 603 41 0 66743 0
vsize: 267136
[startup+1150.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 72505 0 0 0 114847 178 0 0 25 0 1 0 541961434 276471808 66790 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67498 66790 603 41 0 67457 0
vsize: 269992
[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 72967 0 0 0 115846 179 0 0 25 0 1 0 541961434 278306816 67252 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67946 67252 603 41 0 67905 0
vsize: 271784
[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 73742 0 0 0 116844 181 0 0 25 0 1 0 541961434 281456640 68027 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68715 68027 603 41 0 68674 0
vsize: 274860
[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 75332 0 0 0 117841 184 0 0 25 0 1 0 541961434 288034816 69617 4294967295 134512640 134672761 3221224544 3221223728 134615994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70321 69617 603 41 0 70280 0
vsize: 281284
[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 76513 0 0 0 118838 187 0 0 25 0 1 0 541961434 292769792 70798 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71477 70798 603 41 0 71436 0
vsize: 285908
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23905
Raw data (stat): 23848 (minisat+) R 23847 28546 28545 0 -1 0 77215 0 0 0 119838 188 0 0 25 0 1 0 541961434 295665664 71500 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72184 71500 603 41 0 72143 0
vsize: 288736
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.83 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 23905
Raw data (stat): 23848 (minisat+) Z 23847 28546 28545 0 -1 12 77216 0 0 0 119839 202 0 0 24 0 1 0 541961434 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.83
CPU time (s): 1200.42
CPU user time (s): 1198.4
CPU system time (s): 2.02369
CPU usage (%): 99.966
Max. virtual memory (Kb): 288736
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####