PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran12x21.opb
MD5SUM	0d744fe957d41a18692933adc6be4af7
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1493203
Optimality of the best value was proved	NO
Number of terms in the objective function	5292
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1511880035
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	1511880035
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.04
Number of variables	5292
Total number of constraints	285
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	285
Minimum length of a constraint	21
Maximum length of a constraint	420
Trace number 17655

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        438296 kB
Buffers:         31884 kB
Cached:         541424 kB
SwapCached:          0 kB
Active:          42912 kB
Inactive:       533188 kB
HighTotal:      131008 kB
HighFree:        10472 kB
LowTotal:       903652 kB
LowFree:        427824 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            14748 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:28:25 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 19277 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 318 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 316]---> Adder-cost: 428   maxlim: 44523   bits: 16/16
c ---[ 314]---> Adder-cost: 428   maxlim: 45163   bits: 16/16
c ---[ 312]---> Adder-cost: 434   maxlim: 55787   bits: 16/16
c ---[ 310]---> Adder-cost: 428   maxlim: 44395   bits: 16/16
c ---[ 308]---> Adder-cost: 428   maxlim: 43627   bits: 16/16
c ---[ 306]---> Adder-cost: 428   maxlim: 43755   bits: 16/16
c ---[ 304]---> Adder-cost: 428   maxlim: 44267   bits: 16/16
c ---[ 302]---> Adder-cost: 412   maxlim: 29419   bits: 15/15
c ---[ 300]---> Adder-cost: 428   maxlim: 44651   bits: 16/16
c ---[ 298]---> Adder-cost: 428   maxlim: 45035   bits: 16/16
c ---[ 296]---> Adder-cost: 434   maxlim: 51819   bits: 16/16
c ---[ 294]---> Adder-cost: 412   maxlim: 29547   bits: 15/15
c ---[ 292]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 290]---> Adder-cost: 242   maxlim: 23540   bits: 15/15
c ---[ 288]---> Adder-cost: 198   maxlim: 5748   bits: 13/13
c ---[ 286]---> Adder-cost: 262   maxlim: 42356   bits: 16/16
c ---[ 284]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 282]---> Adder-cost: 262   maxlim: 41332   bits: 16/16
c ---[ 280]---> Adder-cost: 220   maxlim: 11636   bits: 14/14
c ---[ 278]---> Adder-cost: 266   maxlim: 46836   bits: 16/16
c ---[ 276]---> Adder-cost: 242   maxlim: 23412   bits: 15/15
c ---[ 274]---> Adder-cost: 220   maxlim: 11380   bits: 14/14
c ---[ 272]---> Adder-cost: 262   maxlim: 41588   bits: 16/16
c ---[ 270]---> Adder-cost: 220   maxlim: 11380   bits: 14/14
c ---[ 268]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 266]---> Adder-cost: 262   maxlim: 41588   bits: 16/16
c ---[ 264]---> Adder-cost: 198   maxlim: 5748   bits: 13/13
c ---[ 262]---> Adder-cost: 262   maxlim: 42612   bits: 16/16
c ---[ 260]---> Adder-cost: 220   maxlim: 11636   bits: 14/14
c ---[ 258]---> Adder-cost: 242   maxlim: 22644   bits: 15/15
c ---[ 256]---> Adder-cost: 266   maxlim: 48372   bits: 16/16
c ---[ 254]---> Adder-cost: 266   maxlim: 49140   bits: 16/16
c ---[ 252]---> Adder-cost: 242   maxlim: 23412   bits: 15/15
c ---[ 251]---> BDD-cost:   10
c ---[ 250]---> BDD-cost:   12
c ---[ 249]---> BDD-cost:   11
c ---[ 248]---> BDD-cost:   15
c ---[ 247]---> BDD-cost:   13
c ---[ 246]---> BDD-cost:   16
c ---[ 245]---> BDD-cost:   13
c ---[ 244]---> BDD-cost:   16
c ---[ 243]---> BDD-cost:   10
c ---[ 242]---> BDD-cost:   12
c ---[ 241]---> BDD-cost:   10
c ---[ 240]---> BDD-cost:   11
c ---[ 239]---> BDD-cost:   14
c ---[ 238]---> BDD-cost:   17
c ---[ 237]---> BDD-cost:   13
c ---[ 236]---> BDD-cost:   14
c ---[ 235]---> BDD-cost:   14
c ---[ 234]---> BDD-cost:   14
c ---[ 233]---> BDD-cost:   15
c ---[ 232]---> BDD-cost:   11
c ---[ 231]---> BDD-cost:   14
c ---[ 230]---> BDD-cost:   10
c ---[ 229]---> BDD-cost:   14
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   10
c ---[ 226]---> BDD-cost:   14
c ---[ 225]---> BDD-cost:   15
c ---[ 224]---> BDD-cost:   13
c ---[ 223]---> BDD-cost:   14
c ---[ 222]---> BDD-cost:   13
c ---[ 221]---> BDD-cost:   14
c ---[ 220]---> BDD-cost:   10
c ---[ 219]---> BDD-cost:   12
c ---[ 218]---> BDD-cost:   10
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   14
c ---[ 215]---> BDD-cost:   17
c ---[ 214]---> BDD-cost:   13
c ---[ 213]---> BDD-cost:   15
c ---[ 212]---> BDD-cost:   17
c ---[ 211]---> BDD-cost:   17
c ---[ 210]---> BDD-cost:   15
c ---[ 209]---> BDD-cost:   11
c ---[ 208]---> BDD-cost:   17
c ---[ 207]---> BDD-cost:   10
c ---[ 206]---> BDD-cost:   17
c ---[ 205]---> BDD-cost:   13
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   17
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   13
c ---[ 200]---> BDD-cost:   17
c ---[ 199]---> BDD-cost:   13
c ---[ 198]---> BDD-cost:   17
c ---[ 197]---> BDD-cost:   10
c ---[ 196]---> BDD-cost:   12
c ---[ 195]---> BDD-cost:   10
c ---[ 194]---> BDD-cost:   14
c ---[ 193]---> BDD-cost:   11
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   13
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   15
c ---[ 187]---> BDD-cost:   15
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   15
c ---[ 184]---> BDD-cost:   10
c ---[ 183]---> BDD-cost:   15
c ---[ 182]---> BDD-cost:   15
c ---[ 181]---> BDD-cost:   13
c ---[ 180]---> BDD-cost:   15
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   13
c ---[ 177]---> BDD-cost:   15
c ---[ 176]---> BDD-cost:   13
c ---[ 175]---> BDD-cost:   15
c ---[ 174]---> BDD-cost:   10
c ---[ 173]---> BDD-cost:   12
c ---[ 172]---> BDD-cost:   13
c ---[ 171]---> BDD-cost:   10
c ---[ 170]---> BDD-cost:   11
c ---[ 169]---> BDD-cost:   17
c ---[ 168]---> BDD-cost:   13
c ---[ 167]---> BDD-cost:   15
c ---[ 166]---> BDD-cost:   18
c ---[ 165]---> BDD-cost:   14
c ---[ 164]---> BDD-cost:   15
c ---[ 163]---> BDD-cost:   11
c ---[ 162]---> BDD-cost:   17
c ---[ 161]---> BDD-cost:   14
c ---[ 160]---> BDD-cost:   10
c ---[ 159]---> BDD-cost:   17
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   18
c ---[ 156]---> BDD-cost:   15
c ---[ 155]---> BDD-cost:   13
c ---[ 154]---> BDD-cost:   17
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   17
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:   13
c ---[ 149]---> BDD-cost:   12
c ---[ 148]---> BDD-cost:   10
c ---[ 147]---> BDD-cost:   11
c ---[ 146]---> BDD-cost:   15
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   15
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   15
c ---[ 141]---> BDD-cost:   15
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:   10
c ---[ 138]---> BDD-cost:   14
c ---[ 137]---> BDD-cost:   15
c ---[ 136]---> BDD-cost:   10
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   15
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   15
c ---[ 127]---> BDD-cost:   10
c ---[ 126]---> BDD-cost:   10
c ---[ 125]---> BDD-cost:   12
c ---[ 124]---> BDD-cost:   10
c ---[ 123]---> BDD-cost:   11
c ---[ 122]---> BDD-cost:   17
c ---[ 121]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   14
c ---[ 118]---> BDD-cost:   14
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   12
c ---[ 115]---> BDD-cost:   11
c ---[ 114]---> BDD-cost:   17
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:   17
c ---[ 111]---> BDD-cost:   13
c ---[ 110]---> BDD-cost:   14
c ---[ 109]---> BDD-cost:   15
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   17
c ---[ 106]---> BDD-cost:   13
c ---[ 105]---> BDD-cost:   10
c ---[ 104]---> BDD-cost:   17
c ---[ 103]---> BDD-cost:   10
c ---[ 102]---> BDD-cost:   12
c ---[ 101]---> BDD-cost:   10
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   17
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   17
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   15
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   17
c ---[  90]---> BDD-cost:   10
c ---[  89]---> BDD-cost:   17
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   17
c ---[  86]---> BDD-cost:   15
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   17
c ---[  80]---> BDD-cost:   13
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   17
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   11
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   13
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   13
c ---[  63]---> BDD-cost:   17
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   12
c ---[  60]---> BDD-cost:   10
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   17
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   15
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   17
c ---[  52]---> BDD-cost:   15
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   10
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   13
c ---[  43]---> BDD-cost:   15
c ---[  42]---> BDD-cost:   17
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   17
c ---[  39]---> BDD-cost:   10
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   14
c ---[  31]---> BDD-cost:   16
c ---[  30]---> BDD-cost:   16
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   17
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   16
c ---[  22]---> BDD-cost:   15
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   17
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   16
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   74146   261190 |   22243       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13001          
c   -- var.elim.:  2000/13001          
c   -- var.elim.:  3000/13001          
c   -- var.elim.:  4000/13001          
c   -- var.elim.:  5000/13001          
c   -- var.elim.:  6000/13001          
c   -- var.elim.:  7000/13001          
c   -- var.elim.:  8000/13001          
c   -- var.elim.:  9000/13001          
c   -- var.elim.:  10000/13001          
c   -- var.elim.:  11000/13001          
c   -- var.elim.:  12000/13001          
c   -- var.elim.:  13000/13001          
c   -- var.elim.:  13001/13001          
c   -- var.elim.:  1000/2396          
c   -- var.elim.:  2000/2396          
c   -- var.elim.:  2396/2396          
c   -- subsuming                       
c   -- var.elim.:  1000/1087          
c   -- var.elim.:  1087/1087          
c   -- var.elim.:  1000/1155          
c   -- var.elim.:  1155/1155          
c   -- subsuming                       
c |         0 |   66352   228266 |      --       0       --      -- |     --   | -5385/-18906
c |         0 |   66352   228266 |   26540       0        0     nan |  0.000 % |
c |       100 |   66352   228266 |   29194     100      309     3.1 | 25.722 % |
c |       250 |   66352   228266 |   32114     250      792     3.2 | 25.722 % |
c |       475 |   66352   228266 |   35325     475     1501     3.2 | 25.722 % |
c |       812 |   66341   228229 |   38851     811     2553     3.1 | 25.728 % |
c |      1318 |   66341   228229 |   42737    1317     4206     3.2 | 25.728 % |
c |      2077 |   66246   227904 |   46943    2075     7707     3.7 | 25.809 % |
c |      3216 |   66118   227468 |   51538    3209    12027     3.7 | 25.909 % |
c |      4924 |   66108   227433 |   56683    4916    20170     4.1 | 25.915 % |
c |      7486 |   66086   227359 |   62330    7476    37128     5.0 | 25.927 % |
c |     11330 |   66076   227324 |   68553   11319    75623     6.7 | 25.934 % |
c |     17097 |   66076   227324 |   75409   17086   124343     7.3 | 25.934 % |
c |     25746 |   66056   227254 |   82924   25733   210889     8.2 | 25.946 % |
c |     38720 |   66045   227217 |   91202   38706   354408     9.2 | 25.952 % |
c |     58181 |   66035   227182 |  100307   58166  1086561    18.7 | 25.958 % |
c |     87375 |   66014   227110 |  110302   87356  2396882    27.4 | 25.971 % |
c ==============================================================================
c (current CPU-time: 131.137 s)
c ==============================================================================
c [1mFound solution: 5180786[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10758   maxlim: 3181553   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    118771 |  141152   495526 |   42345  118742  2841218    23.9 | 25.971 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13870          
c   -- var.elim.:  2000/13870          
c   -- var.elim.:  3000/13870          
c   -- var.elim.:  4000/13870          
c   -- var.elim.:  5000/13870          
c   -- var.elim.:  6000/13870          
c   -- var.elim.:  7000/13870          
c   -- var.elim.:  8000/13870          
c   -- var.elim.:  9000/13870          
c   -- var.elim.:  10000/13870          
c   -- var.elim.:  11000/13870          
c   -- var.elim.:  12000/13870          
c   -- var.elim.:  13000/13870          
c   -- var.elim.:  13870/13870          
c   -- var.elim.:  85/85          
c   -- subsuming                       
c |    118771 |  141079   495112 |      --  118742       --      -- |     --   | -73/-403
c |    118771 |  141079   495112 |   56431  118147  2814181    23.8 | 25.971 % |
c |    118871 |  141079   495112 |   62074   26642   248115     9.3 | 15.635 % |
c |    119021 |  141079   495112 |   68282   26792   248792     9.3 | 15.635 % |
c |    119246 |  141079   495112 |   75110   27017   250111     9.3 | 15.635 % |
c |    119583 |  141079   495112 |   82621   27354   251933     9.2 | 15.635 % |
c |    120089 |  141079   495112 |   90883   27860   254698     9.1 | 15.635 % |
c |    120848 |  141079   495112 |   99972   28619   262247     9.2 | 15.635 % |
c |    121987 |  141079   495112 |  109969   29758   271951     9.1 | 15.635 % |
c |    123695 |  141079   495112 |  120966   31466   285652     9.1 | 15.635 % |
c |    126258 |  141079   495112 |  133062   34029   310253     9.1 | 15.635 % |
c |    130103 |  141068   495075 |  146357   37872   346060     9.1 | 15.639 % |
c |    135869 |  141057   495038 |  160980   43637   416064     9.5 | 15.643 % |
c |    144518 |  141047   495003 |  177066   52284   537927    10.3 | 15.647 % |
c |    157493 |  141016   494896 |  194730   65258   728390    11.2 | 15.661 % |
c |    176954 |  141005   494859 |  214186   84718  1224431    14.5 | 15.665 % |
c |    206146 |  140968   494730 |  235543  113909  2398540    21.1 | 15.680 % |
c |    249938 |  140958   494695 |  259079  157700  3713900    23.6 | 15.684 % |
c ==============================================================================
c (current CPU-time: 361.144 s)
c ==============================================================================
c [1mFound solution: 5077526[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3284813   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    276688 |  141034   495102 |   42310  184450  5142907    27.9 | 15.684 % |
c   -- subsuming                       
c   -- var.elim.:  120/120          
c   -- var.elim.:  41/41          
c |    276688 |  141009   495003 |      --  184450       --      -- |     --   | -25/-89
c |    276688 |  141009   495003 |   56403  184438  5142847    27.9 | 15.684 % |
c |    276788 |  141009   495003 |   62043   19700  1127010    57.2 | 15.714 % |
c |    276938 |  141009   495003 |   68248   19850  1127593    56.8 | 15.714 % |
c |    277163 |  141009   495003 |   75073   20075  1128533    56.2 | 15.714 % |
c |    277501 |  141009   495003 |   82580   20413  1130571    55.4 | 15.714 % |
c |    278007 |  141009   495003 |   90838   20919  1134100    54.2 | 15.714 % |
c |    278766 |  141009   495003 |   99922   21678  1139224    52.6 | 15.714 % |
c |    279905 |  141009   495003 |  109914   22817  1147614    50.3 | 15.714 % |
c |    281613 |  141009   495003 |  120906   24525  1156539    47.2 | 15.714 % |
c |    284175 |  140998   494966 |  132986   27086  1174665    43.4 | 15.717 % |
c |    288019 |  140998   494966 |  146284   30930  1201653    38.9 | 15.717 % |
c |    293785 |  140998   494966 |  160913   36696  1256943    34.3 | 15.717 % |
c |    302434 |  140998   494966 |  177004   45345  1338990    29.5 | 15.717 % |
c |    315408 |  140998   494966 |  194705   58319  1488417    25.5 | 15.717 % |
c |    334870 |  140977   494894 |  214143   77778  1710320    22.0 | 15.725 % |
c ==============================================================================
c (current CPU-time: 521.486 s)
c ==============================================================================
c [1mFound solution: 4944783[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3417556   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    354265 |  141029   495198 |   42308   97173  2011711    20.7 | 15.725 % |
c   -- subsuming                       
c   -- var.elim.:  78/78          
c   -- var.elim.:  32/32          
c |    354265 |  140986   494919 |      --   97173       --      -- |     --   | -21/-5
c |    354265 |  140986   494919 |   56394   97171  2011705    20.7 | 15.725 % |
c |    354365 |  140986   494919 |   62033   26831   259507     9.7 | 15.752 % |
c |    354515 |  140986   494919 |   68237   26981   260120     9.6 | 15.752 % |
c |    354740 |  140976   494884 |   75055   27205   261201     9.6 | 15.756 % |
c |    355078 |  140965   494847 |   82554   27542   263164     9.6 | 15.760 % |
c |    355586 |  140965   494847 |   90810   28050   265777     9.5 | 15.760 % |
c |    356346 |  140965   494847 |   99891   28810   270476     9.4 | 15.760 % |
c |    357485 |  140965   494847 |  109880   29949   278931     9.3 | 15.760 % |
c |    359193 |  140954   494810 |  120858   31656   293458     9.3 | 15.764 % |
c |    361755 |  140954   494810 |  132944   34218   320649     9.4 | 15.764 % |
c |    365599 |  140933   494738 |  146217   38059   383483    10.1 | 15.771 % |
c |    371365 |  140933   494738 |  160839   43825   476830    10.9 | 15.771 % |
c |    380016 |  140923   494703 |  176910   52474   749270    14.3 | 15.775 % |
c |    392990 |  140913   494668 |  194587   65445   952213    14.5 | 15.778 % |
c |    412451 |  140913   494668 |  214046   84906  1241224    14.6 | 15.778 % |
c |    441643 |  140893   494598 |  235418  114095  2641964    23.2 | 15.786 % |
c ==============================================================================
c (current CPU-time: 688.868 s)
c ==============================================================================
c [1mFound solution: 4788096[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3574243   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    463760 |  140934   494833 |   42280  136212  3868455    28.4 | 15.786 % |
c   -- subsuming                       
c   -- var.elim.:  103/103          
c   -- var.elim.:  37/37          
c |    463760 |  140927   494797 |      --  136212       --      -- |     --   | -7/-28
c |    463760 |  140927   494797 |   56370  136181  3867587    28.4 | 15.786 % |
c |    463860 |  140927   494797 |   62007   21530  1089295    50.6 | 15.812 % |
c |    464011 |  140927   494797 |   68208   21681  1090041    50.3 | 15.812 % |
c |    464236 |  140927   494797 |   75029   21906  1091405    49.8 | 15.812 % |
c |    464573 |  140927   494797 |   82532   22243  1093356    49.2 | 15.812 % |
c |    465079 |  140927   494797 |   90785   22749  1095557    48.2 | 15.812 % |
c |    465838 |  140927   494797 |   99864   23508  1099027    46.8 | 15.812 % |
c |    466977 |  140927   494797 |  109850   24647  1104581    44.8 | 15.812 % |
c |    468685 |  140927   494797 |  120835   26355  1115777    42.3 | 15.812 % |
c |    471247 |  140927   494797 |  132919   28917  1153180    39.9 | 15.812 % |
c |    475092 |  140927   494797 |  146211   32762  1184789    36.2 | 15.812 % |
c |    480858 |  140927   494797 |  160832   38528  1243433    32.3 | 15.812 % |
c |    489507 |  140927   494797 |  176915   47177  1360295    28.8 | 15.812 % |
c |    502481 |  140927   494797 |  194607   60151  1588374    26.4 | 15.812 % |
c |    521943 |  140927   494797 |  214068   79613  1883654    23.7 | 15.812 % |
c |    551135 |  140927   494797 |  235474  108805  2475349    22.8 | 15.812 % |
c |    594924 |  140916   494760 |  259002  152593  3577054    23.4 | 15.816 % |
c ==============================================================================
c (current CPU-time: 926.095 s)
c ==============================================================================
c [1mFound solution: 4750975[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3611364   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    604720 |  140947   494976 |   42284  162389  3998198    24.6 | 15.816 % |
c   -- subsuming                       
c   -- var.elim.:  59/59          
c   -- var.elim.:  21/21          
c |    604720 |  140912   494549 |      --  162389       --      -- |     --   | -35/-418
c |    604720 |  140912   494549 |   56364  162389  3998198    24.6 | 15.816 % |
c |    604820 |  140912   494549 |   62001   24269   509039    21.0 | 15.843 % |
c |    604970 |  140912   494549 |   68201   24419   509751    20.9 | 15.843 % |
c |    605195 |  140912   494549 |   75021   24644   510902    20.7 | 15.843 % |
c |    605532 |  140912   494549 |   82523   24981   512627    20.5 | 15.843 % |
c |    606038 |  140912   494549 |   90776   25487   515549    20.2 | 15.843 % |
c |    606797 |  140912   494549 |   99853   26246   519631    19.8 | 15.843 % |
c |    607936 |  140912   494549 |  109839   27385   526262    19.2 | 15.843 % |
c |    609644 |  140912   494549 |  120822   29093   540940    18.6 | 15.843 % |
c |    612206 |  140912   494549 |  132905   31655   634781    20.1 | 15.843 % |
c |    616050 |  140912   494549 |  146195   35499   673014    19.0 | 15.843 % |
c |    621816 |  140912   494549 |  160815   41265   775205    18.8 | 15.843 % |
c |    630465 |  140912   494549 |  176896   49914   971328    19.5 | 15.843 % |
c |    643439 |  140912   494549 |  194586   62888  1149307    18.3 | 15.843 % |
c |    662900 |  140881   494442 |  213998   82347  1464757    17.8 | 15.858 % |
c |    692092 |  140881   494442 |  235397  111539  2066272    18.5 | 15.858 % |
c |    735881 |  140881   494442 |  258937  155328  2903278    18.7 | 15.858 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 X4_bit_1 -X4_bit0 X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 X5_bit_4 X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 X8_bit_1 -X8_bit0 X8_bit1 X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 X9_bit_7 X9_bit_6 X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 X11_bit_7 X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 X12_bit_7 X12_bit_6 X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 X14_bit_3 -X14_bit_2 -X14_bit_1 X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 X15_bit_2 X15_bit_1 X15_bit0 X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 X16_bit_2 X16_bit_1 -X16_bit0 X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 X18_bit_3 -X18_bit_2 X18_bit_1 X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 X19_bit_1 X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 X21_bit_7 -X21_bit_6 -X21_bit_5 X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 X22_bit_4 -X22_bit_3 -X22_bit_2 X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 X23_bit_2 X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 X24_bit_4 X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 X25_bit_5 -X25_bit_4 X25_bit_3 -X25_bit_2 X25_bit_1 -X25_bit0 X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 X27_bit_5 X27_bit_4 X27_bit_3 -X27_bit_2 -X27_bit_1 X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 X28_bit_7 -X28_bit_6 -X28_bit_5 X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 X29_bit0 X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 X30_bit_7 X30_bit_6 X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 X32_bit_5 -X32_bit_4 -X32_bit_3 X32_bit_2 X32_bit_1 -X32_bit0 X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 X33_bit_7 -X33_bit_6 X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 X34_bit_7 -X34_bit_6 -X34_bit_5 X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 X35_bit_7 X35_bit_6 X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 X36_bit_2 X36_bit_1 X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 X38_bit_7 X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 X39_bit_7 X39_bit_6 -X39_bit_5 X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 X42_bit_6 -X42_bit_5 -X42_bit_4 X42_bit_3 -X42_bit_2 X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 X45_bit_6 -X45_bit_5 X45_bit_4 X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 X47_bit_7 -X47_bit_6 X47_bit_5 -X47_bit_4 X47_bit_3 X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 X49_bit_3 X49_bit_2 X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 X50_bit_3 -X50_bit_2 -X50_bit_1 X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 X51_bit_7 X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 X51_bit_1 -X51_bit0 X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 X58_bit_2 -X58_bit_1 -X58_bit0 X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 X59_bit_7 -X59_bit_6 -X59_bit_5 X59_bit_4 X59_bit_3 -X59_bit_2 X59_bit_1 X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 X60_bit_1 X60_bit0 -X60_bit1 -X60_bit2 X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 X61_bit_1 X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 X62_bit_7 -X62_bit_6 X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 -X66_bit_6 -X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 X71_bit_7 X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 X73_bit_7 -X73_bit_6 X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 X76_bit2 X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 X78_bit1 X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 X79_bit_7 X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 X80_bit_3 -X80_bit_2 X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 X84_bit_5 -X84_bit_4 X84_bit_3 X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 X87_bit_7 X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 X88_bit_7 X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 X89_bit_6 -X89_bit_5 X89_bit_4 X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 X90_bit_5 -X90_bit_4 -X90_bit_3 X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 -X92_bit_3 X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 X93_bit_1 X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 X95_bit_7 X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 -X98_bit_6 X98_bit_5 X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 X99_bit_7 X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 X100_bit_7 X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X101_bit_7 X101_bit_6 -X101_bit_5 -X101_bit_4 -X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 X102_bit_6 X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 -X104_bit_6 -X104_bit_5 -X104_bit_4 -X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 X105_bit_7 -X105_bit_6 X105_bit_5 X105_bit_4 X105_bit_3 X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 X106_bit_7 X106_bit_6 -X106_bit_5 X106_bit_4 X106_bit_3 -X106_bit_2 X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 X107_bit_7 -X107_bit_6 -X107_bit_5 -X107_bit_4 -X107_bit_3 -X107_bit_2 -X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 X108_bit_7 -X108_bit_6 -X108_bit_5 -X108_bit_4 -X108_bit_3 -X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 -X110_bit_6 -X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 X111_bit_7 X111_bit_6 -X111_bit_5 -X111_bit_4 X111_bit_3 -X111_bit_2 -X111_bit_1 X111_bit0 X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 X112_bit_7 -X112_bit_6 -X112_bit_5 X112_bit_4 -X112_bit_3 -X112_bit_2 -X112_bit_1 X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 X115_bit_7 -X115_bit_6 -X115_bit_5 -X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 X116_bit_7 -X116_bit_6 -X116_bit_5 -X116_bit_4 -X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 -X117_bit_6 X117_bit_5 -X117_bit_4 -X117_bit_3 -X117_bit_2 -X117_bit_1 -X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 X118_bit_7 X118_bit_6 -X118_bit_5 X118_bit_4 X118_bit_3 -X118_bit_2 X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 -X119_bit_7 -X119_bit_6 X119_bit_5 X119_bit_4 -X119_bit_3 -X119_bit_2 -X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 -X120_bit_7 X120_bit_6 -X120_bit_5 -X120_bit_4 -X120_bit_3 -X120_bit_2 -X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 X121_bit_7 X121_bit_6 -X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 -X122_bit_6 -X122_bit_5 -X122_bit_4 X122_bit_3 X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 -X123_bit_6 X123_bit_5 -X123_bit_4 -X123_bit_3 -X123_bit_2 -X123_bit_1 X123_bit0 X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 -X124_bit_7 -X124_bit_6 -X124_bit_5 -X124_bit_4 X124_bit_3 -X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 -X125_bit_7 -X125_bit_6 -X125_bit_5 -X125_bit_4 -X125_bit_3 -X125_bit_2 -X125_bit_1 -X125_bit0 -X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 -X126_bit_7 X126_bit_6 -X126_bit_5 X126_bit_4 -X126_bit_3 -X126_bit_2 -X126_bit_1 -X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 -X127_bit_7 -X127_bit_6 -X127_bit_5 -X127_bit_4 -X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X128_bit_7 X128_bit_6 -X128_bit_5 -X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 X129_bit_7 -X129_bit_6 -X129_bit_5 X129_bit_4 -X129_bit_3 -X129_bit_2 -X129_bit_1 -X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X130_bit_7 X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 X130_bit_2 -X130_bit_1 -X130_bit0 -X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X131_bit_7 X131_bit_6 -X131_bit_5 -X131_bit_4 -X131_bit_3 -X131_bit_2 -X131_bit_1 -X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 -X132_bit_7 -X132_bit_6 X132_bit_5 X132_bit_4 -X132_bit_3 -X132_bit_2 -X132_bit_1 -X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 -X133_bit_6 X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 X134_bit_7 X134_bit_6 -X134_bit_5 -X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 X135_bit_7 X135_bit_6 X135_bit_5 -X135_bit_4 -X135_bit_3 -X135_bit_2 -X135_bit_1 X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 -X136_bit_7 X136_bit_6 X136_bit_5 -X136_bit_4 -X136_bit_3 -X136_bit_2 -X136_bit_1 X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 X137_bit_7 -X137_bit_6 -X137_bit_5 -X137_bit_4 -X137_bit_3 -X137_bit_2 -X137_bit_1 -X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 X138_bit_7 X138_bit_6 -X138_bit_5 -X138_bit_4 X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 X139_bit_7 -X139_bit_6 -X139_bit_5 -X139_bit_4 X139_bit_3 -X139_bit_2 -X139_bit_1 -X139_bit0 -X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 -X140_bit_7 -X140_bit_6 -X140_bit_5 -X140_bit_4 -X140_bit_3 -X140_bit_2 -X140_bit_1 -X140_bit0 -X140_bit1 -X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 -X141_bit_7 -X141_bit_6 -X141_bit_5 -X141_bit_4 -X141_bit_3 -X141_bit_2 -X141_bit_1 -X141_bit0 -X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 -X142_bit_7 -X142_bit_6 -X142_bit_5 -X142_bit_4 -X142_bit_3 -X142_bit_2 -X142_bit_1 -X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 -X143_bit_7 -X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 X144_bit_7 -X144_bit_6 -X144_bit_5 -X144_bit_4 -X144_bit_3 -X144_bit_2 -X144_bit_1 -X144_bit0 -X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 -X145_bit_7 -X145_bit_6 -X145_bit_5 -X145_bit_4 -X145_bit_3 -X145_bit_2 -X145_bit_1 -X145_bit0 -X145_bit1 -X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 X146_bit_7 -X146_bit_6 -X146_bit_5 -X146_bit_4 -X146_bit_3 -X146_bit_2 -X146_bit_1 -X146_bit0 -X146_bit1 X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 -X147_bit_7 -X147_bit_6 X147_bit_5 -X147_bit_4 -X147_bit_3 X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 -X148_bit_7 -X148_bit_6 -X148_bit_5 X148_bit_4 X148_bit_3 -X148_bit_2 X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 -X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 -X150_bit_7 -X150_bit_6 X150_bit_5 X150_bit_4 -X150_bit_3 -X150_bit_2 -X150_bit_1 -X150_bit0 -X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 -X151_bit_3 -X151_bit_2 X151_bit_1 -X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 -X152_bit_6 -X152_bit_5 -X152_bit_4 -X152_bit_3 -X152_bit_2 -X152_bit_1 -X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 -X153_bit_7 -X153_bit_6 -X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 X154_bit_7 -X154_bit_6 -X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 X154_bit_1 X154_bit0 X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 -X155_bit_7 X155_bit_6 -X155_bit_5 -X155_bit_4 -X155_bit_3 X155_bit_2 -X155_bit_1 -X155_bit0 X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 -X156_bit_6 -X156_bit_5 -X156_bit_4 -X156_bit_3 X156_bit_2 -X156_bit_1 X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 -X157_bit_7 -X157_bit_6 -X157_bit_5 -X157_bit_4 -X157_bit_3 -X157_bit_2 -X157_bit_1 -X157_bit0 -X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 X158_bit_7 X158_bit_6 -X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 -X158_bit_1 -X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 X159_bit_7 X159_bit_6 X159_bit_5 -X159_bit_4 -X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 -X160_bit_7 -X160_bit_6 -X160_bit_5 -X160_bit_4 X160_bit_3 -X160_bit_2 -X160_bit_1 X160_bit0 X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X161_bit_7 -X161_bit_6 -X161_bit_5 -X161_bit_4 -X161_bit_3 -X161_bit_2 -X161_bit_1 -X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 X162_bit_7 -X162_bit_6 -X162_bit_5 -X162_bit_4 -X162_bit_3 -X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 X163_bit_7 -X163_bit_6 -X163_bit_5 X163_bit_4 -X163_bit_3 -X163_bit_2 -X163_bit_1 -X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X165_bit_7 -X165_bit_6 -X165_bit_5 -X165_bit_4 X165_bit_3 -X165_bit_2 -X165_bit_1 -X165_bit0 X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 -X166_bit_7 -X166_bit_6 -X166_bit_5 -X166_bit_4 -X166_bit_3 -X166_bit_2 -X166_bit_1 X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 -X167_bit_7 -X167_bit_6 -X167_bit_5 -X167_bit_4 -X167_bit_3 -X167_bit_2 X167_bit_1 -X167_bit0 -X167_bit1 X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 X168_bit_7 -X168_bit_6 X168_bit_5 -X168_bit_4 -X168_bit_3 -X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -X169_bit_7 -X169_bit_6 -X169_bit_5 -X169_bit_4 -X169_bit_3 -X169_bit_2 -X169_bit_1 -X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 X170_bit_7 -X170_bit_6 -X170_bit_5 -X170_bit_4 -X170_bit_3 -X170_bit_2 -X170_bit_1 -X170_bit0 -X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 -X171_bit_7 -X171_bit_6 -X171_bit_5 -X171_bit_4 -X171_bit_3 -X171_bit_2 -X171_bit_1 -X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 -X172_bit_6 -X172_bit_5 -X172_bit_4 -X172_bit_3 -X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 X173_bit_7 -X173_bit_6 -X173_bit_5 X173_bit_4 X173_bit_3 X173_bit_2 -X173_bit_1 -X173_bit0 -X173_bit1 -X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 -X174_bit_7 -X174_bit_6 X174_bit_5 -X174_bit_4 -X174_bit_3 -X174_bit_2 -X174_bit_1 -X174_bit0 -X174_bit1 -X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 X175_bit_7 -X175_bit_6 X175_bit_5 -X175_bit_4 -X175_bit_3 -X175_bit_2 -X175_bit_1 X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 -X176_bit_7 -X176_bit_6 -X176_bit_5 -X176_bit_4 -X176_bit_3 -X176_bit_2 -X176_bit_1 -X176_bit0 -X176_bit1 -X176_bit2 -X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 X177_bit_7 -X177_bit_6 X177_bit_5 -X177_bit_4 X177_bit_3 -X177_bit_2 -X177_bit_1 X177_bit0 -X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 -X178_bit_7 -X178_bit_6 X178_bit_5 -X178_bit_4 -X178_bit_3 X178_bit_2 -X178_bit_1 -X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 -X179_bit_7 X179_bit_6 -X179_bit_5 X179_bit_4 -X179_bit_3 -X179_bit_2 -X179_bit_1 -X179_bit0 -X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 X180_bit_7 X180_bit_6 X180_bit_5 -X180_bit_4 -X180_bit_3 -X180_bit_2 -X180_bit_1 -X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 X181_bit_7 -X181_bit_6 -X181_bit_5 -X181_bit_4 -X181_bit_3 -X181_bit_2 -X181_bit_1 -X181_bit0 -X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 -X182_bit_7 -X182_bit_6 -X182_bit_5 -X182_bit_4 -X182_bit_3 -X182_bit_2 X182_bit_1 -X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 X183_bit_7 -X183_bit_6 -X183_bit_5 -X183_bit_4 -X183_bit_3 -X183_bit_2 -X183_bit_1 -X183_bit0 X183_bit1 -X183_bit2 -X183_bit3 -X183_bit4 X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 X184_bit_7 X184_bit_6 -X184_bit_5 -X184_bit_4 -X184_bit_3 -X184_bit_2 -X184_bit_1 -X184_bit0 -X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 X185_bit_7 -X185_bit_6 -X185_bit_5 -X185_bit_4 X185_bit_3 X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 -X186_bit_6 -X186_bit_5 X186_bit_4 X186_bit_3 X186_bit_2 X186_bit_1 -X186_bit0 -X186_bit1 X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 -X187_bit_7 -X187_bit_6 -X187_bit_5 -X187_bit_4 -X187_bit_3 -X187_bit_2 -X187_bit_1 -X187_bit0 -X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 -X188_bit_7 -X188_bit_6 -X188_bit_5 -X188_bit_4 -X188_bit_3 -X188_bit_2 -X188_bit_1 -X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 X189_bit_7 -X189_bit_6 -X189_bit_5 -X189_bit_4 -X189_bit_3 -X189_bit_2 -X189_bit_1 -X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 X190_bit_7 -X190_bit_6 -X190_bit_5 -X190_bit_4 -X190_bit_3 X190_bit_2 -X190_bit_1 -X190_bit0 -X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 -X191_bit_7 -X191_bit_6 -X191_bit_5 -X191_bit_4 -X191_bit_3 X191_bit_2 -X191_bit_1 -X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 X192_bit_7 -X192_bit_6 -X192_bit_5 X192_bit_4 X192_bit_3 -X192_bit_2 -X192_bit_1 -X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 -X193_bit_6 X193_bit_5 -X193_bit_4 -X193_bit_3 -X193_bit_2 -X193_bit_1 -X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 -X194_bit_7 -X194_bit_6 X194_bit_5 X194_bit_4 -X194_bit_3 X194_bit_2 -X194_bit_1 -X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 -X195_bit_7 -X195_bit_6 X195_bit_5 -X195_bit_4 -X195_bit_3 X195_bit_2 X195_bit_1 -X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 -X196_bit_7 X196_bit_6 -X196_bit_5 -X196_bit_4 -X196_bit_3 -X196_bit_2 X196_bit_1 -X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 -X197_bit_7 X197_bit_6 -X197_bit_5 -X197_bit_4 -X197_bit_3 X197_bit_2 -X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 X198_bit_7 -X198_bit_6 -X198_bit_5 X198_bit_4 -X198_bit_3 -X198_bit_2 X198_bit_1 -X198_bit0 -X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 -X199_bit_7 -X199_bit_6 X199_bit_5 X199_bit_4 X199_bit_3 X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 X200_bit_7 -X200_bit_6 -X200_bit_5 -X200_bit_4 X200_bit_3 -X200_bit_2 -X200_bit_1 X200_bit0 -X200_bit1 -X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 X201_bit_7 X201_bit_6 X201_bit_5 X201_bit_4 -X201_bit_3 -X201_bit_2 -X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 X202_bit_7 -X202_bit_6 -X202_bit_5 -X202_bit_4 X202_bit_3 -X202_bit_2 X202_bit_1 X202_bit0 -X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 -X203_bit_7 X203_bit_6 X203_bit_5 -X203_bit_4 -X203_bit_3 X203_bit_2 -X203_bit_1 -X203_bit0 -X203_bit1 -X203_bit2 -X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 -X204_bit_6 -X204_bit_5 X204_bit_4 X204_bit_3 -X204_bit_2 X204_bit_1 -X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 X205_bit_7 X205_bit_6 -X205_bit_5 -X205_bit_4 -X205_bit_3 -X205_bit_2 X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 X206_bit_7 -X206_bit_6 X206_bit_5 -X206_bit_4 -X206_bit_3 X206_bit_2 -X206_bit_1 X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 -X207_bit_7 -X207_bit_6 -X207_bit_5 -X207_bit_4 -X207_bit_3 -X207_bit_2 -X207_bit_1 -X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 -X208_bit_7 -X208_bit_6 X208_bit_5 -X208_bit_4 -X208_bit_3 X208_bit_2 -X208_bit_1 -X208_bit0 -X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 X209_bit_7 -X209_bit_6 X209_bit_5 X209_bit_4 -X209_bit_3 X209_bit_2 -X209_bit_1 X209_bit0 X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 -X210_bit_7 -X210_bit_6 -X210_bit_5 -X210_bit_4 -X210_bit_3 -X210_bit_2 -X210_bit_1 -X210_bit0 -X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 -X211_bit_7 -X211_bit_6 -X211_bit_5 -X211_bit_4 -X211_bit_3 X211_bit_2 -X211_bit_1 -X211_bit0 X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 -X212_bit_7 -X212_bit_6 -X212_bit_5 X212_bit_4 -X212_bit_3 X212_bit_2 -X212_bit_1 -X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 -X213_bit_7 -X213_bit_6 -X213_bit_5 -X213_bit_4 X213_bit_3 -X213_bit_2 -X213_bit_1 -X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 -X214_bit_7 -X214_bit_6 -X214_bit_5 -X214_bit_4 -X214_bit_3 -X214_bit_2 X214_bit_1 -X214_bit0 -X214_bit1 -X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 -X215_bit_7 -X215_bit_6 -X215_bit_5 X215_bit_4 -X215_bit_3 X215_bit_2 -X215_bit_1 -X215_bit0 -X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 -X216_bit_7 -X216_bit_6 -X216_bit_5 -X216_bit_4 -X216_bit_3 -X216_bit_2 -X216_bit_1 X216_bit0 -X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 -X217_bit_7 -X217_bit_6 -X217_bit_5 X217_bit_4 -X217_bit_3 -X217_bit_2 -X217_bit_1 -X217_bit0 -X217_bit1 -X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 -X218_bit_7 -X218_bit_6 -X218_bit_5 -X218_bit_4 -X218_bit_3 X218_bit_2 -X218_bit_1 -X218_bit0 X218_bit1 X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 -X219_bit_7 -X219_bit_6 X219_bit_5 -X219_bit_4 X219_bit_3 -X219_bit_2 -X219_bit_1 -X219_bit0 -X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 -X220_bit_7 -X220_bit_6 -X220_bit_5 -X220_bit_4 X220_bit_3 -X220_bit_2 -X220_bit_1 -X220_bit0 -X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 -X221_bit_7 -X221_bit_6 X221_bit_5 -X221_bit_4 -X221_bit_3 -X221_bit_2 -X221_bit_1 -X221_bit0 -X221_bit1 -X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 -X222_bit_7 -X222_bit_6 -X222_bit_5 -X222_bit_4 -X222_bit_3 -X222_bit_2 X222_bit_1 -X222_bit0 -X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 -X223_bit_6 -X223_bit_5 -X223_bit_4 -X223_bit_3 -X223_bit_2 X223_bit_1 -X223_bit0 X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 -X224_bit_7 -X224_bit_6 -X224_bit_5 X224_bit_4 -X224_bit_3 -X224_bit_2 -X224_bit_1 -X224_bit0 -X224_bit1 -X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 -X225_bit_7 -X225_bit_6 -X225_bit_5 X225_bit_4 -X225_bit_3 -X225_bit_2 X225_bit_1 X225_bit0 X225_bit1 -X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 -X226_bit_7 -X226_bit_6 X226_bit_5 -X226_bit_4 X226_bit_3 -X226_bit_2 X226_bit_1 -X226_bit0 -X226_bit1 -X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 -X227_bit_7 -X227_bit_6 X227_bit_5 X227_bit_4 X227_bit_3 -X227_bit_2 -X227_bit_1 X227_bit0 -X227_bit1 -X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 -X228_bit_7 -X228_bit_6 -X228_bit_5 X228_bit_4 -X228_bit_3 -X228_bit_2 -X228_bit_1 -X228_bit0 -X228_bit1 -X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 -X229_bit_7 -X229_bit_6 -X229_bit_5 -X229_bit_4 X229_bit_3 -X229_bit_2 -X229_bit_1 -X229_bit0 -X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 -X230_bit_7 -X230_bit_6 -X230_bit_5 X230_bit_4 X230_bit_3 -X230_bit_2 -X230_bit_1 -X230_bit0 -X230_bit1 X230_bit2 X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 -X231_bit_7 -X231_bit_6 -X231_bit_5 -X231_bit_4 -X231_bit_3 -X231_bit_2 -X231_bit_1 -X231_bit0 -X231_bit1 -X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 X232_bit_7 -X232_bit_6 -X232_bit_5 -X232_bit_4 -X232_bit_3 -X232_bit_2 X232_bit_1 -X232_bit0 X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 X233_bit_7 -X233_bit_6 -X233_bit_5 -X233_bit_4 -X233_bit_3 -X233_bit_2 -X233_bit_1 -X233_bit0 -X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 -X234_bit_7 -X234_bit_6 -X234_bit_5 X234_bit_4 -X234_bit_3 -X234_bit_2 -X234_bit_1 -X234_bit0 -X234_bit1 -X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 -X235_bit_7 -X235_bit_6 -X235_bit_5 -X235_bit_4 -X235_bit_3 -X235_bit_2 -X235_bit_1 -X235_bit0 -X235_bit1 -X235_bit2 -X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 -X236_bit_7 -X236_bit_6 -X236_bit_5 -X236_bit_4 -X236_bit_3 -X236_bit_2 -X236_bit_1 -X236_bit0 -X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 X237_bit_7 -X237_bit_6 X237_bit_5 -X237_bit_4 X237_bit_3 X237_bit_2 X237_bit_1 -X237_bit0 X237_bit1 X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 X238_bit_7 -X238_bit_6 -X238_bit_5 X238_bit_4 -X238_bit_3 -X238_bit_2 X238_bit_1 X238_bit0 -X238_bit1 X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 -X239_bit_6 -X239_bit_5 -X239_bit_4 X239_bit_3 -X239_bit_2 -X239_bit_1 -X239_bit0 -X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 -X240_bit_7 -X240_bit_6 -X240_bit_5 -X240_bit_4 X240_bit_3 -X240_bit_2 -X240_bit_1 -X240_bit0 -X240_bit1 -X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 -X241_bit_7 -X241_bit_6 -X241_bit_5 -X241_bit_4 -X241_bit_3 -X241_bit_2 -X241_bit_1 -X241_bit0 -X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 -X242_bit_7 -X242_bit_6 -X242_bit_5 -X242_bit_4 -X242_bit_3 -X242_bit_2 -X242_bit_1 -X242_bit0 -X242_bit1 -X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 -X243_bit_7 -X243_bit_6 -X243_bit_5 -X243_bit_4 X243_bit_3 X243_bit_2 X243_bit_1 -X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 -X244_bit_7 -X244_bit_6 -X244_bit_5 -X244_bit_4 X244_bit_3 -X244_bit_2 -X244_bit_1 -X244_bit0 -X244_bit1 -X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 -X245_bit_7 -X245_bit_6 -X245_bit_5 -X245_bit_4 -X245_bit_3 X245_bit_2 X245_bit_1 -X245_bit0 -X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 -X246_bit_7 -X246_bit_6 -X246_bit_5 -X246_bit_4 X246_bit_3 -X246_bit_2 -X246_bit_1 -X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 -X247_bit_7 -X247_bit_6 -X247_bit_5 -X247_bit_4 X247_bit_3 -X247_bit_2 -X247_bit_1 -X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 -X248_bit_7 -X248_bit_6 -X248_bit_5 -X248_bit_4 X248_bit_3 X248_bit_2 -X248_bit_1 -X248_bit0 -X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 -X249_bit_7 -X249_bit_6 -X249_bit_5 X249_bit_4 -X249_bit_3 -X249_bit_2 -X249_bit_1 X249_bit0 -X249_bit1 X249_bit2 -X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 -X250_bit_7 -X250_bit_6 -X250_bit_5 -X250_bit_4 X250_bit_3 X250_bit_2 -X250_bit_1 X250_bit0 -X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 -X251_bit_7 -X251_bit_6 -X251_bit_5 -X251_bit_4 X251_bit_3 X251_bit_2 X251_bit_1 -X251_bit0 -X251_bit1 -X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 -Y0_bit0 Y1_bit0 Y2_bit0 Y3_bit0 Y4_bit0 Y5_bit0 Y6_bit0 Y7_bit0 Y8_bit0 Y9_bit0 Y10_bit0 Y11_bit0 Y12_bit0 -Y13_bit0 Y14_bit0 Y15_bit0 Y16_bit0 Y17_bit0 Y18_bit0 Y19_bit0 Y20_bit0 Y21_bit0 Y22_bit0 Y23_bit0 Y24_bit0 Y25_bit0 Y26_bit0 Y27_bit0 Y28_bit0 Y29_bit0 Y30_bit0 Y31_bit0 Y32_bit0 Y33_bit0 Y34_bit0 Y35_bit0 Y36_bit0 Y37_bit0 Y38_bit0 Y39_bit0 Y40_bit0 Y41_bit0 Y42_bit0 Y43_bit0 Y44_bit0 Y45_bit0 Y46_bit0 Y47_bit0 Y48_bit0 Y49_bit0 Y50_bit0 Y51_bit0 Y52_bit0 Y53_bit0 Y54_bit0 Y55_bit0 -Y56_bit0 Y57_bit0 Y58_bit0 Y59_bit0 Y60_bit0 Y61_bit0 Y62_bit0 -Y63_bit0 Y64_bit0 Y65_bit0 -Y66_bit0 -Y67_bit0 Y68_bit0 Y69_bit0 -Y70_bit0 Y71_bit0 Y72_bit0 Y73_bit0 Y74_bit0 Y75_bit0 Y76_bit0 Y77_bit0 Y78_bit0 Y79_bit0 Y80_bit0 Y81_bit0 Y82_bit0 Y83_bit0 Y84_bit0 Y85_bit0 Y86_bit0 Y87_bit0 Y88_bit0 Y89_bit0 Y90_bit0 Y91_bit0 Y92_bit0 Y93_bit0 -Y94_bit0 Y95_bit0 Y96_bit0 Y97_bit0 Y98_bit0 Y99_bit0 Y100_bit0 Y101_bit0 Y102_bit0 Y103_bit0 -Y104_bit0 Y105_bit0 Y106_bit0 Y107_bit0 Y108_bit0 Y109_bit0 -Y110_bit0 Y111_bit0 Y112_bit0 Y113_bit0 Y114_bit0 Y115_bit0 Y116_bit0 Y117_bit0 Y118_bit0 Y119_bit0 Y120_bit0 Y121_bit0 Y122_bit0 Y123_bit0 Y124_bit0 Y125_bit0 Y126_bit0 -Y127_bit0 Y128_bit0 Y129_bit0 Y130_bit0 Y131_bit0 Y132_bit0 Y133_bit0 Y134_bit0 Y135_bit0 Y136_bit0 Y137_bit0 Y138_bit0 Y139_bit0 -Y140_bit0 -Y141_bit0 Y142_bit0 -Y143_bit0 Y144_bit0 -Y145_bit0 Y146_bit0 Y147_bit0 Y148_bit0 Y149_bit0 Y150_bit0 Y151_bit0 -Y152_bit0 -Y153_bit0 Y154_bit0 Y155_bit0 Y156_bit0 Y157_bit0 Y158_bit0 Y159_bit0 Y160_bit0 -Y161_bit0 Y162_bit0 Y163_bit0 Y164_bit0 Y165_bit0 Y166_bit0 Y167_bit0 Y168_bit0 -Y169_bit0 Y1#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.79 0.95 0.91 2/54 7414
Raw data (stat): 7414 (runsolver) R 7413 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486379314 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.83 0.95 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 3469 0 0 0 989 9 0 0 25 0 1 0 486379314 16097280 3041 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3930 3041 603 41 0 3889 0
vsize: 15720
[startup+19.9998 s]
Raw data (loadavg): 0.85 0.95 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 3638 0 0 0 1989 9 0 0 25 0 1 0 486379314 16904192 3210 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4127 3210 603 41 0 4086 0
vsize: 16508
[startup+30.001 s]
Raw data (loadavg): 0.87 0.95 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 3818 0 0 0 2988 10 0 0 25 0 1 0 486379314 17645568 3390 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4308 3390 603 41 0 4267 0
vsize: 17232
[startup+40.0018 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 4013 0 0 0 3987 11 0 0 25 0 1 0 486379314 18456576 3585 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4506 3585 603 41 0 4465 0
vsize: 18024
[startup+50.0031 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 4271 0 0 0 4987 12 0 0 25 0 1 0 486379314 19529728 3843 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4768 3843 603 41 0 4727 0
vsize: 19072
[startup+60.0033 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 4937 0 0 0 5985 14 0 0 25 0 1 0 486379314 22204416 4509 4294967295 134512640 134672761 3221224544 3221223584 134603548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5421 4509 603 41 0 5380 0
vsize: 21684
[startup+70.0041 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 5456 0 0 0 6984 16 0 0 25 0 1 0 486379314 24338432 5028 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5942 5028 603 41 0 5901 0
vsize: 23768
[startup+80.0044 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 5777 0 0 0 7983 17 0 0 25 0 1 0 486379314 25808896 5349 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6301 5349 603 41 0 6260 0
vsize: 25204
[startup+90.0046 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 7094 0 0 0 8980 19 0 0 25 0 1 0 486379314 31129600 6666 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7600 6666 603 41 0 7559 0
vsize: 30400
[startup+100.005 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 7322 0 0 0 9979 20 0 0 25 0 1 0 486379314 32071680 6894 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7830 6894 603 41 0 7789 0
vsize: 31320
[startup+110.006 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 7495 0 0 0 10979 21 0 0 25 0 1 0 486379314 32784384 7067 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8004 7067 603 41 0 7963 0
vsize: 32016
[startup+120.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 7689 0 0 0 11978 22 0 0 25 0 1 0 486379314 33579008 7261 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8198 7261 603 41 0 8157 0
vsize: 32792
[startup+130.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 7920 0 0 0 12977 23 0 0 25 0 1 0 486379314 34512896 7492 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8426 7492 603 41 0 8385 0
vsize: 33704
[startup+140.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 13958 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 14959 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+160.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 15959 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+170.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 16959 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 17958 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 18959 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 19959 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 20959 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223728 134615529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 21959 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223584 134612606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 22960 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 23960 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 24960 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16487 0 0 0 25960 42 0 0 25 0 1 0 486379314 61595648 13685 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 13685 603 41 0 14997 0
vsize: 60152
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16513 0 0 0 26960 42 0 0 25 0 1 0 486379314 61726720 13711 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15070 13711 603 41 0 15029 0
vsize: 60280
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16652 0 0 0 27960 42 0 0 25 0 1 0 486379314 62263296 13850 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15201 13850 603 41 0 15160 0
vsize: 60804
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 16944 0 0 0 28960 43 0 0 25 0 1 0 486379314 63471616 14142 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15496 14142 603 41 0 15455 0
vsize: 61984
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 17133 0 0 0 29959 43 0 0 25 0 1 0 486379314 64802816 14331 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15821 14331 603 41 0 15780 0
vsize: 63284
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 17333 0 0 0 30959 44 0 0 25 0 1 0 486379314 65609728 14531 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16018 14531 603 41 0 15977 0
vsize: 64072
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 17646 0 0 0 31958 45 0 0 25 0 1 0 486379314 66801664 14844 4294967295 134512640 134672761 3221224544 3221223500 1075351130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16309 14844 603 41 0 16268 0
vsize: 65236
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 18285 0 0 0 32957 47 0 0 25 0 1 0 486379314 69332992 15483 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16927 15483 603 41 0 16886 0
vsize: 67708
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 18565 0 0 0 33956 47 0 0 25 0 1 0 486379314 70541312 15763 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17222 15763 603 41 0 17181 0
vsize: 68888
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 18864 0 0 0 34955 48 0 0 25 0 1 0 486379314 71745536 16062 4294967295 134512640 134672761 3221224544 3221223724 134615849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17516 16062 603 41 0 17475 0
vsize: 70064
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 19919 0 0 0 35952 52 0 0 25 0 1 0 486379314 75976704 17117 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18549 17117 603 41 0 18508 0
vsize: 74196
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 36949 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 37949 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 38949 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 39950 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223712 134615864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 40950 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 41950 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 42950 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 43951 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223708 134564596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 44951 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 45951 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 46951 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 47951 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 48951 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 49952 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 50952 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 21509 0 0 0 51952 55 0 0 25 0 1 0 486379314 77479936 17473 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17473 603 41 0 18875 0
vsize: 75664
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 52950 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 53949 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223680 134614710 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 54949 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 55949 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 56950 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 57950 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 58950 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 59950 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 60951 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 61951 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223744 134610709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 62951 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 63951 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 64951 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223728 134615560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 65951 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 66952 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22300 0 0 0 67952 57 0 0 25 0 1 0 486379314 78499840 17688 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19165 17688 603 41 0 19124 0
vsize: 76660
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 22746 0 0 0 68951 59 0 0 25 0 1 0 486379314 77602816 17507 4294967295 134512640 134672761 3221224544 3221221856 134543999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18946 17507 603 41 0 18905 0
vsize: 75784
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 69950 59 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 70950 59 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 71950 59 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 72950 59 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 73950 59 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 74951 59 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 75951 59 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 76951 59 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 77951 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 78950 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 79950 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 80950 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 81951 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+830.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 82951 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 83951 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 84951 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 85951 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 86952 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 87952 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 88952 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 89952 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 90952 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+920.027 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23156 0 0 0 91952 60 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+930.027 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 92950 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+940.027 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 93950 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223712 134564714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+950.027 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 94950 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223668 134566106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+960.027 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 95949 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+970.027 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 96949 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+980.027 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 97949 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+990.027 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 98949 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1000.03 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 99950 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1010.03 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 100950 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1020.03 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 101950 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1030.03 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 102950 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1040.03 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 103950 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1050.03 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 104950 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 105950 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 106951 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 107951 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 108951 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 109951 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 110952 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 111952 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223732 134610770 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 112952 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 113952 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 114952 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 115953 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223696 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 116953 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 117953 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 118953 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 7414
Raw data (stat): 7414 (minisat+) R 7413 30854 30853 0 -1 0 23910 0 0 0 119953 63 0 0 25 0 1 0 486379314 77602816 17508 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18946 17508 603 41 0 18905 0
vsize: 75784
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 7414
Raw data (stat): 7414 (minisat+) Z 7413 30854 30853 0 -1 12 23911 0 0 0 119954 67 0 0 25 0 1 0 486379314 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.08
CPU time (s): 1200.22
CPU user time (s): 1199.55
CPU system time (s): 0.670898
CPU usage (%): 100.011
Max. virtual memory (Kb): 76660
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####