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-ran13x13.opb
MD5SUM	688d61d0de54e028c8c4910e094a132c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	893343
Optimality of the best value was proved	NO
Number of terms in the objective function	3549
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	949933178
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	949933178
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	3549
Total number of constraints	195
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	195
Minimum length of a constraint	21
Maximum length of a constraint	260
Trace number 17644

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        838632 kB
Buffers:         14252 kB
Cached:         157708 kB
SwapCached:        556 kB
Active:          30724 kB
Inactive:       143228 kB
HighTotal:      131008 kB
HighFree:        17388 kB
LowTotal:       903652 kB
LowFree:        821244 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5164 kB
Slab:            16448 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:25:33 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 19291 7 1200.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 221 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 219]---> BDD-cost: 1783
c ---[ 217]---> BDD-cost: 1905
c ---[ 215]---> BDD-cost: 1841
c ---[ 213]---> BDD-cost: 1748
c ---[ 211]---> BDD-cost: 1901
c ---[ 209]---> BDD-cost: 1710
c ---[ 207]---> BDD-cost: 1983
c ---[ 205]---> BDD-cost: 1760
c ---[ 203]---> BDD-cost: 1558
c ---[ 201]---> BDD-cost: 1905
c ---[ 199]---> BDD-cost: 1558
c ---[ 197]---> BDD-cost: 1868
c ---[ 195]---> BDD-cost: 1748
c ---[ 193]---> BDD-cost: 1944
c ---[ 191]---> BDD-cost: 2040
c ---[ 189]---> BDD-cost: 1158
c ---[ 187]---> BDD-cost: 1676
c ---[ 185]---> BDD-cost: 1470
c ---[ 183]---> BDD-cost: 1787
c ---[ 181]---> BDD-cost: 1532
c ---[ 179]---> BDD-cost: 1285
c ---[ 177]---> BDD-cost: 2155
c ---[ 175]---> BDD-cost: 1405
c ---[ 173]---> BDD-cost:  919
c ---[ 171]---> BDD-cost: 2096
c ---[ 169]---> BDD-cost: 2088
c ---[ 168]---> BDD-cost:   14
c ---[ 167]---> BDD-cost:   14
c ---[ 166]---> BDD-cost:   10
c ---[ 165]---> BDD-cost:   13
c ---[ 164]---> BDD-cost:   10
c ---[ 163]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 161]---> BDD-cost:   16
c ---[ 160]---> BDD-cost:   16
c ---[ 159]---> BDD-cost:   15
c ---[ 158]---> BDD-cost:   12
c ---[ 157]---> BDD-cost:   11
c ---[ 156]---> BDD-cost:   16
c ---[ 155]---> BDD-cost:   15
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:    9
c ---[ 152]---> BDD-cost:   16
c ---[ 151]---> BDD-cost:   16
c ---[ 150]---> BDD-cost:   10
c ---[ 149]---> BDD-cost:   15
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   13
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   13
c ---[ 143]---> BDD-cost:   12
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:   13
c ---[ 137]---> BDD-cost:   13
c ---[ 136]---> BDD-cost:   10
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   15
c ---[ 132]---> BDD-cost:   13
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   12
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:   13
c ---[ 123]---> BDD-cost:   13
c ---[ 122]---> BDD-cost:   17
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   12
c ---[ 114]---> BDD-cost:   11
c ---[ 113]---> BDD-cost:   13
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   10
c ---[ 106]---> BDD-cost:   15
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   15
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   12
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   15
c ---[  94]---> BDD-cost:   15
c ---[  93]---> BDD-cost:   10
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   17
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   10
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   12
c ---[  76]---> BDD-cost:   12
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   11
c ---[  72]---> BDD-cost:    9
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   15
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   11
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   12
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:   15
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:   15
c ---[  56]---> BDD-cost:   15
c ---[  55]---> BDD-cost:   10
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   15
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   12
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   15
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   15
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   13
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   12
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:    9
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   13
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   17
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   12
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   17
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:    9
c ---[  14]---> BDD-cost:   17
c ---[  13]---> BDD-cost:   17
c ---[  12]---> BDD-cost:   10
c ---[  11]---> BDD-cost:   15
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   5]---> BDD-cost:   12
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   13
c ---[   2]---> BDD-cost:   11
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  131420   381433 |   43806       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 4270402[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:308071     Base: 2 2 2 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        58 |  984576  2372896 |  328192      58     1853    31.9 |  0.000 % |
c |       159 |  984576  2372896 |  361011     159     4482    28.2 |  0.535 % |
c |       309 |  984576  2372896 |  397112     309     5279    17.1 |  0.535 % |
c |       534 |  984576  2372896 |  436823     534     6336    11.9 |  0.535 % |
c |       871 |  984576  2372896 |  480505     871     8360     9.6 |  0.535 % |
c |      1377 |  984576  2372896 |  528556    1377    17955    13.0 |  0.535 % |
c |      2136 |  984576  2372896 |  581412    2136    27186    12.7 |  0.535 % |
c |      3275 |  984576  2372896 |  639553    3275    56112    17.1 |  0.535 % |
c |      4983 |  984576  2372896 |  703508    4983    73948    14.8 |  0.535 % |
c |      7546 |  984576  2372896 |  773859    7546    95876    12.7 |  0.535 % |
c |     11390 |  984545  2372827 |  851245   11389   270891    23.8 |  0.537 % |
c |     17157 |  984545  2372827 |  936370   17156  4384809   255.6 |  0.537 % |
c |     25806 |  984488  2372699 | 1030007   25804  4590764   177.9 |  0.541 % |
c |     38780 |  984488  2372699 | 1133007   38778  5232170   134.9 |  0.541 % |
c |     58243 |  984488  2372699 | 1246308   58241  5551294    95.3 |  0.541 % |
c |     87435 |  984440  2372591 | 1370939   87430  6204035    71.0 |  0.545 % |
c |    131224 |  984315  2372310 | 1508033  131215  7423752    56.6 |  0.555 % |
c ==============================================================================
c [1mFound solution: 3934690[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    163342 |  984409  2374155 |  328136  163315 10525382    64.4 |  0.555 % |
c |    163442 |  984409  2374155 |  360949  163415 10525886    64.4 |  0.710 % |
c |    163592 |  984292  2373886 |  397044  163563 10526893    64.4 |  0.720 % |
c |    163818 |  984198  2373671 |  436749  163788 10536420    64.3 |  0.727 % |
c |    164157 |  983895  2372981 |  480423  164124 10559718    64.3 |  0.752 % |
c |    164666 |  983895  2372981 |  528466  164633 10577149    64.2 |  0.752 % |
c |    165425 |  983895  2372981 |  581312  165392 10625812    64.2 |  0.752 % |
c |    166564 |  983809  2372784 |  639444  166530 10660391    64.0 |  0.760 % |
c |    168273 |  983730  2372605 |  703388  168237 10735407    63.8 |  0.766 % |
c |    170835 |  983550  2372194 |  773727  170797 10803655    63.3 |  0.782 % |
c |    174679 |  983133  2371249 |  851100  174630 10845978    62.1 |  0.816 % |
c |    180445 |  983133  2371249 |  936210  180396 10935303    60.6 |  0.816 % |
c |    189095 |  983133  2371249 | 1029831  189046 11337394    60.0 |  0.816 % |
c ==============================================================================
c [1mFound solution: 3045061[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    189370 |  985594  2377518 |  328531  189321 11367061    60.0 |  0.816 % |
c |    189470 |  985365  2376996 |  361384  189418 11368521    60.0 |  0.832 % |
c |    189620 |  985365  2376996 |  397522  189568 11372697    60.0 |  0.832 % |
c |    189847 |  985365  2376996 |  437274  189795 11385955    60.0 |  0.832 % |
c |    190184 |  983704  2373206 |  481002  190119 11389062    59.9 |  0.971 % |
c |    190692 |  983704  2373206 |  529102  190627 11393809    59.8 |  0.971 % |
c |    191452 |  983704  2373206 |  582012  191387 11401075    59.6 |  0.971 % |
c |    192591 |  983704  2373206 |  640213  192526 11410151    59.3 |  0.971 % |
c |    194299 |  983647  2373073 |  704235  194233 11429183    58.8 |  0.977 % |
c |    196861 |  983647  2373073 |  774658  196795 11459431    58.2 |  0.977 % |
c |    200705 |  983647  2373073 |  852124  200639 11702739    58.3 |  0.977 % |
c |    206472 |  983541  2372829 |  937337  206405 12099853    58.6 |  0.987 % |
c |    215122 |  983541  2372829 | 1031071  215055 12336516    57.4 |  0.987 % |
c |    228097 |  983541  2372829 | 1134178  228030 12587577    55.2 |  0.987 % |
c |    247561 |  983404  2372517 | 1247595  247491 13111395    53.0 |  0.998 % |
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 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 Y#### 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.85 0.95 0.91 2/55 32256
Raw data (stat): 32256 (runsolver) R 32255 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544578296 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.95 0.91 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 29247 0 0 0 933 65 0 0 25 0 1 0 544578296 131538944 27922 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32114 27922 603 41 0 32073 0
vsize: 128456
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.96 0.91 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 29326 0 0 0 1933 65 0 0 25 0 1 0 544578296 131809280 28001 4294967295 134512640 134672761 3221224528 3221223664 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32180 28001 603 41 0 32139 0
vsize: 128720
[startup+30.0074 s]
Raw data (loadavg): 0.91 0.96 0.91 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 29439 0 0 0 2933 66 0 0 25 0 1 0 544578296 132345856 28114 4294967295 134512640 134672761 3221224528 3221223664 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32311 28114 603 41 0 32270 0
vsize: 129244
[startup+40.0078 s]
Raw data (loadavg): 0.92 0.96 0.91 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 29468 0 0 0 3933 66 0 0 25 0 1 0 544578296 132481024 28143 4294967295 134512640 134672761 3221224528 3221223664 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32344 28143 603 41 0 32303 0
vsize: 129376
[startup+50.0086 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 29510 0 0 0 4933 67 0 0 25 0 1 0 544578296 132612096 28185 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32376 28185 603 41 0 32335 0
vsize: 129504
[startup+60.0098 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 29549 0 0 0 5932 67 0 0 25 0 1 0 544578296 132747264 28224 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32409 28224 603 41 0 32368 0
vsize: 129636
[startup+70.0102 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 29589 0 0 0 6932 67 0 0 25 0 1 0 544578296 132878336 28264 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32441 28264 603 41 0 32400 0
vsize: 129764
[startup+80.011 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 29864 0 0 0 7931 68 0 0 25 0 1 0 544578296 133685248 28539 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32638 28539 603 41 0 32597 0
vsize: 130552
[startup+90.0112 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 30144 0 0 0 8931 69 0 0 25 0 1 0 544578296 134778880 28819 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32905 28819 603 41 0 32864 0
vsize: 131620
[startup+100.011 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 30529 0 0 0 9929 71 0 0 25 0 1 0 544578296 136396800 29204 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33300 29204 603 41 0 33259 0
vsize: 133200
[startup+110.015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 30884 0 0 0 10929 71 0 0 25 0 1 0 544578296 137883648 29559 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33663 29559 603 41 0 33622 0
vsize: 134652
[startup+120.016 s]
Raw data (loadavg): 1.06 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 31302 0 0 0 11927 73 0 0 25 0 1 0 544578296 139472896 29977 4294967295 134512640 134672761 3221224528 3221223712 134559280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34051 29977 603 41 0 34010 0
vsize: 136204
[startup+130.017 s]
Raw data (loadavg): 1.05 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 31739 0 0 0 12926 75 0 0 25 0 1 0 544578296 141357056 30414 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34511 30414 603 41 0 34470 0
vsize: 138044
[startup+140.018 s]
Raw data (loadavg): 1.04 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 32196 0 0 0 13924 77 0 0 25 0 1 0 544578296 143241216 30871 4294967295 134512640 134672761 3221224528 3221223632 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34971 30871 603 41 0 34930 0
vsize: 139884
[startup+150.018 s]
Raw data (loadavg): 1.03 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 32661 0 0 0 14923 78 0 0 25 0 1 0 544578296 145121280 31336 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35430 31336 603 41 0 35389 0
vsize: 141720
[startup+160.019 s]
Raw data (loadavg): 1.03 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 33105 0 0 0 15922 79 0 0 25 0 1 0 544578296 146989056 31780 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35886 31780 603 41 0 35845 0
vsize: 143544
[startup+170.019 s]
Raw data (loadavg): 1.02 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 33546 0 0 0 16920 81 0 0 25 0 1 0 544578296 148742144 32221 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36314 32221 603 41 0 36273 0
vsize: 145256
[startup+180.02 s]
Raw data (loadavg): 1.02 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 33818 0 0 0 17919 83 0 0 25 0 1 0 544578296 149925888 32493 4294967295 134512640 134672761 3221224528 3221223652 134566073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36603 32493 603 41 0 36562 0
vsize: 146412
[startup+190.022 s]
Raw data (loadavg): 1.02 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 33899 0 0 0 18919 83 0 0 25 0 1 0 544578296 150196224 32574 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36669 32574 603 41 0 36628 0
vsize: 146676
[startup+200.022 s]
Raw data (loadavg): 1.01 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 34001 0 0 0 19918 84 0 0 25 0 1 0 544578296 150466560 32676 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36735 32676 603 41 0 36694 0
vsize: 146940
[startup+210.023 s]
Raw data (loadavg): 1.01 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 34120 0 0 0 20918 84 0 0 25 0 1 0 544578296 150999040 32795 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36865 32795 603 41 0 36824 0
vsize: 147460
[startup+220.024 s]
Raw data (loadavg): 1.01 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 34181 0 0 0 21918 84 0 0 25 0 1 0 544578296 151269376 32856 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36931 32856 603 41 0 36890 0
vsize: 147724
[startup+230.024 s]
Raw data (loadavg): 1.01 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 34246 0 0 0 22918 84 0 0 25 0 1 0 544578296 151535616 32921 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36996 32921 603 41 0 36955 0
vsize: 147984
[startup+240.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 34427 0 0 0 23918 85 0 0 25 0 1 0 544578296 152338432 33102 4294967295 134512640 134672761 3221224528 3221223652 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37192 33102 603 41 0 37151 0
vsize: 148768
[startup+250.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 34761 0 0 0 24917 86 0 0 25 0 1 0 544578296 153677824 33436 4294967295 134512640 134672761 3221224528 3221223696 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37519 33436 603 41 0 37478 0
vsize: 150076
[startup+260.026 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 32256
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 34833 0 0 0 25917 86 0 0 25 0 1 0 544578296 153944064 33508 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37584 33508 603 41 0 37543 0
vsize: 150336
[startup+270.025 s]
Raw data (loadavg): 1.08 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 34958 0 0 0 26916 87 0 0 25 0 1 0 544578296 154476544 33633 4294967295 134512640 134672761 3221224528 3221223696 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37714 33633 603 41 0 37673 0
vsize: 150856
[startup+280.027 s]
Raw data (loadavg): 1.06 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35131 0 0 0 27916 87 0 0 25 0 1 0 544578296 155144192 33806 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37877 33806 603 41 0 37836 0
vsize: 151508
[startup+290.027 s]
Raw data (loadavg): 1.05 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35296 0 0 0 28915 88 0 0 25 0 1 0 544578296 155815936 33971 4294967295 134512640 134672761 3221224528 3221223672 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38041 33971 603 41 0 38000 0
vsize: 152164
[startup+300.027 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35326 0 0 0 29915 89 0 0 25 0 1 0 544578296 155947008 34001 4294967295 134512640 134672761 3221224528 3221223696 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 34001 603 41 0 38032 0
vsize: 152292
[startup+310.028 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35363 0 0 0 30915 89 0 0 25 0 1 0 544578296 156078080 34038 4294967295 134512640 134672761 3221224528 3221223696 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38105 34038 603 41 0 38064 0
vsize: 152420
[startup+320.028 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35405 0 0 0 31914 90 0 0 25 0 1 0 544578296 156209152 34080 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38137 34080 603 41 0 38096 0
vsize: 152548
[startup+330.029 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35439 0 0 0 32914 90 0 0 25 0 1 0 544578296 156344320 34114 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38170 34114 603 41 0 38129 0
vsize: 152680
[startup+340.029 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35484 0 0 0 33914 90 0 0 25 0 1 0 544578296 156610560 34159 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38235 34159 603 41 0 38194 0
vsize: 152940
[startup+350.029 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35542 0 0 0 34913 91 0 0 25 0 1 0 544578296 157003776 34217 4294967295 134512640 134672761 3221224528 3221223680 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38331 34217 603 41 0 38290 0
vsize: 153324
[startup+360.031 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35603 0 0 0 35913 92 0 0 25 0 1 0 544578296 157274112 34278 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38397 34278 603 41 0 38356 0
vsize: 153588
[startup+370.033 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35659 0 0 0 36913 92 0 0 25 0 1 0 544578296 157540352 34334 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38462 34334 603 41 0 38421 0
vsize: 153848
[startup+380.033 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35721 0 0 0 37913 92 0 0 25 0 1 0 544578296 157806592 34396 4294967295 134512640 134672761 3221224528 3221223696 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38527 34396 603 41 0 38486 0
vsize: 154108
[startup+390.034 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35781 0 0 0 38913 92 0 0 25 0 1 0 544578296 158072832 34456 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38592 34456 603 41 0 38551 0
vsize: 154368
[startup+400.034 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35821 0 0 0 39913 92 0 0 25 0 1 0 544578296 158203904 34496 4294967295 134512640 134672761 3221224528 3221223664 134560622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38624 34496 603 41 0 38583 0
vsize: 154496
[startup+410.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 35948 0 0 0 40913 92 0 0 25 0 1 0 544578296 158744576 34623 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38756 34623 603 41 0 38715 0
vsize: 155024
[startup+420.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 36066 0 0 0 41913 92 0 0 25 0 1 0 544578296 159145984 34741 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38854 34741 603 41 0 38813 0
vsize: 155416
[startup+430.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 36182 0 0 0 42914 93 0 0 25 0 1 0 544578296 159682560 34857 4294967295 134512640 134672761 3221224528 3221223696 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38985 34857 603 41 0 38944 0
vsize: 155940
[startup+440.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 36294 0 0 0 43912 94 0 0 25 0 1 0 544578296 160083968 34969 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39083 34969 603 41 0 39042 0
vsize: 156332
[startup+450.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 36386 0 0 0 44912 94 0 0 25 0 1 0 544578296 160485376 35061 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39181 35061 603 41 0 39140 0
vsize: 156724
[startup+460.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 36476 0 0 0 45912 95 0 0 25 0 1 0 544578296 160751616 35151 4294967295 134512640 134672761 3221224528 3221223696 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39246 35151 603 41 0 39205 0
vsize: 156984
[startup+470.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 36567 0 0 0 46911 95 0 0 25 0 1 0 544578296 161157120 35242 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39345 35242 603 41 0 39304 0
vsize: 157380
[startup+480.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 36676 0 0 0 47911 96 0 0 25 0 1 0 544578296 161558528 35351 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39443 35351 603 41 0 39402 0
vsize: 157772
[startup+490.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 36814 0 0 0 48911 96 0 0 25 0 1 0 544578296 162091008 35489 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39573 35489 603 41 0 39532 0
vsize: 158292
[startup+500.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 36850 0 0 0 49911 96 0 0 25 0 1 0 544578296 162222080 35525 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39605 35525 603 41 0 39564 0
vsize: 158420
[startup+510.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 36964 0 0 0 50910 97 0 0 25 0 1 0 544578296 162762752 35639 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39737 35639 603 41 0 39696 0
vsize: 158948
[startup+520.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 37269 0 0 0 51909 98 0 0 25 0 1 0 544578296 163962880 35944 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40030 35944 603 41 0 39989 0
vsize: 160120
[startup+530.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 37483 0 0 0 52909 99 0 0 25 0 1 0 544578296 164888576 36158 4294967295 134512640 134672761 3221224528 3221223716 134557974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40256 36158 603 41 0 40215 0
vsize: 161024
[startup+540.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 37524 0 0 0 53909 99 0 0 25 0 1 0 544578296 165023744 36199 4294967295 134512640 134672761 3221224528 3221223672 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40289 36199 603 41 0 40248 0
vsize: 161156
[startup+550.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 37608 0 0 0 54908 99 0 0 25 0 1 0 544578296 165289984 36283 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40354 36283 603 41 0 40313 0
vsize: 161416
[startup+560.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32258
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 37685 0 0 0 55908 100 0 0 25 0 1 0 544578296 165691392 36360 4294967295 134512640 134672761 3221224528 3221223728 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40452 36360 603 41 0 40411 0
vsize: 161808
[startup+570.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 37733 0 0 0 56908 100 0 0 25 0 1 0 544578296 165826560 36408 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40485 36408 603 41 0 40444 0
vsize: 161940
[startup+580.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 37759 0 0 0 57908 100 0 0 25 0 1 0 544578296 165961728 36434 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40518 36434 603 41 0 40477 0
vsize: 162072
[startup+590.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 37849 0 0 0 58908 100 0 0 25 0 1 0 544578296 166756352 36524 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40712 36524 603 41 0 40671 0
vsize: 162848
[startup+600.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 38015 0 0 0 59907 101 0 0 25 0 1 0 544578296 167424000 36690 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40875 36690 603 41 0 40834 0
vsize: 163500
[startup+610.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 38136 0 0 0 60907 102 0 0 25 0 1 0 544578296 167956480 36811 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41005 36811 603 41 0 40964 0
vsize: 164020
[startup+620.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 38296 0 0 0 61907 102 0 0 25 0 1 0 544578296 168628224 36971 4294967295 134512640 134672761 3221224528 3221223700 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41169 36971 603 41 0 41128 0
vsize: 164676
[startup+630.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 38324 0 0 0 62907 102 0 0 25 0 1 0 544578296 168763392 36999 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41202 36999 603 41 0 41161 0
vsize: 164808
[startup+640.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 38363 0 0 0 63906 103 0 0 25 0 1 0 544578296 168898560 37038 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41235 37038 603 41 0 41194 0
vsize: 164940
[startup+650.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 38606 0 0 0 64906 104 0 0 25 0 1 0 544578296 169840640 37281 4294967295 134512640 134672761 3221224528 3221223664 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41465 37281 603 41 0 41424 0
vsize: 165860
[startup+660.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 38782 0 0 0 65905 104 0 0 25 0 1 0 544578296 170508288 37457 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41628 37457 603 41 0 41587 0
vsize: 166512
[startup+670.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 39136 0 0 0 66904 105 0 0 25 0 1 0 544578296 171995136 37811 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41991 37811 603 41 0 41950 0
vsize: 167964
[startup+680.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 39533 0 0 0 67904 106 0 0 25 0 1 0 544578296 173617152 38208 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42387 38208 603 41 0 42346 0
vsize: 169548
[startup+690.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 39905 0 0 0 68903 107 0 0 25 0 1 0 544578296 175095808 38580 4294967295 134512640 134672761 3221224528 3221223632 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42748 38580 603 41 0 42707 0
vsize: 170992
[startup+700.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 40282 0 0 0 69902 108 0 0 25 0 1 0 544578296 176713728 38957 4294967295 134512640 134672761 3221224528 3221223632 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43143 38957 603 41 0 43102 0
vsize: 172572
[startup+710.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 40640 0 0 0 70901 109 0 0 25 0 1 0 544578296 178061312 39315 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43472 39315 603 41 0 43431 0
vsize: 173888
[startup+720.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 40967 0 0 0 71901 110 0 0 25 0 1 0 544578296 179396608 39642 4294967295 134512640 134672761 3221224528 3221223632 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43798 39642 603 41 0 43757 0
vsize: 175192
[startup+730.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 41097 0 0 0 72900 110 0 0 25 0 1 0 544578296 179933184 39772 4294967295 134512640 134672761 3221224528 3221223652 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43929 39772 603 41 0 43888 0
vsize: 175716
[startup+740.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 41551 0 0 0 73899 112 0 0 25 0 1 0 544578296 181608448 40161 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44338 40161 603 41 0 44297 0
vsize: 177352
[startup+750.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 41585 0 0 0 74899 112 0 0 25 0 1 0 544578296 181743616 40195 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44371 40195 603 41 0 44330 0
vsize: 177484
[startup+760.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 41622 0 0 0 75899 112 0 0 25 0 1 0 544578296 181878784 40232 4294967295 134512640 134672761 3221224528 3221223664 134560645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44404 40232 603 41 0 44363 0
vsize: 177616
[startup+770.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 41665 0 0 0 76899 112 0 0 25 0 1 0 544578296 182140928 40275 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44468 40275 603 41 0 44427 0
vsize: 177872
[startup+780.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 41724 0 0 0 77898 113 0 0 25 0 1 0 544578296 182276096 40334 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44501 40334 603 41 0 44460 0
vsize: 178004
[startup+790.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 41797 0 0 0 78897 114 0 0 25 0 1 0 544578296 182681600 40407 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44600 40407 603 41 0 44559 0
vsize: 178400
[startup+800.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 41869 0 0 0 79897 114 0 0 25 0 1 0 544578296 182943744 40479 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44664 40479 603 41 0 44623 0
vsize: 178656
[startup+810.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 41900 0 0 0 80897 115 0 0 25 0 1 0 544578296 183074816 40510 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44696 40510 603 41 0 44655 0
vsize: 178784
[startup+820.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 41925 0 0 0 81896 115 0 0 25 0 1 0 544578296 183074816 40535 4294967295 134512640 134672761 3221224528 3221223700 134556658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44696 40535 603 41 0 44655 0
vsize: 178784
[startup+830.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 41979 0 0 0 82896 116 0 0 25 0 1 0 544578296 183341056 40589 4294967295 134512640 134672761 3221224528 3221223696 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44761 40589 603 41 0 44720 0
vsize: 179044
[startup+840.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42033 0 0 0 83896 116 0 0 25 0 1 0 544578296 183607296 40643 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44826 40643 603 41 0 44785 0
vsize: 179304
[startup+850.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42119 0 0 0 84895 117 0 0 25 0 1 0 544578296 183873536 40729 4294967295 134512640 134672761 3221224528 3221223632 134560495 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44891 40729 603 41 0 44850 0
vsize: 179564
[startup+860.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32260
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42206 0 0 0 85895 117 0 0 25 0 1 0 544578296 184274944 40816 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44989 40816 603 41 0 44948 0
vsize: 179956
[startup+870.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42312 0 0 0 86894 118 0 0 25 0 1 0 544578296 184680448 40922 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45088 40922 603 41 0 45047 0
vsize: 180352
[startup+880.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42341 0 0 0 87894 118 0 0 25 0 1 0 544578296 184815616 40951 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45121 40951 603 41 0 45080 0
vsize: 180484
[startup+890.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42380 0 0 0 88894 119 0 0 25 0 1 0 544578296 184946688 40990 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45153 40990 603 41 0 45112 0
vsize: 180612
[startup+900.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42489 0 0 0 89893 119 0 0 25 0 1 0 544578296 185352192 41099 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45252 41099 603 41 0 45211 0
vsize: 181008
[startup+910.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42739 0 0 0 90893 119 0 0 25 0 1 0 544578296 186040320 41282 4294967295 134512640 134672761 3221224528 3221223700 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45420 41282 603 41 0 45379 0
vsize: 181680
[startup+920.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42761 0 0 0 91893 120 0 0 25 0 1 0 544578296 186175488 41304 4294967295 134512640 134672761 3221224528 3221223700 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45453 41304 603 41 0 45412 0
vsize: 181812
[startup+930.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42761 0 0 0 92893 120 0 0 25 0 1 0 544578296 186175488 41304 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45453 41304 603 41 0 45412 0
vsize: 181812
[startup+940.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42815 0 0 0 93892 121 0 0 25 0 1 0 544578296 186310656 41358 4294967295 134512640 134672761 3221224528 3221223664 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45486 41358 603 41 0 45445 0
vsize: 181944
[startup+950.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42881 0 0 0 94892 121 0 0 25 0 1 0 544578296 186580992 41424 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45552 41424 603 41 0 45511 0
vsize: 182208
[startup+960.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42937 0 0 0 95892 121 0 0 25 0 1 0 544578296 186847232 41480 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45617 41480 603 41 0 45576 0
vsize: 182468
[startup+970.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 42981 0 0 0 96892 122 0 0 25 0 1 0 544578296 186978304 41524 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45649 41524 603 41 0 45608 0
vsize: 182596
[startup+980.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 43060 0 0 0 97892 122 0 0 25 0 1 0 544578296 187379712 41603 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45747 41603 603 41 0 45706 0
vsize: 182988
[startup+990.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 43127 0 0 0 98891 123 0 0 25 0 1 0 544578296 187650048 41670 4294967295 134512640 134672761 3221224528 3221223664 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45813 41670 603 41 0 45772 0
vsize: 183252
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 43206 0 0 0 99891 123 0 0 25 0 1 0 544578296 187920384 41749 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45879 41749 603 41 0 45838 0
vsize: 183516
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 43294 0 0 0 100891 123 0 0 25 0 1 0 544578296 188325888 41837 4294967295 134512640 134672761 3221224528 3221223680 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45978 41837 603 41 0 45937 0
vsize: 183912
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 43400 0 0 0 101891 123 0 0 25 0 1 0 544578296 188731392 41943 4294967295 134512640 134672761 3221224528 3221223632 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46077 41943 603 41 0 46036 0
vsize: 184308
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 43545 0 0 0 102890 124 0 0 25 0 1 0 544578296 189272064 42088 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46209 42088 603 41 0 46168 0
vsize: 184836
[startup+1040.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 43694 0 0 0 103890 124 0 0 25 0 1 0 544578296 189939712 42237 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46372 42237 603 41 0 46331 0
vsize: 185488
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 43904 0 0 0 104890 125 0 0 25 0 1 0 544578296 190746624 42447 4294967295 134512640 134672761 3221224528 3221223664 134560560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46569 42447 603 41 0 46528 0
vsize: 186276
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 43971 0 0 0 105890 125 0 0 25 0 1 0 544578296 191012864 42514 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46634 42514 603 41 0 46593 0
vsize: 186536
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44089 0 0 0 106889 126 0 0 25 0 1 0 544578296 191414272 42632 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46732 42632 603 41 0 46691 0
vsize: 186928
[startup+1080.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44134 0 0 0 107889 126 0 0 25 0 1 0 544578296 191676416 42677 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46796 42677 603 41 0 46755 0
vsize: 187184
[startup+1090.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44185 0 0 0 108889 126 0 0 25 0 1 0 544578296 191807488 42728 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46828 42728 603 41 0 46787 0
vsize: 187312
[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44260 0 0 0 109889 127 0 0 25 0 1 0 544578296 192077824 42803 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46894 42803 603 41 0 46853 0
vsize: 187576
[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44331 0 0 0 110888 127 0 0 25 0 1 0 544578296 192479232 42874 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46992 42874 603 41 0 46951 0
vsize: 187968
[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44393 0 0 0 111888 128 0 0 25 0 1 0 544578296 192614400 42936 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47025 42936 603 41 0 46984 0
vsize: 188100
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44552 0 0 0 112888 129 0 0 25 0 1 0 544578296 193286144 43095 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47189 43095 603 41 0 47148 0
vsize: 188756
[startup+1140.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44653 0 0 0 113887 129 0 0 25 0 1 0 544578296 193687552 43196 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47287 43196 603 41 0 47246 0
vsize: 189148
[startup+1150.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44722 0 0 0 114887 129 0 0 25 0 1 0 544578296 193957888 43265 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47353 43265 603 41 0 47312 0
vsize: 189412
[startup+1160.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32262
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44906 0 0 0 115887 130 0 0 25 0 1 0 544578296 194764800 43449 4294967295 134512640 134672761 3221224528 3221223632 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47550 43449 603 41 0 47509 0
vsize: 190200
[startup+1170.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32264
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44941 0 0 0 116887 130 0 0 25 0 1 0 544578296 194899968 43484 4294967295 134512640 134672761 3221224528 3221223700 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47583 43484 603 41 0 47542 0
vsize: 190332
[startup+1180.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32264
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44941 0 0 0 117887 130 0 0 25 0 1 0 544578296 194899968 43484 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47583 43484 603 41 0 47542 0
vsize: 190332
[startup+1190.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32264
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 44957 0 0 0 118887 130 0 0 25 0 1 0 544578296 194899968 43500 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47583 43500 603 41 0 47542 0
vsize: 190332
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 32264
Raw data (stat): 32256 (minisat+) R 32255 22929 22928 0 -1 0 45110 0 0 0 119886 130 0 0 25 0 1 0 544578296 195571712 43653 4294967295 134512640 134672761 3221224528 3221223672 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47747 43653 603 41 0 47706 0
vsize: 190988
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 1.00 0.93 1/55 32264
Raw data (stat): 32256 (minisat+) Z 32255 22929 22928 0 -1 12 45113 0 0 0 119887 139 0 0 25 0 1 0 544578296 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.15
CPU time (s): 1200.27
CPU user time (s): 1198.88
CPU system time (s): 1.39379
CPU usage (%): 100.01
Max. virtual memory (Kb): 190988
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####