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 14796

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 01:22:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19292 boxname=wulflinc10 idbench=1484 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  688d61d0de54e028c8c4910e094a132c  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-ran13x13.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-ran13x13.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-ran13x13.opb
IDLAUNCH: 19292
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        905980 kB
Buffers:         26880 kB
Cached:          79404 kB
SwapCached:          0 kB
Active:          18084 kB
Inactive:        90680 kB
HighTotal:      131008 kB
HighFree:        77364 kB
LowTotal:       903652 kB
LowFree:        828616 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            14068 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:42:18 (client local time) WITH STATUS 10 IN 1200.13 SECONDS
stats: 19292 7 1200.13 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]---> Adder-cost: 250   maxlim: 16883   bits: 15/15
c ---[ 217]---> Adder-cost: 258   maxlim: 26227   bits: 15/15
c ---[ 215]---> Adder-cost: 258   maxlim: 26867   bits: 15/15
c ---[ 213]---> Adder-cost: 250   maxlim: 17139   bits: 15/15
c ---[ 211]---> Adder-cost: 258   maxlim: 26355   bits: 15/15
c ---[ 209]---> Adder-cost: 250   maxlim: 17267   bits: 15/15
c ---[ 207]---> Adder-cost: 258   maxlim: 25331   bits: 15/15
c ---[ 205]---> Adder-cost: 250   maxlim: 17011   bits: 15/15
c ---[ 203]---> Adder-cost: 234   maxlim: 10611   bits: 14/14
c ---[ 201]---> Adder-cost: 258   maxlim: 26227   bits: 15/15
c ---[ 199]---> Adder-cost: 234   maxlim: 10611   bits: 14/14
c ---[ 197]---> Adder-cost: 258   maxlim: 26611   bits: 15/15
c ---[ 195]---> Adder-cost: 250   maxlim: 17139   bits: 15/15
c ---[ 193]---> Adder-cost: 272   maxlim: 34291   bits: 16/16
c ---[ 191]---> Adder-cost: 272   maxlim: 33267   bits: 16/16
c ---[ 189]---> Adder-cost: 216   maxlim: 6387   bits: 13/13
c ---[ 187]---> Adder-cost: 258   maxlim: 23411   bits: 15/15
c ---[ 185]---> Adder-cost: 240   maxlim: 12659   bits: 14/14
c ---[ 183]---> Adder-cost: 258   maxlim: 22899   bits: 15/15
c ---[ 181]---> Adder-cost: 240   maxlim: 12531   bits: 14/14
c ---[ 179]---> Adder-cost: 216   maxlim: 6259   bits: 13/13
c ---[ 177]---> Adder-cost: 272   maxlim: 31347   bits: 16/15
c ---[ 175]---> Adder-cost: 240   maxlim: 12787   bits: 14/14
c ---[ 173]---> Sorter-cost: 2075     Base: 2 2 2 2 2 2 2
c ---[ 171]---> Adder-cost: 272   maxlim: 32499   bits: 16/15
c ---[ 169]---> Adder-cost: 272   maxlim: 32755   bits: 16/15
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 |   50977   171174 |   16992       0        0     nan |  0.000 % |
c |       101 |   50910   170945 |   18691      95      436     4.6 | 20.390 % |
c |       251 |   50855   170766 |   20560     238      944     4.0 | 20.468 % |
c |       476 |   50772   170489 |   22616     454     1874     4.1 | 20.578 % |
c |       813 |   50674   170161 |   24877     780     3223     4.1 | 20.718 % |
c |      1319 |   50586   169871 |   27365    1276     4892     3.8 | 20.835 % |
c |      2078 |   50472   169489 |   30102    2021     8037     4.0 | 20.984 % |
c |      3218 |   50423   169322 |   33112    3155    15932     5.0 | 21.046 % |
c |      4926 |   50144   168663 |   36423    4846    40095     8.3 | 21.686 % |
c |      7488 |   49519   167105 |   40066    7385    55117     7.5 | 23.162 % |
c |     11332 |   49127   165859 |   44072   11153    77539     7.0 | 23.731 % |
c |     17098 |   48800   164742 |   48480   16861   117457     7.0 | 24.169 % |
c |     25747 |   48522   163841 |   53328   25470   215730     8.5 | 24.575 % |
c |     38722 |   48463   163642 |   58660   38437   603947    15.7 | 24.660 % |
c ==============================================================================
c [1mFound solution: 3708422[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 6663   maxlim: 1984372   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43292 |   94878   329541 |   31626   42977   667026    15.5 | 24.660 % |
c |     43392 |   94878   329541 |   34788   17878   310143    17.3 | 16.458 % |
c |     43545 |   94878   329541 |   38267   18031   311130    17.3 | 16.458 % |
c |     43770 |   94878   329541 |   42094   18256   312348    17.1 | 16.458 % |
c |     44107 |   94746   329237 |   46303   18586   314270    16.9 | 16.663 % |
c |     44613 |   94746   329237 |   50933   19092   317466    16.6 | 16.663 % |
c |     45373 |   94746   329237 |   56027   19852   323697    16.3 | 16.663 % |
c |     46512 |   94737   329208 |   61630   20990   330630    15.8 | 16.674 % |
c |     48221 |   94561   328800 |   67793   22687   341410    15.0 | 16.956 % |
c |     50783 |   94507   328649 |   74572   25243   360422    14.3 | 17.028 % |
c |     54628 |   94498   328620 |   82029   29087   406181    14.0 | 17.038 % |
c |     60394 |   94473   328539 |   90232   34849   473921    13.6 | 17.064 % |
c |     69044 |   94368   328221 |   99255   43487   760766    17.5 | 17.192 % |
c ==============================================================================
c [1mFound solution: 2642087[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 3050707   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74359 |   94383   328355 |   31461   48799   848095    17.4 | 17.192 % |
c |     74459 |   94383   328355 |   34607   20929   376016    18.0 | 17.240 % |
c |     74609 |   94383   328355 |   38067   21079   376895    17.9 | 17.240 % |
c |     74836 |   94383   328355 |   41874   21306   378350    17.8 | 17.240 % |
c |     75173 |   94383   328355 |   46062   21643   380515    17.6 | 17.240 % |
c |     75679 |   94383   328355 |   50668   22149   383728    17.3 | 17.240 % |
c |     76438 |   94383   328355 |   55735   22908   389888    17.0 | 17.240 % |
c |     77577 |   94383   328355 |   61308   24047   400096    16.6 | 17.240 % |
c |     79285 |   94368   328304 |   67439   25750   415533    16.1 | 17.250 % |
c |     81847 |   94359   328273 |   74183   28310   444940    15.7 | 17.256 % |
c |     85693 |   94337   328222 |   81601   32155   860387    26.8 | 17.291 % |
c |     91459 |   94325   328187 |   89761   37919  1244531    32.8 | 17.302 % |
c ==============================================================================
c [1mFound solution: 2639956[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3052838   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     93054 |   94323   328286 |   31441   39512  1282134    32.4 | 17.302 % |
c |     93154 |   94323   328286 |   34585   19653   865741    44.1 | 17.336 % |
c |     93306 |   94186   327964 |   38043   19784   866504    43.8 | 17.536 % |
c |     93531 |   94186   327964 |   41847   20009   868242    43.4 | 17.536 % |
c |     93868 |   94186   327964 |   46032   20346   870872    42.8 | 17.536 % |
c |     94374 |   94186   327964 |   50636   20852   873548    41.9 | 17.536 % |
c |     95133 |   94186   327964 |   55699   21611   877811    40.6 | 17.536 % |
c |     96272 |   94186   327964 |   61269   22750   885288    38.9 | 17.536 % |
c |     97980 |   94186   327964 |   67396   24458   922726    37.7 | 17.536 % |
c |    100544 |   94180   327944 |   74136   27020   998359    36.9 | 17.542 % |
c |    104390 |   94180   327944 |   81549   30866  1143146    37.0 | 17.542 % |
c |    110157 |   94174   327924 |   89704   36631  1573459    43.0 | 17.547 % |
c |    118806 |   94110   327778 |   98675   45276  2243345    49.5 | 17.654 % |
c |    131780 |   94087   327703 |  108542   58246  3852381    66.1 | 17.675 % |
c |    151245 |   94062   327632 |  119397   77708  4691861    60.4 | 17.706 % |
c |    180438 |   93965   327379 |  131336  106891  6563728    61.4 | 17.864 % |
c |    224228 |   93850   327106 |  144470   24581  1200282    48.8 | 18.034 % |
c |    289913 |   93632   326577 |  158917   90246  5433928    60.2 | 18.418 % |
c |    388441 |   93615   326528 |  174809   38924  1164355    29.9 | 18.439 % |
c |    536232 |   93590   326459 |  192290  186711 11250882    60.3 | 18.469 % |
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 Y5#### 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.80 0.92 0.91 2/54 21824
Raw data (stat): 21824 (runsolver) R 21823 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482870107 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.0011 s]
Raw data (loadavg): 0.83 0.93 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 1591 0 1 0 988 4 0 0 25 0 1 0 482870107 8167424 1553 4294967295 134512640 134672761 3221224544 3221223696 134565070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1994 1553 603 41 0 1953 0
vsize: 7976
[startup+20.0017 s]
Raw data (loadavg): 0.86 0.93 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 1704 0 1 0 1987 5 0 0 25 0 1 0 482870107 8572928 1666 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2093 1666 603 41 0 2052 0
vsize: 8372
[startup+30.0018 s]
Raw data (loadavg): 0.88 0.93 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 1902 0 1 0 2987 6 0 0 25 0 1 0 482870107 9441280 1864 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2305 1864 603 41 0 2264 0
vsize: 9220
[startup+40.0018 s]
Raw data (loadavg): 0.90 0.93 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 2563 0 1 0 3985 8 0 0 25 0 1 0 482870107 12128256 2525 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2961 2525 603 41 0 2920 0
vsize: 11844
[startup+50.0033 s]
Raw data (loadavg): 0.91 0.93 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 6454 0 1 0 4976 18 0 0 25 0 1 0 482870107 26128384 5750 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6379 5750 603 41 0 6338 0
vsize: 25516
[startup+60.0035 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 6454 0 1 0 5976 18 0 0 25 0 1 0 482870107 26128384 5750 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6379 5750 603 41 0 6338 0
vsize: 25516
[startup+70.0035 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 6455 0 1 0 6975 18 0 0 25 0 1 0 482870107 26128384 5751 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6379 5751 603 41 0 6338 0
vsize: 25516
[startup+80.0041 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 6591 0 1 0 7975 18 0 0 25 0 1 0 482870107 26804224 5887 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6544 5887 603 41 0 6503 0
vsize: 26176
[startup+90.0042 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 7054 0 1 0 8973 20 0 0 25 0 1 0 482870107 28246016 6289 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6896 6289 603 41 0 6855 0
vsize: 27584
[startup+100.005 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 7054 0 1 0 9973 21 0 0 25 0 1 0 482870107 28246016 6289 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6896 6289 603 41 0 6855 0
vsize: 27584
[startup+110.006 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 7081 0 1 0 10972 21 0 0 25 0 1 0 482870107 28377088 6316 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6928 6316 603 41 0 6887 0
vsize: 27712
[startup+120.006 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 7630 0 1 0 11971 23 0 0 25 0 1 0 482870107 30334976 6803 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7406 6803 603 41 0 7365 0
vsize: 29624
[startup+130.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 7630 0 1 0 12971 23 0 0 25 0 1 0 482870107 30334976 6803 4294967295 134512640 134672761 3221224544 3221223712 134561269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7406 6803 603 41 0 7365 0
vsize: 29624
[startup+140.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 7630 0 1 0 13971 23 0 0 25 0 1 0 482870107 30334976 6803 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7406 6803 603 41 0 7365 0
vsize: 29624
[startup+150.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 8379 0 1 0 14968 26 0 0 25 0 1 0 482870107 33431552 7552 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8162 7552 603 41 0 8121 0
vsize: 32648
[startup+160.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 8939 0 1 0 15967 28 0 0 25 0 1 0 482870107 35725312 8112 4294967295 134512640 134672761 3221224544 3221223648 134555093 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8722 8112 603 41 0 8681 0
vsize: 34888
[startup+170.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 9940 0 1 0 16964 30 0 0 25 0 1 0 482870107 39903232 9113 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9742 9113 603 41 0 9701 0
vsize: 38968
[startup+180.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 10413 0 1 0 17962 33 0 0 25 0 1 0 482870107 41783296 9586 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10201 9586 603 41 0 10160 0
vsize: 40804
[startup+190.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 10784 0 1 0 18961 34 0 0 25 0 1 0 482870107 43520000 9957 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10625 9957 603 41 0 10584 0
vsize: 42500
[startup+200.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 11323 0 1 0 19958 37 0 0 25 0 1 0 482870107 45674496 10496 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11151 10496 603 41 0 11110 0
vsize: 44604
[startup+210.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 11810 0 1 0 20956 39 0 0 25 0 1 0 482870107 47689728 10983 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11643 10983 603 41 0 11602 0
vsize: 46572
[startup+220.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 12216 0 1 0 21955 40 0 0 25 0 1 0 482870107 49336320 11389 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12045 11389 603 41 0 12004 0
vsize: 48180
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 12777 0 1 0 22953 42 0 0 25 0 1 0 482870107 51638272 11950 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12607 11950 603 41 0 12566 0
vsize: 50428
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 13324 0 1 0 23951 45 0 0 25 0 1 0 482870107 53792768 12497 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13133 12497 603 41 0 13092 0
vsize: 52532
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 13537 0 1 0 24950 46 0 0 25 0 1 0 482870107 54743040 12710 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13365 12710 603 41 0 13324 0
vsize: 53460
[startup+260.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 13837 0 1 0 25948 47 0 0 25 0 1 0 482870107 55824384 13010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13629 13010 603 41 0 13588 0
vsize: 54516
[startup+270.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 14186 0 1 0 26947 48 0 0 25 0 1 0 482870107 57331712 13359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13997 13359 603 41 0 13956 0
vsize: 55988
[startup+280.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 14511 0 1 0 27946 49 0 0 25 0 1 0 482870107 58699776 13684 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14331 13684 603 41 0 14290 0
vsize: 57324
[startup+290.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 14819 0 1 0 28946 50 0 0 25 0 1 0 482870107 59949056 13992 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14636 13992 603 41 0 14595 0
vsize: 58544
[startup+300.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 15106 0 1 0 29944 52 0 0 25 0 1 0 482870107 61603840 14279 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15040 14279 603 41 0 14999 0
vsize: 60160
[startup+310.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 15404 0 1 0 30944 53 0 0 25 0 1 0 482870107 62816256 14577 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15336 14577 603 41 0 15295 0
vsize: 61344
[startup+320.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 15684 0 1 0 31942 54 0 0 25 0 1 0 482870107 64032768 14857 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15633 14857 603 41 0 15592 0
vsize: 62532
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 15926 0 1 0 32941 56 0 0 25 0 1 0 482870107 64983040 15099 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15865 15099 603 41 0 15824 0
vsize: 63460
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16185 0 1 0 33940 57 0 0 25 0 1 0 482870107 66060288 15358 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16128 15358 603 41 0 16087 0
vsize: 64512
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16430 0 1 0 34938 58 0 0 25 0 1 0 482870107 67096576 15603 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16381 15603 603 41 0 16340 0
vsize: 65524
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 35937 60 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 36937 60 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 37937 60 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 38936 61 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 39936 61 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 40936 62 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 41935 62 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 42935 62 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 43935 63 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 44935 63 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 45935 63 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 46934 64 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 47934 64 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+490.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 48934 64 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 49934 65 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16596 0 1 0 50934 65 0 0 25 0 1 0 482870107 67768320 15769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 15769 603 41 0 16504 0
vsize: 66180
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 16794 0 1 0 51933 66 0 0 25 0 1 0 482870107 68567040 15967 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16740 15967 603 41 0 16699 0
vsize: 66960
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 17409 0 1 0 52931 68 0 0 25 0 1 0 482870107 71131136 16582 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17366 16582 603 41 0 17325 0
vsize: 69464
[startup+540.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 17804 0 1 0 53930 69 0 0 25 0 1 0 482870107 72740864 16977 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17759 16977 603 41 0 17718 0
vsize: 71036
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 18179 0 1 0 54929 70 0 0 25 0 1 0 482870107 74227712 17352 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18122 17352 603 41 0 18081 0
vsize: 72488
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 18533 0 1 0 55928 72 0 0 25 0 1 0 482870107 75710464 17706 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17706 603 41 0 18443 0
vsize: 73936
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 18835 0 1 0 56927 73 0 0 25 0 1 0 482870107 76914688 18008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18778 18008 603 41 0 18737 0
vsize: 75112
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 57926 74 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 58925 75 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+600.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 59925 75 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+610.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 60925 75 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 61925 75 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 62925 76 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+640.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 63925 76 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+650.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 64925 76 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+660.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 65924 76 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223728 134559588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 66924 77 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 67924 77 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+690.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 68924 77 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 69924 77 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+710.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 70924 78 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+720.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 71923 78 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223692 134566158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 72923 78 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+740.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19140 0 1 0 73923 79 0 0 25 0 1 0 482870107 78131200 18313 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18313 603 41 0 19034 0
vsize: 76300
[startup+750.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19147 0 1 0 74923 79 0 0 25 0 1 0 482870107 78131200 18320 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18320 603 41 0 19034 0
vsize: 76300
[startup+760.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19571 0 1 0 75922 80 0 0 25 0 1 0 482870107 79876096 18744 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19501 18744 603 41 0 19460 0
vsize: 78004
[startup+770.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 19907 0 1 0 76921 82 0 0 25 0 1 0 482870107 81223680 19080 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19830 19080 603 41 0 19789 0
vsize: 79320
[startup+780.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 20572 0 1 0 77918 84 0 0 25 0 1 0 482870107 83910656 19745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20486 19745 603 41 0 20445 0
vsize: 81944
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 21331 0 1 0 78916 86 0 0 25 0 1 0 482870107 86994944 20504 4294967295 134512640 134672761 3221224544 3221223648 134559805 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21239 20504 603 41 0 21198 0
vsize: 84956
[startup+800.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 21870 0 1 0 79915 88 0 0 25 0 1 0 482870107 89149440 21043 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21765 21043 603 41 0 21724 0
vsize: 87060
[startup+810.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22423 0 1 0 80913 89 0 0 25 0 1 0 482870107 91435008 21596 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21596 603 41 0 22282 0
vsize: 89292
[startup+820.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22432 0 1 0 81913 90 0 0 25 0 1 0 482870107 91435008 21605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21605 603 41 0 22282 0
vsize: 89292
[startup+830.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22432 0 1 0 82913 90 0 0 25 0 1 0 482870107 91435008 21605 4294967295 134512640 134672761 3221224544 3221223788 134561422 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21605 603 41 0 22282 0
vsize: 89292
[startup+840.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22432 0 1 0 83913 90 0 0 25 0 1 0 482870107 91435008 21605 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21605 603 41 0 22282 0
vsize: 89292
[startup+850.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22432 0 1 0 84913 90 0 0 25 0 1 0 482870107 91435008 21605 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21605 603 41 0 22282 0
vsize: 89292
[startup+860.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22432 0 1 0 85913 91 0 0 25 0 1 0 482870107 91435008 21605 4294967295 134512640 134672761 3221224544 3221223680 134565132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21605 603 41 0 22282 0
vsize: 89292
[startup+870.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22432 0 1 0 86912 91 0 0 25 0 1 0 482870107 91435008 21605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21605 603 41 0 22282 0
vsize: 89292
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22432 0 1 0 87912 91 0 0 25 0 1 0 482870107 91435008 21605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21605 603 41 0 22282 0
vsize: 89292
[startup+890.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22432 0 1 0 88912 91 0 0 25 0 1 0 482870107 91435008 21605 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21605 603 41 0 22282 0
vsize: 89292
[startup+900.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22432 0 1 0 89912 91 0 0 25 0 1 0 482870107 91435008 21605 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21605 603 41 0 22282 0
vsize: 89292
[startup+910.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22432 0 1 0 90912 92 0 0 25 0 1 0 482870107 91435008 21605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21605 603 41 0 22282 0
vsize: 89292
[startup+920.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22433 0 1 0 91912 92 0 0 25 0 1 0 482870107 91435008 21606 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21606 603 41 0 22282 0
vsize: 89292
[startup+930.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22433 0 1 0 92911 92 0 0 25 0 1 0 482870107 91435008 21606 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21606 603 41 0 22282 0
vsize: 89292
[startup+940.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22433 0 1 0 93911 93 0 0 25 0 1 0 482870107 91435008 21606 4294967295 134512640 134672761 3221224544 3221223612 1075346603 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21606 603 41 0 22282 0
vsize: 89292
[startup+950.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22433 0 1 0 94911 93 0 0 25 0 1 0 482870107 91435008 21606 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21606 603 41 0 22282 0
vsize: 89292
[startup+960.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22433 0 1 0 95911 93 0 0 25 0 1 0 482870107 91435008 21606 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21606 603 41 0 22282 0
vsize: 89292
[startup+970.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22433 0 1 0 96911 93 0 0 25 0 1 0 482870107 91435008 21606 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21606 603 41 0 22282 0
vsize: 89292
[startup+980.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22435 0 1 0 97911 93 0 0 25 0 1 0 482870107 91435008 21608 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21608 603 41 0 22282 0
vsize: 89292
[startup+990.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22435 0 1 0 98911 94 0 0 25 0 1 0 482870107 91435008 21608 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21608 603 41 0 22282 0
vsize: 89292
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22435 0 1 0 99911 94 0 0 25 0 1 0 482870107 91435008 21608 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21608 603 41 0 22282 0
vsize: 89292
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22435 0 1 0 100911 94 0 0 25 0 1 0 482870107 91435008 21608 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21608 603 41 0 22282 0
vsize: 89292
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22435 0 1 0 101911 94 0 0 25 0 1 0 482870107 91435008 21608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21608 603 41 0 22282 0
vsize: 89292
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22435 0 1 0 102911 95 0 0 25 0 1 0 482870107 91435008 21608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21608 603 41 0 22282 0
vsize: 89292
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22435 0 1 0 103910 95 0 0 25 0 1 0 482870107 91435008 21608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21608 603 41 0 22282 0
vsize: 89292
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22435 0 1 0 104910 95 0 0 25 0 1 0 482870107 91435008 21608 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21608 603 41 0 22282 0
vsize: 89292
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22435 0 1 0 105910 96 0 0 25 0 1 0 482870107 91435008 21608 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21608 603 41 0 22282 0
vsize: 89292
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22438 0 1 0 106909 96 0 0 25 0 1 0 482870107 91435008 21611 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21611 603 41 0 22282 0
vsize: 89292
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22438 0 1 0 107909 96 0 0 25 0 1 0 482870107 91435008 21611 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21611 603 41 0 22282 0
vsize: 89292
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22438 0 1 0 108909 97 0 0 25 0 1 0 482870107 91435008 21611 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21611 603 41 0 22282 0
vsize: 89292
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22438 0 1 0 109909 97 0 0 25 0 1 0 482870107 91435008 21611 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21611 603 41 0 22282 0
vsize: 89292
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22441 0 1 0 110909 97 0 0 25 0 1 0 482870107 91435008 21614 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21614 603 41 0 22282 0
vsize: 89292
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22441 0 1 0 111909 97 0 0 25 0 1 0 482870107 91435008 21614 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21614 603 41 0 22282 0
vsize: 89292
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22441 0 1 0 112909 98 0 0 25 0 1 0 482870107 91435008 21614 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21614 603 41 0 22282 0
vsize: 89292
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22441 0 1 0 113909 98 0 0 25 0 1 0 482870107 91435008 21614 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21614 603 41 0 22282 0
vsize: 89292
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22442 0 1 0 114908 98 0 0 25 0 1 0 482870107 91435008 21615 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21615 603 41 0 22282 0
vsize: 89292
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22443 0 1 0 115908 99 0 0 25 0 1 0 482870107 91435008 21616 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21616 603 41 0 22282 0
vsize: 89292
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22446 0 1 0 116908 99 0 0 25 0 1 0 482870107 91435008 21619 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21619 603 41 0 22282 0
vsize: 89292
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22446 0 1 0 117908 99 0 0 25 0 1 0 482870107 91435008 21619 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21619 603 41 0 22282 0
vsize: 89292
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22446 0 1 0 118908 100 0 0 25 0 1 0 482870107 91435008 21619 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21619 603 41 0 22282 0
vsize: 89292
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21824
Raw data (stat): 21824 (minisat+) R 21823 25347 25346 0 -1 0 22446 0 1 0 119907 100 0 0 25 0 1 0 482870107 91435008 21619 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22323 21619 603 41 0 22282 0
vsize: 89292
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 21824
Raw data (stat): 21824 (minisat+) Z 21823 25347 25346 0 -1 12 22449 0 1 0 119908 104 0 0 25 0 1 0 482870107 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.1
CPU time (s): 1200.13
CPU user time (s): 1199.08
CPU system time (s): 1.04884
CPU usage (%): 100.003
Max. virtual memory (Kb): 89292
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####