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-ran6x43.opb
MD5SUM	795a1eda830447df9b9714fdf1d66b4e
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2795888
Optimality of the best value was proved	NO
Number of terms in the objective function	5418
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	1537450315
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	1537450315
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	1224.65
Number of variables	5418
Total number of constraints	307
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	307
Minimum length of a constraint	21
Maximum length of a constraint	860
Trace number 17617

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 10:53:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19349 boxname=wulflinc13 idbench=1489 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  795a1eda830447df9b9714fdf1d66b4e  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-ran6x43.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-ran6x43.opb
IDLAUNCH: 19349
/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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        431712 kB
Buffers:         34940 kB
Cached:         545604 kB
SwapCached:        176 kB
Active:         235988 kB
Inactive:       347296 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        431460 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            14104 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:13:53 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 19349 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 356 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 354]---> Adder-cost: 894   maxlim: 78677   bits: 17/17
c ---[ 352]---> Adder-cost: 894   maxlim: 84309   bits: 17/17
c ---[ 350]---> Adder-cost: 886   maxlim: 78933   bits: 17/17
c ---[ 348]---> Adder-cost: 894   maxlim: 93141   bits: 17/17
c ---[ 346]---> Adder-cost: 818   maxlim: 37973   bits: 16/16
c ---[ 344]---> Adder-cost: 894   maxlim: 84437   bits: 17/17
c ---[ 342]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 340]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 336]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 334]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 330]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 258]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 257]---> BDD-cost:   12
c ---[ 256]---> BDD-cost:   12
c ---[ 255]---> BDD-cost:   14
c ---[ 254]---> BDD-cost:   11
c ---[ 253]---> BDD-cost:   15
c ---[ 252]---> BDD-cost:   17
c ---[ 251]---> BDD-cost:   14
c ---[ 250]---> BDD-cost:   10
c ---[ 249]---> BDD-cost:   12
c ---[ 248]---> BDD-cost:   17
c ---[ 247]---> BDD-cost:   12
c ---[ 246]---> BDD-cost:   10
c ---[ 245]---> BDD-cost:   15
c ---[ 244]---> BDD-cost:   17
c ---[ 243]---> BDD-cost:   12
c ---[ 242]---> BDD-cost:   13
c ---[ 241]---> BDD-cost:   11
c ---[ 240]---> BDD-cost:   15
c ---[ 239]---> BDD-cost:   17
c ---[ 238]---> BDD-cost:   12
c ---[ 237]---> BDD-cost:   11
c ---[ 236]---> BDD-cost:   12
c ---[ 235]---> BDD-cost:    9
c ---[ 234]---> BDD-cost:   11
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   10
c ---[ 230]---> BDD-cost:   14
c ---[ 229]---> BDD-cost:   17
c ---[ 228]---> BDD-cost:   17
c ---[ 227]---> BDD-cost:    9
c ---[ 226]---> BDD-cost:   15
c ---[ 225]---> BDD-cost:   14
c ---[ 224]---> BDD-cost:   11
c ---[ 223]---> BDD-cost:   12
c ---[ 222]---> BDD-cost:   12
c ---[ 221]---> BDD-cost:   12
c ---[ 220]---> BDD-cost:   13
c ---[ 219]---> BDD-cost:   11
c ---[ 218]---> BDD-cost:   17
c ---[ 217]---> BDD-cost:   14
c ---[ 216]---> BDD-cost:   14
c ---[ 215]---> BDD-cost:   11
c ---[ 214]---> BDD-cost:   11
c ---[ 213]---> BDD-cost:   12
c ---[ 212]---> BDD-cost:   14
c ---[ 211]---> BDD-cost:   11
c ---[ 210]---> BDD-cost:   17
c ---[ 209]---> BDD-cost:   13
c ---[ 208]---> BDD-cost:   12
c ---[ 207]---> BDD-cost:   11
c ---[ 206]---> BDD-cost:   15
c ---[ 205]---> BDD-cost:   19
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:   10
c ---[ 202]---> BDD-cost:   12
c ---[ 201]---> BDD-cost:   15
c ---[ 200]---> BDD-cost:   15
c ---[ 199]---> BDD-cost:   12
c ---[ 198]---> BDD-cost:   10
c ---[ 197]---> BDD-cost:   15
c ---[ 196]---> BDD-cost:   12
c ---[ 195]---> BDD-cost:   13
c ---[ 194]---> BDD-cost:   11
c ---[ 193]---> BDD-cost:   15
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   12
c ---[ 190]---> BDD-cost:   11
c ---[ 189]---> BDD-cost:   19
c ---[ 188]---> BDD-cost:   12
c ---[ 187]---> BDD-cost:    9
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   10
c ---[ 183]---> BDD-cost:   14
c ---[ 182]---> BDD-cost:   17
c ---[ 181]---> BDD-cost:   19
c ---[ 180]---> BDD-cost:    9
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   14
c ---[ 177]---> BDD-cost:   14
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   13
c ---[ 174]---> BDD-cost:   12
c ---[ 173]---> BDD-cost:   13
c ---[ 172]---> BDD-cost:   11
c ---[ 171]---> BDD-cost:   13
c ---[ 170]---> BDD-cost:   13
c ---[ 169]---> BDD-cost:   13
c ---[ 168]---> BDD-cost:   11
c ---[ 167]---> BDD-cost:   10
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   13
c ---[ 164]---> BDD-cost:   13
c ---[ 163]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 161]---> BDD-cost:   12
c ---[ 160]---> BDD-cost:   11
c ---[ 159]---> BDD-cost:   13
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   13
c ---[ 156]---> BDD-cost:   12
c ---[ 155]---> BDD-cost:   10
c ---[ 154]---> BDD-cost:   13
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   12
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:   13
c ---[ 149]---> BDD-cost:   12
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   11
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   19
c ---[ 143]---> BDD-cost:   13
c ---[ 142]---> BDD-cost:   13
c ---[ 141]---> BDD-cost:   11
c ---[ 140]---> BDD-cost:   12
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:   11
c ---[ 137]---> BDD-cost:   13
c ---[ 136]---> BDD-cost:   10
c ---[ 135]---> BDD-cost:   13
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   12
c ---[ 132]---> BDD-cost:   13
c ---[ 131]---> BDD-cost:    9
c ---[ 130]---> BDD-cost:   13
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   12
c ---[ 126]---> BDD-cost:   12
c ---[ 125]---> BDD-cost:   13
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   17
c ---[ 122]---> BDD-cost:   10
c ---[ 121]---> BDD-cost:   14
c ---[ 120]---> BDD-cost:   14
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:   11
c ---[ 117]---> BDD-cost:   12
c ---[ 116]---> BDD-cost:   14
c ---[ 115]---> BDD-cost:   17
c ---[ 114]---> BDD-cost:   13
c ---[ 113]---> BDD-cost:   12
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:   19
c ---[ 108]---> BDD-cost:   14
c ---[ 107]---> BDD-cost:   10
c ---[ 106]---> BDD-cost:   12
c ---[ 105]---> BDD-cost:   19
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   10
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   12
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   12
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   12
c ---[  92]---> BDD-cost:    9
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   13
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   17
c ---[  85]---> BDD-cost:   19
c ---[  84]---> BDD-cost:    9
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   14
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   12
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   12
c ---[  73]---> BDD-cost:    9
c ---[  72]---> BDD-cost:   11
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   14
c ---[  68]---> BDD-cost:   17
c ---[  67]---> BDD-cost:   19
c ---[  66]---> BDD-cost:    9
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   11
c ---[  61]---> BDD-cost:   12
c ---[  60]---> BDD-cost:   12
c ---[  59]---> BDD-cost:   13
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   14
c ---[  49]---> BDD-cost:   17
c ---[  48]---> BDD-cost:   13
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   11
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   19
c ---[  43]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:   10
c ---[  40]---> BDD-cost:   12
c ---[  39]---> BDD-cost:   19
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   12
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:   15
c ---[  30]---> BDD-cost:   17
c ---[  29]---> BDD-cost:   12
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   12
c ---[  26]---> BDD-cost:    9
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   17
c ---[  23]---> BDD-cost:   10
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   17
c ---[  19]---> BDD-cost:   19
c ---[  18]---> BDD-cost:    9
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   12
c ---[  13]---> BDD-cost:   12
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   12
c ---[   9]---> BDD-cost:   17
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   11
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   17
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  130292   351692 |   43430       0        0     nan |  0.000 % |
c |       101 |  129982   350986 |   47773      86      285     3.3 | 10.876 % |
c |       251 |  129745   350445 |   52550     227      782     3.4 | 11.042 % |
c |       476 |  129592   350099 |   57805     440     1526     3.5 | 11.148 % |
c |       813 |  129191   349134 |   63585     754     2652     3.5 | 11.410 % |
c |      1319 |  128975   348574 |   69944    1248     4595     3.7 | 11.548 % |
c |      2078 |  128738   348035 |   76938    1990     7288     3.7 | 11.708 % |
c |      3217 |  128642   347807 |   84632    3122    12665     4.1 | 11.773 % |
c |      4925 |  127437   345051 |   93096    4770    19257     4.0 | 12.643 % |
c |      7487 |  126161   342093 |  102405    7233    34078     4.7 | 13.545 % |
c |     11331 |  125335   340140 |  112646   11015    52922     4.8 | 14.126 % |
c |     17097 |  124262   337580 |  123910   16676   117469     7.0 | 14.869 % |
c |     25746 |  122620   333161 |  136301   25013   205317     8.2 | 15.886 % |
c ==============================================================================
c [1mFound solution: 5546607[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10631   maxlim: 2940636   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27381 |  196862   598439 |   65620   26643   226329     8.5 | 15.886 % |
c |     27481 |  196862   598439 |   72182   26743   226818     8.5 | 12.776 % |
c |     27633 |  196862   598439 |   79400   26895   228559     8.5 | 12.776 % |
c |     27858 |  196831   598367 |   87340   27115   229812     8.5 | 12.795 % |
c |     28198 |  196821   598344 |   96074   27454   234688     8.5 | 12.800 % |
c |     28704 |  196816   598332 |  105681   27959   238050     8.5 | 12.804 % |
c |     29463 |  196789   598269 |  116249   28715   244784     8.5 | 12.827 % |
c |     30602 |  196645   597933 |  127874   29837   257229     8.6 | 12.903 % |
c |     32310 |  196572   597740 |  140662   31537   288602     9.2 | 12.937 % |
c |     34872 |  196497   597566 |  154728   34085   327172     9.6 | 12.982 % |
c |     38716 |  196415   597377 |  170201   37920   408071    10.8 | 13.033 % |
c ==============================================================================
c [1mFound solution: 5464409[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3022834   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40674 |  196375   597463 |   65458   39873   440595    11.0 | 13.033 % |
c |     40774 |  196361   597431 |   72003   39971   440993    11.0 | 13.102 % |
c |     40926 |  196361   597431 |   79204   40123   441640    11.0 | 13.102 % |
c |     41151 |  196361   597431 |   87124   40348   445423    11.0 | 13.102 % |
c |     41489 |  196361   597431 |   95837   40686   449468    11.0 | 13.102 % |
c |     41995 |  196361   597431 |  105420   41192   456314    11.1 | 13.102 % |
c |     42756 |  196361   597431 |  115962   41953   468201    11.2 | 13.102 % |
c |     43896 |  196361   597431 |  127559   43093   507870    11.8 | 13.102 % |
c |     45605 |  196263   597204 |  140315   44787   538528    12.0 | 13.160 % |
c |     48167 |  196263   597204 |  154346   47349   640087    13.5 | 13.160 % |
c |     52011 |  196263   597204 |  169781   51193   740047    14.5 | 13.160 % |
c |     57777 |  196246   597165 |  186759   56958   936123    16.4 | 13.172 % |
c ==============================================================================
c [1mFound solution: 4979303[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3507940   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58953 |  196205   597212 |   65401   58131   963072    16.6 | 13.172 % |
c |     59053 |  196176   597146 |   71941   58228   963450    16.5 | 13.245 % |
c |     59203 |  195987   596712 |   79135   58357   964531    16.5 | 13.350 % |
c |     59428 |  195979   596693 |   87048   58581   965593    16.5 | 13.355 % |
c |     59765 |  195972   596677 |   95753   58917   967368    16.4 | 13.359 % |
c |     60271 |  195962   596654 |  105328   59420   971149    16.3 | 13.367 % |
c |     61030 |  195962   596654 |  115861   60179   985365    16.4 | 13.367 % |
c |     62170 |  195962   596654 |  127448   61319  1015148    16.6 | 13.367 % |
c |     63878 |  195917   596549 |  140192   63022  1099870    17.5 | 13.395 % |
c |     66440 |  195882   596467 |  154212   65582  1154706    17.6 | 13.414 % |
c |     70284 |  195842   596376 |  169633   69423  1305384    18.8 | 13.440 % |
c |     76050 |  195759   596182 |  186596   75177  1516897    20.2 | 13.485 % |
c |     84699 |  195695   596036 |  205256   83817  2272271    27.1 | 13.524 % |
c |     97674 |  195663   595964 |  225781   96787  2891364    29.9 | 13.541 % |
c ==============================================================================
c [1mFound solution: 4309718[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4177525   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    104001 |  195645   596091 |   65215  103108  3242572    31.4 | 13.541 % |
c |    104101 |  195626   596046 |   71736   19413   764607    39.4 | 13.598 % |
c |    104252 |  195591   595967 |   78910   19561   765175    39.1 | 13.617 % |
c |    104477 |  195578   595937 |   86801   19783   766247    38.7 | 13.624 % |
c |    104815 |  195578   595937 |   95481   20121   767833    38.2 | 13.624 % |
c |    105321 |  195537   595843 |  105029   20619   770380    37.4 | 13.652 % |
c |    106080 |  195457   595661 |  115532   21371   773963    36.2 | 13.699 % |
c |    107219 |  195450   595645 |  127085   22509   780010    34.7 | 13.705 % |
c |    108927 |  195320   595346 |  139794   24195   790289    32.7 | 13.787 % |
c |    111489 |  195308   595317 |  153773   26756   861791    32.2 | 13.795 % |
c |    115333 |  195166   594991 |  169150   30585   905345    29.6 | 13.881 % |
c |    121099 |  195133   594915 |  186066   36348  1124727    30.9 | 13.902 % |
c |    129749 |  195033   594688 |  204672   44987  1286747    28.6 | 13.962 % |
c |    142723 |  195005   594623 |  225139   57958  1605740    27.7 | 13.978 % |
c |    162184 |  194983   594565 |  247653   77413  2465958    31.9 | 13.992 % |
c ==============================================================================
c [1mFound solution: 4302747[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4184496   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    182112 |  194984   594668 |   64994   97340  3835165    39.4 | 13.992 % |
c |    182212 |  194984   594668 |   71493   20413  1143629    56.0 | 14.006 % |
c |    182363 |  194972   594641 |   78642   20562  1144274    55.6 | 14.013 % |
c |    182589 |  194952   594594 |   86507   20786  1145506    55.1 | 14.028 % |
c |    182926 |  194930   594542 |   95157   21122  1147624    54.3 | 14.039 % |
c |    183433 |  194930   594542 |  104673   21629  1150269    53.2 | 14.039 % |
c |    184192 |  194914   594505 |  115140   22387  1153834    51.5 | 14.047 % |
c |    185331 |  194891   594453 |  126654   23522  1161557    49.4 | 14.060 % |
c |    187039 |  194879   594425 |  139320   25228  1172314    46.5 | 14.066 % |
c |    189601 |  194778   594193 |  153252   27781  1188064    42.8 | 14.124 % |
c |    193445 |  194716   594051 |  168577   31620  1248764    39.5 | 14.156 % |
c |    199212 |  194697   594006 |  185435   37385  1655594    44.3 | 14.167 % |
c |    207861 |  194678   593956 |  203979   46029  1911038    41.5 | 14.176 % |
c |    220836 |  194678   593956 |  224376   59004  3351981    56.8 | 14.176 % |
c |    240297 |  194377   593259 |  246814   78430  3748761    47.8 | 14.354 % |
c |    269490 |  194350   593196 |  271496  107620  5493226    51.0 | 14.373 % |
c |    313280 |  194330   593150 |  298645  151408 12103280    79.9 | 14.386 % |
c |    378964 |  194318   593122 |  328510  217089 24344104   112.1 | 14.394 % |
c ==============================================================================
c [1mFound solution: 3514344[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4972899   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    460943 |  194338   593278 |   64779  299067 30336227   101.4 | 14.394 % |
c |    461043 |  194319   593234 |   71256   22220  1807280    81.3 | 14.422 % |
c |    461193 |  194293   593175 |   78382   22366  1808032    80.8 | 14.439 % |
c |    461419 |  194276   593133 |   86220   22589  1808886    80.1 | 14.449 % |
c |    461756 |  194276   593133 |   94842   22926  1810216    79.0 | 14.449 % |
c |    462262 |  194267   593112 |  104327   23430  1813261    77.4 | 14.456 % |
c |    463021 |  194241   593051 |  114759   24187  1817885    75.2 | 14.473 % |
c |    464161 |  194183   592916 |  126235   25321  1828387    72.2 | 14.507 % |
c |    465869 |  194146   592830 |  138859   27025  1842916    68.2 | 14.531 % |
c |    468431 |  194113   592755 |  152745   29583  1873186    63.3 | 14.552 % |
c |    472275 |  194085   592691 |  168020   33424  1911935    57.2 | 14.567 % |
c |    478041 |  194064   592642 |  184822   39186  2315555    59.1 | 14.578 % |
c |    486692 |  193964   592411 |  203304   47823  2447108    51.2 | 14.636 % |
c |    499666 |  193885   592227 |  223634   60782  2725103    44.8 | 14.683 % |
c |    519127 |  193875   592204 |  245998   80241  3589969    44.7 | 14.688 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 X0_bit_5 X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 X2_bit_7 X2_bit_6 X2_bit_5 X2_bit_4 X2_bit_3 X2_bit_2 X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 X4_bit_5 -X4_bit_4 -X4_bit_3 X4_bit_2 X4_bit_1 X4_bit0 -X4_bit1 X4_bit2 -X4_bit3 X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 X5_bit_6 X5_bit_5 X5_bit_4 X5_bit_3 X5_bit_2 X5_bit_1 -X5_bit0 X5_bit1 X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 X6_bit_5 X6_bit_4 -X6_bit_3 X6_bit_2 X6_bit_1 X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 X10_bit_7 -X10_bit_6 X10_bit_5 -X10_bit_4 X10_bit_3 X10_bit_2 X10_bit_1 X10_bit0 -X10_bit1 X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 X11_bit_7 -X11_bit_6 -X11_bit_5 X11_bit_4 -X11_bit_3 X11_bit_2 X11_bit_1 X11_bit0 -X11_bit1 X11_bit2 X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 X12_bit_7 -X12_bit_6 X12_bit_5 X12_bit_4 X12_bit_3 -X12_bit_2 -X12_bit_1 X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 X15_bit_7 -X15_bit_6 X15_bit_5 -X15_bit_4 X15_bit_3 X15_bit_2 X15_bit_1 -X15_bit0 X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 X20_bit_7 -X20_bit_6 -X20_bit_5 X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 X20_bit0 X20_bit1 X20_bit2 X20_bit3 X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 X21_bit_3 X21_bit_2 -X21_bit_1 X21_bit0 -X21_bit1 X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 X22_bit_7 X22_bit_6 X22_bit_5 X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 X26_bit_7 X26_bit_6 X26_bit_5 X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 X28_bit0 X28_bit1 -X28_bit2 X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 X29_bit_7 X29_bit_6 X29_bit_5 X29_bit_4 X29_bit_3 X29_bit_2 X29_bit_1 X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 X30_bit_7 X30_bit_6 -X30_bit_5 X30_bit_4 X30_bit_3 X30_bit_2 X30_bit_1 -X30_bit0 X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 X33_bit_7 -X33_bit_6 X33_bit_5 -X33_bit_4 X33_bit_3 X33_bit_2 X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 X34_bit_7 X34_bit_6 X34_bit_5 X34_bit_4 X34_bit_3 X34_bit_2 X34_bit_1 X34_bit0 -X34_bit1 X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 X37_bit_7 X37_bit_6 X37_bit_5 -X37_bit_4 X37_bit_3 X37_bit_2 X37_bit_1 -X37_bit0 -X37_bit1 X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 X38_bit_4 X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 X38_bit1 X38_bit2 -X38_bit3 X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 X39_bit_7 X39_bit_6 X39_bit_5 -X39_bit_4 -X39_bit_3 X39_bit_2 X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 X41_bit_5 X41_bit_4 X41_bit_3 X41_bit_2 X41_bit_1 X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 X43_bit_5 X43_bit_4 X43_bit_3 -X43_bit_2 -X43_bit_1 X43_bit0 -X43_bit1 X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 X44_bit_6 X44_bit_5 X44_bit_4 X44_bit_3 X44_bit_2 X44_bit_1 X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 X45_bit_6 X45_bit_5 X45_bit_4 X45_bit_3 X45_bit_2 X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 X47_bit_6 -X47_bit_5 X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 X47_bit0 X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 X48_bit_7 X48_bit_6 X48_bit_5 X48_bit_4 X48_bit_3 -X48_bit_2 X48_bit_1 -X48_bit0 X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 X49_bit_7 X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 X49_bit_2 X49_bit_1 X49_bit0 X49_bit1 X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 X53_bit_5 X53_bit_4 X53_bit_3 X53_bit_2 X53_bit_1 -X53_bit0 X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 X57_bit0 X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 X58_bit_7 X58_bit_6 X58_bit_5 -X58_bit_4 X58_bit_3 X58_bit_2 X58_bit_1 X58_bit0 X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 X59_bit_7 -X59_bit_6 X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 X59_bit3 X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 X60_bit_6 X60_bit_5 -X60_bit_4 X60_bit_3 -X60_bit_2 X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 X62_bit_7 X62_bit_6 X62_bit_5 X62_bit_4 X62_bit_3 X62_bit_2 X62_bit_1 X62_bit0 X62_bit1 X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 X63_bit_6 X63_bit_5 -X63_bit_4 X63_bit_3 X63_bit_2 X63_bit_1 -X63_bit0 X63_bit1 -X63_bit2 X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 X66_bit_6 X66_bit_5 X66_bit_4 X66_bit_3 X66_bit_2 X66_bit_1 X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 X68_bit_7 -X68_bit_6 X68_bit_5 X68_bit_4 X68_bit_3 -X68_bit_2 X68_bit_1 -X68_bit0 X68_bit1 X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 X69_bit_6 X69_bit_5 X69_bit_4 -X69_bit_3 -X69_bit_2 X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 X72_bit_5 X72_bit_4 X72_bit_3 X72_bit_2 X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 X73_bit_7 X73_bit_6 -X73_bit_5 X73_bit_4 -X73_bit_3 X73_bit_2 X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 X76_bit_7 -X76_bit_6 X76_bit_5 X76_bit_4 X76_bit_3 X76_bit_2 X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 X77_bit_7 X77_bit_6 X77_bit_5 X77_bit_4 -X77_bit_3 X77_bit_2 X77_bit_1 X77_bit0 -X77_bit1 X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 X81_bit_4 X81_bit_3 X81_bit_2 -X81_bit_1 -X81_bit0 X81_bit1 -X81_bit2 X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 X82_bit_7 -X82_bit_6 -X82_bit_5 X82_bit_4 X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 X83_bit_6 -X83_bit_5 X83_bit_4 -X83_bit_3 -X83_bit_2 X83_bit_1 -X83_bit0 -X83_bit1 X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 X86_bit_5 X86_bit_4 -X86_bit_3 X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 X88_bit_6 -X88_bit_5 -X88_bit_4 X88_bit_3 X88_bit_2 X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 -X89_bit_6 -X89_bit_5 -X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 -X98_bit_6 -X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 -X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 X99_bit1 X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 -X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X101_bit_7 -X101_bit_6 -X101_bit_5 -X101_bit_4 -X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 -X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 -X104_bit_6 -X104_bit_5 -X104_bit_4 -X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X105_bit_7 -X105_bit_6 -X105_bit_5 -X105_bit_4 -X105_bit_3 -X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 -X106_bit_7 -X106_bit_6 -X106_bit_5 -X106_bit_4 -X106_bit_3 -X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X107_bit_7 -X107_bit_6 -X107_bit_5 -X107_bit_4 X107_bit_3 -X107_bit_2 X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 -X108_bit_6 -X108_bit_5 -X108_bit_4 -X108_bit_3 -X108_bit_2 X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 -X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 -X110_bit_6 -X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 -X111_bit_7 -X111_bit_6 -X111_bit_5 -X111_bit_4 X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 -X112_bit_5 -X112_bit_4 X112_bit_3 -X112_bit_2 -X112_bit_1 -X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 -X115_bit_6 X115_bit_5 -X115_bit_4 X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 -X116_bit_7 -X116_bit_6 -X116_bit_5 X116_bit_4 X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 -X117_bit_6 -X117_bit_5 -X117_bit_4 -X117_bit_3 -X117_bit_2 -X117_bit_1 -X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 -X118_bit_7 -X118_bit_6 -X118_bit_5 -X118_bit_4 X118_bit_3 -X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 -X119_bit_7 -X119_bit_6 -X119_bit_5 -X119_bit_4 -X119_bit_3 -X119_bit_2 -X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 -X120_bit_7 X120_bit_6 X120_bit_5 -X120_bit_4 X120_bit_3 -X120_bit_2 -X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 -X121_bit_6 X121_bit_5 -X121_bit_4 X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 -X122_bit_6 -X122_bit_5 -X122_bit_4 X122_bit_3 -X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 -X123_bit_6 -X123_bit_5 -X123_bit_4 -X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 -X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 -X124_bit_7 -X124_bit_6 -X124_bit_5 X124_bit_4 X124_bit_3 -X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 -X125_bit_7 -X125_bit_6 -X125_bit_5 -X125_bit_4 -X125_bit_3 -X125_bit_2 -X125_bit_1 -X125_bit0 -X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 -X126_bit_7 -X126_bit_6 -X126_bit_5 -X126_bit_4 X126_bit_3 -X126_bit_2 -X126_bit_1 -X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 -X127_bit_7 -X127_bit_6 -X127_bit_5 -X127_bit_4 -X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X128_bit_7 -X128_bit_6 -X128_bit_5 -X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 -X129_bit_7 -X129_bit_6 X129_bit_5 X129_bit_4 -X129_bit_3 -X129_bit_2 -X129_bit_1 -X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X130_bit_7 X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 -X130_bit_1 -X130_bit0 -X130_bit1 X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X131_bit_7 X131_bit_6 X131_bit_5 -X131_bit_4 X131_bit_3 -X131_bit_2 -X131_bit_1 -X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 -X132_bit_7 -X132_bit_6 -X132_bit_5 -X132_bit_4 -X132_bit_3 -X132_bit_2 -X132_bit_1 -X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 -X133_bit_6 X133_bit_5 X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 -X134_bit_7 -X134_bit_6 X134_bit_5 -X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 -X135_bit_7 -X135_bit_6 -X135_bit_5 X135_bit_4 X135_bit_3 -X135_bit_2 -X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 -X136_bit_7 -X136_bit_6 -X136_bit_5 -X136_bit_4 -X136_bit_3 -X136_bit_2 -X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 -X137_bit_7 -X137_bit_6 -X137_bit_5 -X137_bit_4 -X137_bit_3 -X137_bit_2 -X137_bit_1 -X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 -X138_bit_7 -X138_bit_6 -X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 -X139_bit_7 -X139_bit_6 -X139_bit_5 -X139_bit_4 -X139_bit_3 -X139_bit_2 -X139_bit_1 -X139_bit0 -X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 -X140_bit_7 -X140_bit_6 -X140_bit_5 -X140_bit_4 -X140_bit_3 -X140_bit_2 -X140_bit_1 -X140_bit0 -X140_bit1 -X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 -X141_bit_7 -X141_bit_6 -X141_bit_5 -X141_bit_4 -X141_bit_3 -X141_bit_2 -X141_bit_1 -X141_bit0 -X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 -X142_bit_7 -X142_bit_6 -X142_bit_5 -X142_bit_4 -X142_bit_3 -X142_bit_2 -X142_bit_1 -X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 -X143_bit_7 -X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 -X144_bit_7 -X144_bit_6 -X144_bit_5 X144_bit_4 -X144_bit_3 -X144_bit_2 -X144_bit_1 -X144_bit0 -X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 -X145_bit_7 -X145_bit_6 -X145_bit_5 X145_bit_4 -X145_bit_3 -X145_bit_2 -X145_bit_1 X145_bit0 -X145_bit1 -X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 -X146_bit_7 -X146_bit_6 -X146_bit_5 -X146_bit_4 -X146_bit_3 -X146_bit_2 -X146_bit_1 -X146_bit0 -X146_bit1 -X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 -X147_bit_7 -X147_bit_6 -X147_bit_5 -X147_bit_4 -X147_bit_3 -X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 -X148_bit_7 -X148_bit_6 -X148_bit_5 -X148_bit_4 -X148_bit_3 -X148_bit_2 -X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 -X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 -X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 -X150_bit_7 -X150_bit_6 -X150_bit_5 -X150_bit_4 -X150_bit_3 -X150_bit_2 -X150_bit_1 -X150_bit0 -X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 -X151_bit_3 -X151_bit_2 -X151_bit_1 -X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 -X152_bit_6 -X152_bit_5 -X152_bit_4 -X152_bit_3 -X152_bit_2 -X152_bit_1 X152_bit0 -X152_bit1 -X152_bit2 X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 -X153_bit_7 -X153_bit_6 -X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 -X154_bit_7 -X154_bit_6 -X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 -X154_bit_1 -X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 -X155_bit_7 X155_bit_6 X155_bit_5 -X155_bit_4 -X155_bit_3 -X155_bit_2 -X155_bit_1 -X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 -X156_bit_6 -X156_bit_5 -X156_bit_4 -X156_bit_3 -X156_bit_2 -X156_bit_1 -X156_bit0 -X156_bit1 -X156_bit2 X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 -X157_bit_7 -X157_bit_6 -X157_bit_5 -X157_bit_4 -X157_bit_3 -X157_bit_2 -X157_bit_1 -X157_bit0 -X157_bit1 -X157_bit2 X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X158_bit_7 -X158_bit_6 X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 -X158_bit_1 -X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X159_bit_7 -X159_bit_6 -X159_bit_5 -X159_bit_4 -X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 -X160_bit_7 -X160_bit_6 -X160_bit_5 -X160_bit_4 -X160_bit_3 -X160_bit_2 -X160_bit_1 -X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X161_bit_7 -X161_bit_6 -X161_bit_5 -X161_bit_4 -X161_bit_3 -X161_bit_2 -X161_bit_1 -X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 -X162_bit_7 -X162_bit_6 -X162_bit_5 -X162_bit_4 -X162_bit_3 -X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 -X163_bit_7 X163_bit_6 X163_bit_5 X163_bit_4 X163_bit_3 X163_bit_2 X163_bit_1 -X163_bit0 -X163_bit1 X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 -X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X165_bit_7 -X165_bit_6 -X165_bit_5 -X165_bit_4 -X165_bit_3 -X165_bit_2 -X165_bit_1 -X165_bit0 -X165_bit1 X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 -X166_bit_7 -X166_bit_6 -X166_bit_5 -X166_bit_4 -X166_bit_3 -X166_bit_2 -X166_bit_1 -X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 -X167_bit_7 -X167_bit_6 -X167_bit_5 X167_bit_4 X167_bit_3 -X167_bit_2 -X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 -X168_bit_7 -X168_bit_6 -X168_bit_5 -X168_bit_4 -X168_bit_3 -X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -X169_bit_7 -X169_bit_6 -X169_bit_5 -X169_bit_4 -X169_bit_3 -X169_bit_2 -X169_bit_1 -X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 -X170_bit_7 -X170_bit_6 X170_bit_5 -X170_bit_4 -X170_bit_3 -X170_bit_2 -X170_bit_1 -X170_bit0 -X170_bit1 -X170_bit2 X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 -X171_bit_7 -X171_bit_6 -X171_bit_5 -X171_bit_4 -X171_bit_3 -X171_bit_2 -X171_bit_1 -X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 -X172_bit_6 -X172_bit_5 -X172_bit_4 -X172_bit_3 X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 -X173_bit_7 -X173_bit_6 -X173_bit_5 -X173_bit_4 -X173_bit_3 -X173_bit_2 -X173_bit_1 -X173_bit0 -X173_bit1 -X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 X174_bit_7 -X174_bit_6 X174_bit_5 X174_bit_4 X174_bit_3 X174_bit_2 X174_bit_1 -X174_bit0 -X174_bit1 -X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 -X175_bit_7 -X175_bit_6 -X175_bit_5 -X175_bit_4 -X175_bit_3 -X175_bit_2 -X175_bit_1 -X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 -X176_bit_7 -X176_bit_6 -X176_bit_5 -X176_bit_4 -X176_bit_3 -X176_bit_2 -X176_bit_1 -X176_bit0 -X176_bit1 -X176_bit2 -X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 X177_bit_7 X177_bit_6 X177_bit_5 X177_bit_4 X177_bit_3 -X177_bit_2 -X177_bit_1 -X177_bit0 -X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 -X178_bit_7 -X178_bit_6 -X178_bit_5 -X178_bit_4 X178_bit_3 -X178_bit_2 -X178_bit_1 -X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 -X179_bit_7 -X179_bit_6 -X179_bit_5 -X179_bit_4 -X179_bit_3 -X179_bit_2 -X179_bit_1 -X179_bit0 -X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 -X180_bit_7 -X180_bit_6 -X180_bit_5 -X180_bit_4 -X180_bit_3 -X180_bit_2 -X180_bit_1 -X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 -X181_bit_7 -X181_bit_6 -X181_bit_5 -X181_bit_4 -X181_bit_3 -X181_bit_2 -X181_bit_1 -X181_bit0 -X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 -X182_bit_7 -X182_bit_6 -X182_bit_5 -X182_bit_4 -X182_bit_3 -X182_bit_2 -X182_bit_1 -X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 -X183_bit_7 -X183_bit_6 -X183_bit_5 -X183_bit_4 -X183_bit_3 -X183_bit_2 -X183_bit_1 -X183_bit0 -X183_bit1 -X183_bit2 -X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 -X184_bit_7 -X184_bit_6 -X184_bit_5 -X184_bit_4 -X184_bit_3 -X184_bit_2 -X184_bit_1 -X184_bit0 -X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 -X185_bit_7 -X185_bit_6 -X185_bit_5 -X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 -X186_bit_6 -X186_bit_5 -X186_bit_4 -X186_bit_3 -X186_bit_2 -X186_bit_1 -X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 X187_bit_7 -X187_bit_6 X187_bit_5 X187_bit_4 -X187_bit_3 -X187_bit_2 -X187_bit_1 -X187_bit0 X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 -X188_bit_7 -X188_bit_6 X188_bit_5 X188_bit_4 -X188_bit_3 -X188_bit_2 -X188_bit_1 -X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 -X189_bit_7 -X189_bit_6 -X189_bit_5 -X189_bit_4 -X189_bit_3 -X189_bit_2 -X189_bit_1 -X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -X190_bit_7 -X190_bit_6 -X190_bit_5 -X190_bit_4 -X190_bit_3 -X190_bit_2 -X190_bit_1 -X190_bit0 -X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 X191_bit_7 -X191_bit_6 -X191_bit_5 -X191_bit_4 -X191_bit_3 -X191_bit_2 -X191_bit_1 -X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 -X192_bit_7 -X192_bit_6 -X192_bit_5 -X192_bit_4 -X192_bit_3 -X192_bit_2 -X192_bit_1 -X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 -X193_bit_6 -X193_bit_5 -X193_bit_4 -X193_bit_3 -X193_bit_2 -X193_bit_1 -X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 -X194_bit_7 X194_bit_6 -X194_bit_5 X194_bit_4 -X194_bit_3 -X194_bit_2 -X194_bit_1 -X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 -X195_bit_7 X195_bit_6 -X195_bit_5 -X195_bit_4 -X195_bit_3 -X195_bit_2 -X195_bit_1 -X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 -X196_bit_7 -X196_bit_6 -X196_bit_5 -X196_bit_4 -X196_bit_3 -X196_bit_2 -X196_bit_1 -X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 X197_bit_7 X197_bit_6 -X197_bit_5 -X197_bit_4 X197_bit_3 -X197_bit_2 -X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 X198_bit_7 -X198_bit_6 X198_bit_5 X198_bit_4 -X198_bit_3 -X198_bit_2 -X198_bit_1 -X198_bit0 -X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 X199_bit_7 -X199_bit_6 -X199_bit_5 X199_bit_4 -X199_bit_3 X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 -X200_bit_7 -X200_bit_6 -X200_bit_5 -X200_bit_4 -X200_bit_3 -X200_bit_2 -X200_bit_1 -X200_bit0 -X200_bit1 -X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 X201_bit_7 -X201_bit_6 -X201_bit_5 X201_bit_4 X201_bit_3 X201_bit_2 X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 -X202_bit_7 X202_bit_6 -X202_bit_5 -X202_bit_4 -X202_bit_3 -X202_bit_2 -X202_bit_1 -X202_bit0 -X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 -X203_bit_7 -X203_bit_6 -X203_bit_5 -X203_bit_4 -X203_bit_3 -X203_bit_2 -X203_bit_1 -X203_bit0 -X203_bit1 -X203_bit2 -X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 -X204_bit_6 -X204_bit_5 -X204_bit_4 -X204_bit_3 -X204_bit_2 -X204_bit_1 -X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 X205_bit_7 -X205_bit_6 -X205_bit_5 X205_bit_4 X205_bit_3 -X205_bit_2 -X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 X206_bit_7 X206_bit_6 X206_bit_5 X206_bit_4 X206_bit_3 X206_bit_2 X206_bit_1 -X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 -X207_bit_7 -X207_bit_6 -X207_bit_5 -X207_bit_4 -X207_bit_3 -X207_bit_2 -X207_bit_1 -X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 -X208_bit_7 X208_bit_6 -X208_bit_5 -X208_bit_4 X208_bit_3 X208_bit_2 -X208_bit_1 -X208_bit0 -X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 -X209_bit_7 -X209_bit_6 -X209_bit_5 -X209_bit_4 -X209_bit_3 -X209_bit_2 -X209_bit_1 -X209_bit0 -X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 -X210_bit_7 -X210_bit_6 -X210_bit_5 -X210_bit_4 -X210_bit_3 -X210_bit_2 -X210_bit_1 -X210_bit0 -X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 -X211_bit_7 -X211_bit_6 -X211_bit_5 -X211_bit_4 -X211_bit_3 -X211_bit_2 -X211_bit_1 -X211_bit0 -X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 -X212_bit_7 -X212_bit_6 -X212_bit_5 -X212_bit_4 -X212_bit_3 -X212_bit_2 -X212_bit_1 -X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 -X213_bit_7 -X213_bit_6 -X213_bit_5 -X213_bit_4 -X213_bit_3 -X213_bit_2 -X213_bit_1 -X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 -X214_bit_7 -X214_bit_6 -X214_bit_5 -X214_bit_4 -X214_bit_3 -X214_bit_2 -X214_bit_1 -X214_bit0 -X214_bit1 -X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 -X215_bit_7 -X215_bit_6 -X215_bit_5 -X215_bit_4 -X215_bit_3 -X215_bit_2 -X215_bit_1 -X215_bit0 -X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 -X216_bit_7 -X216_bit_6 -X216_bit_5 -X216_bit_4 -X216_bit_3 -X216_bit_2 -X216_bit_1 -X216_bit0 -X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 -X217_bit_7 X217_bit_6 X217_bit_5 X217_bit_4 X217_bit_3 X217_bit_2 X217_bit_1 -X217_bit0 -X217_bit1 -X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 -X218_bit_7 -X218_bit_6 -X218_bit_5 -X218_bit_4 -X218_bit_3 -X218_bit_2 -X218_bit_1 -X218_bit0 -X218_bit1 X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 -X219_bit_7 X219_bit_6 X219_bit_5 -X219_bit_4 -X219_bit_3 -X219_bit_2 -X219_bit_1 -X219_bit0 -X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 -X220_bit_7 -X220_bit_6 -X220_bit_5 -X220_bit_4 -X220_bit_3 -X220_bit_2 -X220_bit_1 -X220_bit0 -X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 X221_bit_7 -X221_bit_6 -X221_bit_5 X221_bit_4 X221_bit_3 X221_bit_2 X221_bit_1 X221_bit0 -X221_bit1 X221_bit2 X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 -X222_bit_7 -X222_bit_6 -X222_bit_5 -X222_bit_4 -X222_bit_3 -X222_bit_2 -X222_bit_1 -X222_bit0 -X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 -X223_bit_6 -X223_bit_5 -X223_bit_4 -X223_bit_3 -X223_bit_2 -X223_bit_1 X223_bit0 X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 -X224_bit_7 -X224_bit_6 -X224_bit_5 -X224_bit_4 -X224_bit_3 -X224_bit_2 -X224_bit_1 -X224_bit0 -X224_bit1 X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 X225_bit_7 X225_bit_6 X225_bit_5 X225_bit_4 -X225_bit_3 -X225_bit_2 -X225_bit_1 X225_bit0 -X225_bit1 -X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 X226_bit_7 X226_bit_6 X226_bit_5 -X226_bit_4 X226_bit_3 -X226_bit_2 -X226_bit_1 X226_bit0 -X226_bit1 X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 X227_bit_7 -X227_bit_6 -X227_bit_5 -X227_bit_4 -X227_bit_3 X227_bit_2 -X227_bit_1 -X227_bit0 X227_bit1 X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 -X228_bit_7 -X228_bit_6 -X228_bit_5 -X228_bit_4 -X228_bit_3 -X228_bit_2 -X228_bit_1 -X228_bit0 -X228_bit1 -X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 -X229_bit_7 -X229_bit_6 -X229_bit_5 -X229_bit_4 -X229_bit_3 -X229_bit_2 -X229_bit_1 -X229_bit0 -X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 X230_bit_7 X230_bit_6 X230_bit_5 X230_bit_4 X230_bit_3 X230_bit_2 X230_bit_1 X230_bit0 X230_bit1 -X230_bit2 -X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 X231_bit_7 X231_bit_6 X231_bit_5 -X231_bit_4 -X231_bit_3 X231_bit_2 X231_bit_1 X231_bit0 -X231_bit1 X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 -X232_bit_7 X232_bit_6 -X232_bit_5 X232_bit_4 -X232_bit_3 X232_bit_2 -X232_bit_1 X232_bit0 -X232_bit1 -X232_bit2 X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 -X233_bit_7 -X233_bit_6 -X233_bit_5 -X233_bit_4 -X233_bit_3 -X233_bit_2 -X233_bit_1 -X233_bit0 -X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 -X234_bit_7 -X234_bit_6 -X234_bit_5 -X234_bit_4 -X234_bit_3 -X234_bit_2 -X234_bit_1 -X234_bit0 -X234_bit1 -X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 X235_bit_7 -X235_bit_6 -X235_bit_5 -X235_bit_4 -X235_bit_3 -X235_bit_2 -X235_bit_1 X235_bit0 X235_bit1 X235_bit2 -X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 -X236_bit_7 -X236_bit_6 -X236_bit_5 -X236_bit_4 -X236_bit_3 -X236_bit_2 -X236_bit_1 -X236_bit0 -X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 X237_bit_7 X237_bit_6 X237_bit_5 -X237_bit_4 -X237_bit_3 X237_bit_2 -X237_bit_1 -X237_bit0 -X237_bit1 -X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 -X238_bit_7 -X238_bit_6 -X238_bit_5 -X238_bit_4 -X238_bit_3 -X238_bit_2 -X238_bit_1 -X238_bit0 -X238_bit1 -X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 -X239_bit_6 -X239_bit_5 -X239_bit_4 -X239_bit_3 -X239_bit_2 -X239_bit_1 -X239_bit0 X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 -X240_bit_7 -X240_bit_6 -X240_bit_5 -X240_bit_4 -X240_bit_3 -X240_bit_2 -X240_bit_1 -X240_bit0 -X240_bit1 -X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 -X241_bit_7 -X241_bit_6 -X241_bit_5 -X241_bit_4 -X241_bit_3 -X241_bit_2 -X241_bit_1 -X241_bit0 -X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 X242_bit_7 X242_bit_6 -X242_bit_5 -X242_bit_4 X242_bit_3 -X242_bit_2 X242_bit_1 -X242_bit0 X242_bit1 X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 -X243_bit_7 -X243_bit_6 -X243_bit_5 -X243_bit_4 -X243_bit_3 -X243_bit_2 -X243_bit_1 -X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 -X244_bit_7 -X244_bit_6 X244_bit_5 -X244_bit_4 X244_bit_3 X244_bit_2 X244_bit_1 X244_bit0 X244_bit1 -X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 -X245_bit_7 -X245_bit_6 -X245_bit_5 -X245_bit_4 -X245_bit_3 -X245_bit_2 -X245_bit_1 -X245_bit0 -X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 -X246_bit_7 -X246_bit_6 -X246_bit_5 -X246_bit_4 -X246_bit_3 -X246_bit_2 -X246_bit_1 -X246_bit0 X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 -X247_bit_7 -X247_bit_6 -X247_bit_5 -X247_bit_4 X247_bit_3 X247_bit_2 X247_bit_1 -X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 X248_bit_7 -X248_bit_6 X248_bit_5 -X248_bit_4 X248_bit_3 X248_bit_2 X248_bit_1 -X248_bit0 -X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 X249_bit_7 X249_bit_6 X249_bit_5 X249_bit_4 X249_bit_3 X249_bit_2 X249_bit_1 -X249_bit0 -X249_bit1 X249_bit2 -X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 -X250_bit_7 -X250_bit_6 X250_bit_5 X250_bit_4 -X250_bit_3 X250_bit_2 X250_bit_1 X250_bit0 -X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 -X251_bit_7 X251_bit_6 X251_bit_5 X251_bit_4 X251_bit_3 X251_bit_2 -X251_bit_1 X251_bit0 -X251_bit1 X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 X252_bit_7 -X252_bit_6 -X252_bit_5 X252_bit_4 -X252_bit_3 -X252_bit_2 -X252_bit_1 -X252_bit0 -X252_bit1 X252_bit2 X252_bit3 -X252_bit4 -X252_bit5 -X252_bit6 -X252_bit7 -X252_bit8 -X252_bit9 -X252_bit10 -X252_bit11 -X252_bit12 -X253_bit_7 -X253_bit_6 -X253_bit_5 -X253_bit_4 -X253_bit_3 -X253_bit_2 -X253_bit_1 -X253_bit0 -X253_bit1 -X253_bit2 -X253_bit3 -X253_bit4 -X253_bit5 -X253_bit6 -X253_bit7 -X253_bit8 -X253_bit9 -X253_bit10 -X253_bit11 -X253_bit12 -X254_bit_7 -X254_bit_6 -X254_bit_5 -X254_bit_4 -X254_bit_3 -X254_bit_2 -X254_bit_1 -X254_bit0 -X254_bit1 -X254_bit2 -X254_bit3 -X254_bit4 -X254_bit5 -X254_bit6 -X254_bit7 -X254_bit8 -X254_bit9 -X254_bit10 -X254_bit11 -X254_bit12 -X255_bit_7 X255_bit_6 X255_bit_5 -X255_bit_4 -X255_bit_3 X255_bit_2 -X255_bit_1 -X255_bit0 -X255_bit1 -X255_bit2 X255_bit3 -X255_bit4 -X255_bit5 -X255_bit6 -X255_bit7 -X255_bit8 -X255_bit9 -X255_bit10 -X255_bit11 -X255_bit12 -X256_bit_7 -X256_bit_6 -X256_bit_5 -X256_bit_4 -X256_bit_3 -X256_bit_2 -X256_bit_1 -X256_bit0 -X256_bit1 -X256_bit2 -X256_bit3 -X256_bit4 -X256_bit5 -X256_bit6 -X256_bit7 -X256_bit8 -X256_bit9 -X256_bit10 -X256_bit11 -X256_bit12 -X257_bit_7 -X257_bit_6 -X257_bit_5 -X257_bit_4 -X257_bit_3 -X257_bit_2 -X257_bit_1 -X257_bit0 X257_bit1 -X257_bit2 -X257_bit3 -X257_bit4 -X257_bit5 -X257_bit6 -X257_bit7 -X257_bit8 -X257_bit9 -X257_bit10 -X257_bit11 -X257_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_bit#### 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.92 0.97 0.90 2/54 7740
Raw data (stat): 7740 (runsolver) R 7739 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486296276 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 4106 0 0 0 986 11 0 0 25 0 1 0 486296276 19570688 3920 4294967295 134512640 134672761 3221224624 3221223796 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4778 3920 603 41 0 4737 0
vsize: 19112
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 4124 0 0 0 1986 12 0 0 25 0 1 0 486296276 19701760 3938 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4810 3938 603 41 0 4769 0
vsize: 19240
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 4158 0 0 0 2986 12 0 0 25 0 1 0 486296276 19877888 3972 4294967295 134512640 134672761 3221224624 3221223784 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4853 3972 603 41 0 4812 0
vsize: 19412
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 4195 0 0 0 3986 12 0 0 25 0 1 0 486296276 19877888 4009 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4853 4009 603 41 0 4812 0
vsize: 19412
[startup+50.0009 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 4219 0 0 0 4986 12 0 0 25 0 1 0 486296276 20013056 4033 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4886 4033 603 41 0 4845 0
vsize: 19544
[startup+60.0009 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 4288 0 0 0 5985 13 0 0 25 0 1 0 486296276 20430848 4102 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4988 4102 603 41 0 4947 0
vsize: 19952
[startup+70.0015 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 4308 0 0 0 6986 13 0 0 25 0 1 0 486296276 20430848 4122 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4988 4122 603 41 0 4947 0
vsize: 19952
[startup+80.0019 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 4411 0 0 0 7986 13 0 0 25 0 1 0 486296276 20836352 4225 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4225 603 41 0 5046 0
vsize: 20348
[startup+90.0019 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 10802 0 0 0 8971 27 0 0 25 0 1 0 486296276 42897408 9413 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10473 9413 603 41 0 10432 0
vsize: 41892
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 10919 0 0 0 9971 27 0 0 25 0 1 0 486296276 43302912 9530 4294967295 134512640 134672761 3221224624 3221223792 134560767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10572 9530 603 41 0 10531 0
vsize: 42288
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 11047 0 0 0 10971 28 0 0 25 0 1 0 486296276 43970560 9658 4294967295 134512640 134672761 3221224624 3221223796 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10735 9658 603 41 0 10694 0
vsize: 42940
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 11454 0 0 0 11970 29 0 0 25 0 1 0 486296276 45436928 10013 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11093 10013 603 41 0 11052 0
vsize: 44372
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 11482 0 0 0 12970 29 0 0 25 0 1 0 486296276 45436928 10041 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11093 10041 603 41 0 11052 0
vsize: 44372
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 12019 0 0 0 13967 31 0 0 25 0 1 0 486296276 47591424 10578 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11619 10578 603 41 0 11578 0
vsize: 46476
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 12252 0 0 0 14967 32 0 0 25 0 1 0 486296276 48144384 10722 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11754 10722 603 41 0 11713 0
vsize: 47016
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 12405 0 0 0 15967 32 0 0 25 0 1 0 486296276 49074176 10875 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11981 10875 603 41 0 11940 0
vsize: 47924
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 12707 0 0 0 16967 32 0 0 25 0 1 0 486296276 50286592 11177 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12277 11177 603 41 0 12236 0
vsize: 49108
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 12903 0 0 0 17967 33 0 0 25 0 1 0 486296276 51097600 11373 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12475 11373 603 41 0 12434 0
vsize: 49900
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 12987 0 0 0 18967 33 0 0 25 0 1 0 486296276 51367936 11457 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12541 11457 603 41 0 12500 0
vsize: 50164
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 13725 0 0 0 19965 35 0 0 25 0 1 0 486296276 54452224 12195 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13294 12195 603 41 0 13253 0
vsize: 53176
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 14355 0 0 0 20964 36 0 0 25 0 1 0 486296276 56872960 12825 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13885 12825 603 41 0 13844 0
vsize: 55540
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 21962 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 22962 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 23962 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 24962 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 25962 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 26962 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 27963 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223840 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 28963 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 29963 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223792 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 30963 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 31964 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223748 134566133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 32964 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223792 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 33964 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223792 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15052 0 0 0 34964 39 0 0 25 0 1 0 486296276 59281408 13420 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 13420 603 41 0 14432 0
vsize: 57892
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 15586 0 0 0 35963 40 0 0 25 0 1 0 486296276 61571072 13954 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15032 13954 603 41 0 14991 0
vsize: 60128
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7740
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 36962 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+380.009 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 7793
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 37962 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+390.01 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 7793
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 38963 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+400.009 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 7793
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 39963 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+410.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 7793
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 40963 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+420.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 7793
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 41963 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+430.011 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 7793
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 42963 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+440.012 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 7793
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 43964 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+450.012 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 44964 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+460.012 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 45964 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+470.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 46964 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223760 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+480.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 47964 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+490.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16017 0 0 0 48965 41 0 0 25 0 1 0 486296276 62808064 14281 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14281 603 41 0 15293 0
vsize: 61336
[startup+500.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16056 0 0 0 49965 41 0 0 25 0 1 0 486296276 63078400 14320 4294967295 134512640 134672761 3221224624 3221223824 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15400 14320 603 41 0 15359 0
vsize: 61600
[startup+510.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 16673 0 0 0 50963 43 0 0 25 0 1 0 486296276 65499136 14937 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15991 14937 603 41 0 15950 0
vsize: 63964
[startup+520.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 17201 0 0 0 51961 45 0 0 25 0 1 0 486296276 67657728 15465 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16518 15465 603 41 0 16477 0
vsize: 66072
[startup+530.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 17702 0 0 0 52961 46 0 0 25 0 1 0 486296276 69816320 15966 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17045 15966 603 41 0 17004 0
vsize: 68180
[startup+540.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 18086 0 0 0 53960 47 0 0 25 0 1 0 486296276 71303168 16350 4294967295 134512640 134672761 3221224624 3221223808 134558697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17408 16350 603 41 0 17367 0
vsize: 69632
[startup+550.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 18940 0 0 0 54958 49 0 0 25 0 1 0 486296276 74805248 17204 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18263 17204 603 41 0 18222 0
vsize: 73052
[startup+560.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 19799 0 0 0 55955 52 0 0 25 0 1 0 486296276 78311424 18063 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19119 18063 603 41 0 19078 0
vsize: 76476
[startup+570.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 20543 0 0 0 56954 53 0 0 25 0 1 0 486296276 81281024 18807 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19844 18807 603 41 0 19803 0
vsize: 79376
[startup+580.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 21268 0 0 0 57952 56 0 0 25 0 1 0 486296276 84242432 19532 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 19532 603 41 0 20526 0
vsize: 82268
[startup+590.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 22088 0 0 0 58950 58 0 0 25 0 1 0 486296276 88133632 20352 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21517 20352 603 41 0 21476 0
vsize: 86068
[startup+600.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 22781 0 0 0 59949 59 0 0 25 0 1 0 486296276 90959872 21045 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22207 21045 603 41 0 22166 0
vsize: 88828
[startup+610.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 23629 0 0 0 60947 61 0 0 25 0 1 0 486296276 94470144 21893 4294967295 134512640 134672761 3221224624 3221223728 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23064 21893 603 41 0 23023 0
vsize: 92256
[startup+620.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 24227 0 0 0 61945 63 0 0 25 0 1 0 486296276 96903168 22491 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23658 22491 603 41 0 23617 0
vsize: 94632
[startup+630.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 24693 0 0 0 62944 64 0 0 25 0 1 0 486296276 98791424 22957 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24119 22957 603 41 0 24078 0
vsize: 96476
[startup+640.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 25097 0 0 0 63943 66 0 0 25 0 1 0 486296276 100409344 23361 4294967295 134512640 134672761 3221224624 3221223728 134560039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24514 23361 603 41 0 24473 0
vsize: 98056
[startup+650.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 25338 0 0 0 64942 67 0 0 25 0 1 0 486296276 101355520 23602 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24745 23602 603 41 0 24704 0
vsize: 98980
[startup+660.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 26060 0 0 0 65941 68 0 0 25 0 1 0 486296276 104321024 24324 4294967295 134512640 134672761 3221224624 3221223728 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25469 24324 603 41 0 25428 0
vsize: 101876
[startup+670.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 26918 0 0 0 66938 71 0 0 25 0 1 0 486296276 107810816 25182 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26321 25182 603 41 0 26280 0
vsize: 105284
[startup+680.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 27794 0 0 0 67937 72 0 0 25 0 1 0 486296276 111443968 26058 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27208 26058 603 41 0 27167 0
vsize: 108832
[startup+690.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 28600 0 0 0 68935 74 0 0 25 0 1 0 486296276 114679808 26864 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27998 26864 603 41 0 27957 0
vsize: 111992
[startup+700.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 29323 0 0 0 69933 76 0 0 25 0 1 0 486296276 117637120 27587 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28720 27587 603 41 0 28679 0
vsize: 114880
[startup+710.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 30040 0 0 0 70932 78 0 0 25 0 1 0 486296276 120594432 28304 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29442 28304 603 41 0 29401 0
vsize: 117768
[startup+720.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 30660 0 0 0 71932 79 0 0 25 0 1 0 486296276 123162624 28924 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30069 28924 603 41 0 30028 0
vsize: 120276
[startup+730.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 31316 0 0 0 72930 81 0 0 25 0 1 0 486296276 125845504 29580 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30724 29580 603 41 0 30683 0
vsize: 122896
[startup+740.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 31919 0 0 0 73929 82 0 0 25 0 1 0 486296276 128266240 30183 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31315 30183 603 41 0 31274 0
vsize: 125260
[startup+750.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7795
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 32463 0 0 0 74927 84 0 0 25 0 1 0 486296276 130416640 30727 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31840 30727 603 41 0 31799 0
vsize: 127360
[startup+760.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 33149 0 0 0 75926 86 0 0 25 0 1 0 486296276 133251072 31413 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32532 31413 603 41 0 32491 0
vsize: 130128
[startup+770.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 33655 0 0 0 76925 87 0 0 25 0 1 0 486296276 135405568 31919 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 31919 603 41 0 33017 0
vsize: 132232
[startup+780.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 34204 0 0 0 77924 88 0 0 25 0 1 0 486296276 137572352 32468 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33587 32468 603 41 0 33546 0
vsize: 134348
[startup+790.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 34751 0 0 0 78924 89 0 0 25 0 1 0 486296276 139886592 33015 4294967295 134512640 134672761 3221224624 3221223728 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34152 33015 603 41 0 34111 0
vsize: 136608
[startup+800.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 35260 0 0 0 79922 91 0 0 25 0 1 0 486296276 141926400 33524 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34650 33524 603 41 0 34609 0
vsize: 138600
[startup+810.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 35566 0 0 0 80922 92 0 0 25 0 1 0 486296276 143138816 33830 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34946 33830 603 41 0 34905 0
vsize: 139784
[startup+820.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 35907 0 0 0 81921 93 0 0 25 0 1 0 486296276 144490496 34171 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35276 34171 603 41 0 35235 0
vsize: 141104
[startup+830.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 36268 0 0 0 82920 93 0 0 25 0 1 0 486296276 145973248 34532 4294967295 134512640 134672761 3221224624 3221223728 134560390 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35638 34532 603 41 0 35597 0
vsize: 142552
[startup+840.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 36640 0 0 0 83920 94 0 0 25 0 1 0 486296276 147456000 34904 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36000 34904 603 41 0 35959 0
vsize: 144000
[startup+850.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 37047 0 0 0 84918 96 0 0 25 0 1 0 486296276 149196800 35311 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36425 35311 603 41 0 36384 0
vsize: 145700
[startup+860.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 37466 0 0 0 85918 97 0 0 25 0 1 0 486296276 150953984 35730 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36854 35730 603 41 0 36813 0
vsize: 147416
[startup+870.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 37859 0 0 0 86916 98 0 0 25 0 1 0 486296276 152432640 36123 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37215 36123 603 41 0 37174 0
vsize: 148860
[startup+880.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 38344 0 0 0 87915 100 0 0 25 0 1 0 486296276 154456064 36608 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37709 36608 603 41 0 37668 0
vsize: 150836
[startup+890.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 38793 0 0 0 88913 101 0 0 25 0 1 0 486296276 156340224 37057 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38169 37057 603 41 0 38128 0
vsize: 152676
[startup+900.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 39463 0 0 0 89911 103 0 0 25 0 1 0 486296276 159031296 37727 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38826 37727 603 41 0 38785 0
vsize: 155304
[startup+910.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 39938 0 0 0 90910 105 0 0 25 0 1 0 486296276 160907264 38202 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39284 38202 603 41 0 39243 0
vsize: 157136
[startup+920.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 40348 0 0 0 91909 106 0 0 25 0 1 0 486296276 162525184 38612 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39679 38612 603 41 0 39638 0
vsize: 158716
[startup+930.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 40736 0 0 0 92909 106 0 0 25 0 1 0 486296276 164130816 39000 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40071 39000 603 41 0 40030 0
vsize: 160284
[startup+940.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 41067 0 0 0 93909 107 0 0 25 0 1 0 486296276 166543360 39331 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40660 39331 603 41 0 40619 0
vsize: 162640
[startup+950.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 41375 0 0 0 94908 108 0 0 25 0 1 0 486296276 167809024 39639 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40969 39639 603 41 0 40928 0
vsize: 163876
[startup+960.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 41637 0 0 0 95907 109 0 0 25 0 1 0 486296276 168923136 39901 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41241 39901 603 41 0 41200 0
vsize: 164964
[startup+970.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 41913 0 0 0 96906 110 0 0 25 0 1 0 486296276 170004480 40177 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41505 40177 603 41 0 41464 0
vsize: 166020
[startup+980.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 42243 0 0 0 97906 111 0 0 25 0 1 0 486296276 171356160 40507 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41835 40507 603 41 0 41794 0
vsize: 167340
[startup+990.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 42718 0 0 0 98904 112 0 0 25 0 1 0 486296276 173236224 40982 4294967295 134512640 134672761 3221224624 3221223792 134564457 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42294 40982 603 41 0 42253 0
vsize: 169176
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 43132 0 0 0 99903 114 0 0 25 0 1 0 486296276 174989312 41396 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42722 41396 603 41 0 42681 0
vsize: 170888
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 43563 0 0 0 100902 115 0 0 25 0 1 0 486296276 176746496 41827 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43151 41827 603 41 0 43110 0
vsize: 172604
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 43999 0 0 0 101902 116 0 0 25 0 1 0 486296276 178499584 42263 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43579 42263 603 41 0 43538 0
vsize: 174316
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44403 0 0 0 102901 117 0 0 25 0 1 0 486296276 180117504 42667 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43974 42667 603 41 0 43933 0
vsize: 175896
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 103900 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 104900 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223824 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 105900 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 106900 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 107900 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223792 134564467 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 108900 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 109901 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 110901 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 111901 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223792 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 112901 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 113901 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223760 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 114901 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 115901 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 116902 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 117902 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 118902 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7797
Raw data (stat): 7740 (minisat+) R 7739 30701 30700 0 -1 0 44684 0 0 0 119902 117 0 0 25 0 1 0 486296276 180854784 42860 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44154 42860 603 41 0 44113 0
vsize: 176616
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 7797
Raw data (stat): 7740 (minisat+) Z 7739 30701 30700 0 -1 12 44687 0 0 0 119903 126 0 0 25 0 1 0 486296276 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.14
CPU time (s): 1200.3
CPU user time (s): 1199.04
CPU system time (s): 1.26181
CPU usage (%): 100.013
Max. virtual memory (Kb): 176616
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####