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-ran12x12.opb
MD5SUM	eac61d4d68844395596b0518195dd6df
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	493056
Optimality of the best value was proved	NO
Number of terms in the objective function	3024
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	839045346
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	839045346
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	41.1977
Number of variables	3024
Total number of constraints	168
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	168
Minimum length of a constraint	21
Maximum length of a constraint	240
Trace number 14806

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        800096 kB
Buffers:          5524 kB
Cached:         205752 kB
SwapCached:          0 kB
Active:          60344 kB
Inactive:       153888 kB
HighTotal:      131008 kB
HighFree:        77028 kB
LowTotal:       903652 kB
LowFree:        723068 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14600 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 01:50:31 (client local time) WITH STATUS 10 IN 1200.29 SECONDS
stats: 19258 7 1200.29 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 192 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 190]---> Adder-cost: 244   maxlim: 29300   bits: 15/15
c ---[ 188]---> Adder-cost: 220   maxlim: 11124   bits: 14/14
c ---[ 186]---> Adder-cost: 244   maxlim: 29812   bits: 15/15
c ---[ 184]---> Adder-cost: 236   maxlim: 18164   bits: 15/15
c ---[ 182]---> Adder-cost: 244   maxlim: 29812   bits: 15/15
c ---[ 180]---> Adder-cost: 244   maxlim: 28916   bits: 15/15
c ---[ 178]---> Adder-cost: 220   maxlim: 11252   bits: 14/14
c ---[ 176]---> Adder-cost: 244   maxlim: 29556   bits: 15/15
c ---[ 174]---> Adder-cost: 236   maxlim: 18420   bits: 15/15
c ---[ 172]---> Adder-cost: 244   maxlim: 30196   bits: 15/15
c ---[ 170]---> Adder-cost: 244   maxlim: 29172   bits: 15/15
c ---[ 168]---> Adder-cost: 244   maxlim: 30068   bits: 15/15
c ---[ 166]---> Adder-cost: 220   maxlim: 11380   bits: 14/14
c ---[ 164]---> Adder-cost: 220   maxlim: 11508   bits: 14/14
c ---[ 162]---> Adder-cost: 256   maxlim: 36468   bits: 16/16
c ---[ 160]---> Adder-cost: 256   maxlim: 35700   bits: 16/16
c ---[ 158]---> Adder-cost: 256   maxlim: 36724   bits: 16/16
c ---[ 156]---> Adder-cost: 220   maxlim: 11508   bits: 14/14
c ---[ 154]---> Adder-cost: 256   maxlim: 34804   bits: 16/16
c ---[ 152]---> Adder-cost: 256   maxlim: 36340   bits: 16/16
c ---[ 150]---> Adder-cost: 240   maxlim: 21108   bits: 15/15
c ---[ 148]---> Adder-cost: 198   maxlim: 5748   bits: 13/13
c ---[ 146]---> Adder-cost: 256   maxlim: 33268   bits: 16/16
c ---[ 144]---> Adder-cost: 240   maxlim: 21236   bits: 15/15
c ---[ 143]---> BDD-cost:   13
c ---[ 142]---> BDD-cost:   12
c ---[ 141]---> BDD-cost:   17
c ---[ 140]---> BDD-cost:   14
c ---[ 139]---> BDD-cost:   15
c ---[ 138]---> BDD-cost:   15
c ---[ 137]---> BDD-cost:   11
c ---[ 136]---> BDD-cost:   14
c ---[ 135]---> BDD-cost:   14
c ---[ 134]---> BDD-cost:   17
c ---[ 133]---> BDD-cost:   14
c ---[ 132]---> BDD-cost:   13
c ---[ 131]---> BDD-cost:   12
c ---[ 130]---> BDD-cost:   17
c ---[ 129]---> BDD-cost:   17
c ---[ 128]---> BDD-cost:   12
c ---[ 127]---> BDD-cost:   17
c ---[ 126]---> BDD-cost:   17
c ---[ 125]---> BDD-cost:   15
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   17
c ---[ 122]---> BDD-cost:   14
c ---[ 121]---> BDD-cost:   17
c ---[ 120]---> BDD-cost:   17
c ---[ 119]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   12
c ---[ 116]---> BDD-cost:   17
c ---[ 115]---> BDD-cost:   12
c ---[ 114]---> BDD-cost:   17
c ---[ 113]---> BDD-cost:   17
c ---[ 112]---> BDD-cost:   15
c ---[ 111]---> BDD-cost:   11
c ---[ 110]---> BDD-cost:   17
c ---[ 109]---> BDD-cost:   14
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   17
c ---[ 106]---> BDD-cost:   17
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   14
c ---[ 102]---> BDD-cost:   12
c ---[ 101]---> BDD-cost:   14
c ---[ 100]---> BDD-cost:   14
c ---[  99]---> BDD-cost:   15
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   13
c ---[  96]---> BDD-cost:   14
c ---[  95]---> BDD-cost:   14
c ---[  94]---> BDD-cost:   14
c ---[  93]---> BDD-cost:   14
c ---[  92]---> BDD-cost:   13
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   13
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   17
c ---[  86]---> BDD-cost:   13
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   12
c ---[  80]---> BDD-cost:   17
c ---[  79]---> BDD-cost:   12
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   17
c ---[  76]---> BDD-cost:   12
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   11
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   14
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   17
c ---[  69]---> BDD-cost:   13
c ---[  68]---> BDD-cost:   12
c ---[  67]---> BDD-cost:   17
c ---[  66]---> BDD-cost:   12
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   16
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   15
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   17
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   15
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:   11
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   11
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   15
c ---[  42]---> BDD-cost:   13
c ---[  41]---> BDD-cost:   12
c ---[  40]---> BDD-cost:   17
c ---[  39]---> BDD-cost:   12
c ---[  38]---> BDD-cost:   17
c ---[  37]---> BDD-cost:   15
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   17
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:   17
c ---[  30]---> BDD-cost:   17
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   12
c ---[  27]---> BDD-cost:   13
c ---[  26]---> BDD-cost:   12
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:   17
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   13
c ---[  16]---> BDD-cost:   13
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   12
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   13
c ---[   2]---> BDD-cost:   12
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   40508   140677 |   13502       0        0     nan |  0.000 % |
c |       100 |   40415   140352 |   14852      89      279     3.1 | 22.670 % |
c |       250 |   40287   139920 |   16337     219      727     3.3 | 22.894 % |
c |       475 |   40137   139408 |   17971     427     1389     3.3 | 23.169 % |
c |       812 |   40090   139251 |   19768     757     2522     3.3 | 23.251 % |
c |      1319 |   39827   138346 |   21745    1232     4167     3.4 | 23.709 % |
c |      2078 |   39726   137997 |   23919    1978     7596     3.8 | 23.862 % |
c |      3218 |   39622   137621 |   26311    3104    13060     4.2 | 24.035 % |
c |      4926 |   39450   137041 |   28942    4792    24650     5.1 | 24.351 % |
c |      7488 |   39420   136943 |   31837    7350    50483     6.9 | 24.402 % |
c |     11332 |   39340   136663 |   35020   11189   151268    13.5 | 24.554 % |
c |     17098 |   39089   135820 |   38522   16921   208217    12.3 | 25.023 % |
c |     25747 |   38826   134961 |   42375   25534   315160    12.3 | 25.563 % |
c ==============================================================================
c [1mFound solution: 2373072[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 6078   maxlim: 1731858   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36868 |   81266   286566 |   27088   36654  1088112    29.7 | 25.563 % |
c |     36968 |   81259   286543 |   29796   14051   781106    55.6 | 15.866 % |
c |     37118 |   81259   286543 |   32776   14201   781790    55.1 | 15.866 % |
c |     37343 |   81259   286543 |   36054   14426   782851    54.3 | 15.866 % |
c |     37681 |   81259   286543 |   39659   14764   784364    53.1 | 15.866 % |
c |     38187 |   81259   286543 |   43625   15270   786797    51.5 | 15.866 % |
c |     38946 |   81259   286543 |   47988   16029   791000    49.3 | 15.866 % |
c |     40085 |   81243   286491 |   52786   17166   807878    47.1 | 15.885 % |
c |     41793 |   81243   286491 |   58065   18874   823239    43.6 | 15.885 % |
c |     44355 |   81236   286468 |   63872   21435   859448    40.1 | 15.891 % |
c |     48199 |   81201   286351 |   70259   25275   894972    35.4 | 15.935 % |
c |     53965 |   81176   286270 |   77285   31038   966277    31.1 | 15.967 % |
c |     62615 |   81176   286270 |   85013   39688  1207102    30.4 | 15.967 % |
c |     75589 |   81070   285922 |   93515   52645  1501302    28.5 | 16.093 % |
c ==============================================================================
c [1mFound solution: 2355797[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1749133   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80588 |   81025   285866 |   27008   57633  1554802    27.0 | 16.093 % |
c |     80688 |   81025   285866 |   29708   19960   149155     7.5 | 16.211 % |
c |     80838 |   81025   285866 |   32679   20110   151057     7.5 | 16.211 % |
c |     81063 |   81025   285866 |   35947   20335   153258     7.5 | 16.211 % |
c |     81400 |   81025   285866 |   39542   20672   157747     7.6 | 16.211 % |
c |     81906 |   81025   285866 |   43496   21178   166225     7.8 | 16.211 % |
c |     82665 |   81025   285866 |   47846   21937   172892     7.9 | 16.211 % |
c |     83805 |   81025   285866 |   52630   23077   181862     7.9 | 16.211 % |
c |     85513 |   81025   285866 |   57894   24785   197827     8.0 | 16.211 % |
c ==============================================================================
c [1mFound solution: 2230733[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1874197   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88055 |   81038   285997 |   27012   27327   229702     8.4 | 16.211 % |
c |     88155 |   81029   285968 |   29713   27426   230273     8.4 | 16.265 % |
c |     88306 |   81029   285968 |   32684   27577   231609     8.4 | 16.265 % |
c |     88531 |   81029   285968 |   35952   27802   233492     8.4 | 16.265 % |
c |     88868 |   81029   285968 |   39548   28139   240936     8.6 | 16.265 % |
c |     89374 |   81029   285968 |   43503   28645   246829     8.6 | 16.265 % |
c |     90133 |   81029   285968 |   47853   29404   253347     8.6 | 16.265 % |
c |     91272 |   81029   285968 |   52638   30543   278617     9.1 | 16.265 % |
c |     92980 |   81029   285968 |   57902   32251   337979    10.5 | 16.265 % |
c |     95542 |   81029   285968 |   63692   34813   374946    10.8 | 16.265 % |
c |     99388 |   81029   285968 |   70062   38659   688203    17.8 | 16.265 % |
c |    105154 |   81013   285916 |   77068   44421   856041    19.3 | 16.284 % |
c |    113803 |   81013   285916 |   84775   53070  1020410    19.2 | 16.284 % |
c ==============================================================================
c [1mFound solution: 1938543[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2166387   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    117705 |   81011   285742 |   27003   56856  1096543    19.3 | 16.284 % |
c |    117805 |   81011   285742 |   29703   21876   273209    12.5 | 16.330 % |
c |    117956 |   81011   285742 |   32673   22027   274007    12.4 | 16.330 % |
c |    118181 |   81011   285742 |   35940   22252   275269    12.4 | 16.330 % |
c |    118518 |   81011   285742 |   39535   22589   277244    12.3 | 16.330 % |
c |    119024 |   81011   285742 |   43488   23095   280627    12.2 | 16.330 % |
c |    119783 |   81011   285742 |   47837   23854   295496    12.4 | 16.330 % |
c |    120922 |   81011   285742 |   52621   24993   305057    12.2 | 16.330 % |
c |    122630 |   81011   285742 |   57883   26701   339479    12.7 | 16.330 % |
c |    125194 |   81011   285742 |   63671   29265   513445    17.5 | 16.330 % |
c |    129038 |   81011   285742 |   70038   33109   588312    17.8 | 16.330 % |
c |    134804 |   81011   285742 |   77042   38875   668809    17.2 | 16.330 % |
c |    143453 |   81011   285742 |   84746   47524   914978    19.3 | 16.330 % |
c ==============================================================================
c [1mFound solution: 1374872[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2730058   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    146092 |   81026   285868 |   27008   50163   966211    19.3 | 16.330 % |
c |    146192 |   81026   285868 |   29708   21497   336527    15.7 | 16.371 % |
c |    146343 |   81026   285868 |   32679   21648   337346    15.6 | 16.371 % |
c |    146568 |   81026   285868 |   35947   21873   338510    15.5 | 16.371 % |
c |    146905 |   81026   285868 |   39542   22210   340226    15.3 | 16.371 % |
c |    147411 |   81026   285868 |   43496   22716   343487    15.1 | 16.371 % |
c |    148170 |   81026   285868 |   47846   23475   349274    14.9 | 16.371 % |
c |    149310 |   81026   285868 |   52630   24615   414647    16.8 | 16.371 % |
c |    151020 |   81026   285868 |   57894   26325   430302    16.3 | 16.371 % |
c |    153582 |   81026   285868 |   63683   28887   459449    15.9 | 16.371 % |
c |    157427 |   81026   285868 |   70051   32732   507423    15.5 | 16.371 % |
c |    163193 |   81026   285868 |   77056   38498   641129    16.7 | 16.371 % |
c |    171843 |   81017   285837 |   84762   47145  1007625    21.4 | 16.377 % |
c |    184817 |   81017   285837 |   93238   60119  2099823    34.9 | 16.377 % |
c |    204278 |   81017   285837 |  102562   79580  4025724    50.6 | 16.377 % |
c |    233470 |   81017   285837 |  112819  108772  5488057    50.5 | 16.377 % |
c |    277259 |   81008   285806 |  124101   60984  2443782    40.1 | 16.383 % |
c |    342943 |   81008   285806 |  136511  126668 13598869   107.4 | 16.383 % |
c |    441470 |   81008   285806 |  150162  107843 43636887   404.6 | 16.383 % |
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_bit#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.95 0.90 2/55 32396
Raw data (stat): 32396 (runsolver) R 32395 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 418396370 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99992 s]
Raw data (loadavg): 0.87 0.95 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 1529 0 0 0 995 4 0 0 25 0 1 0 418396370 8032256 1498 4294967295 134512640 134672761 3221224624 3221223824 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1961 1498 603 41 0 1920 0
vsize: 7844
[startup+19.9995 s]
Raw data (loadavg): 0.89 0.95 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 1839 0 0 0 1994 5 0 0 25 0 1 0 418396370 9359360 1808 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2285 1808 603 41 0 2244 0
vsize: 9140
[startup+30.0007 s]
Raw data (loadavg): 0.90 0.95 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 6345 0 0 0 2982 17 0 0 25 0 1 0 418396370 25485312 5694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6222 5694 603 41 0 6181 0
vsize: 24888
[startup+40.0003 s]
Raw data (loadavg): 0.92 0.95 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 6350 0 0 0 3982 17 0 0 25 0 1 0 418396370 25485312 5699 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6222 5699 603 41 0 6181 0
vsize: 24888
[startup+50.0007 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 6350 0 0 0 4982 17 0 0 25 0 1 0 418396370 25485312 5699 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6222 5699 603 41 0 6181 0
vsize: 24888
[startup+60.0003 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7001 0 0 0 5979 20 0 0 25 0 1 0 418396370 28184576 6350 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6881 6350 603 41 0 6840 0
vsize: 27524
[startup+70 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7134 0 0 0 6979 20 0 0 25 0 1 0 418396370 28725248 6483 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7013 6483 603 41 0 6972 0
vsize: 28052
[startup+80.0007 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7356 0 0 0 7978 21 0 0 25 0 1 0 418396370 29401088 6690 4294967295 134512640 134672761 3221224624 3221223748 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7178 6690 603 41 0 7137 0
vsize: 28712
[startup+90.0008 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7356 0 0 0 8978 21 0 0 25 0 1 0 418396370 29401088 6690 4294967295 134512640 134672761 3221224624 3221223748 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7178 6690 603 41 0 7137 0
vsize: 28712
[startup+100.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7356 0 0 0 9978 21 0 0 25 0 1 0 418396370 29401088 6690 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7178 6690 603 41 0 7137 0
vsize: 28712
[startup+110.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7356 0 0 0 10978 22 0 0 25 0 1 0 418396370 29401088 6690 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7178 6690 603 41 0 7137 0
vsize: 28712
[startup+120.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7357 0 0 0 11978 22 0 0 25 0 1 0 418396370 29401088 6691 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7178 6691 603 41 0 7137 0
vsize: 28712
[startup+130.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7357 0 0 0 12978 22 0 0 25 0 1 0 418396370 29401088 6691 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7178 6691 603 41 0 7137 0
vsize: 28712
[startup+140.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7357 0 0 0 13979 22 0 0 25 0 1 0 418396370 29401088 6691 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7178 6691 603 41 0 7137 0
vsize: 28712
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7358 0 0 0 14979 22 0 0 25 0 1 0 418396370 29401088 6692 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7178 6692 603 41 0 7137 0
vsize: 28712
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7358 0 0 0 15979 22 0 0 25 0 1 0 418396370 29401088 6692 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7178 6692 603 41 0 7137 0
vsize: 28712
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7358 0 0 0 16979 22 0 0 25 0 1 0 418396370 29401088 6692 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7178 6692 603 41 0 7137 0
vsize: 28712
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 7923 0 0 0 17978 23 0 0 25 0 1 0 418396370 31682560 7257 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7735 7257 603 41 0 7694 0
vsize: 30940
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 8325 0 0 0 18977 24 0 0 25 0 1 0 418396370 33296384 7659 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8129 7659 603 41 0 8088 0
vsize: 32516
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 9037 0 0 0 19975 26 0 0 25 0 1 0 418396370 36515840 8371 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8915 8371 603 41 0 8874 0
vsize: 35660
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 10123 0 0 0 20971 30 0 0 25 0 1 0 418396370 40960000 9457 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10000 9457 603 41 0 9959 0
vsize: 40000
[startup+220 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 10457 0 0 0 21971 31 0 0 25 0 1 0 418396370 42303488 9791 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10328 9791 603 41 0 10287 0
vsize: 41312
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 10753 0 0 0 22970 32 0 0 25 0 1 0 418396370 43380736 10087 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10591 10087 603 41 0 10550 0
vsize: 42364
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 11230 0 0 0 23968 34 0 0 25 0 1 0 418396370 45404160 10564 4294967295 134512640 134672761 3221224624 3221223728 134555105 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11085 10564 603 41 0 11044 0
vsize: 44340
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 11952 0 0 0 24966 36 0 0 25 0 1 0 418396370 48238592 11286 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11777 11286 603 41 0 11736 0
vsize: 47108
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 12259 0 0 0 25965 37 0 0 25 0 1 0 418396370 49582080 11593 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12105 11593 603 41 0 12064 0
vsize: 48420
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 12259 0 0 0 26965 37 0 0 25 0 1 0 418396370 49582080 11593 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12105 11593 603 41 0 12064 0
vsize: 48420
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 12259 0 0 0 27965 37 0 0 25 0 1 0 418396370 49582080 11593 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12105 11593 603 41 0 12064 0
vsize: 48420
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 12259 0 0 0 28965 37 0 0 25 0 1 0 418396370 49582080 11593 4294967295 134512640 134672761 3221224624 3221223760 134560613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12105 11593 603 41 0 12064 0
vsize: 48420
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 12259 0 0 0 29966 37 0 0 25 0 1 0 418396370 49582080 11593 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12105 11593 603 41 0 12064 0
vsize: 48420
[startup+310 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 12259 0 0 0 30966 37 0 0 25 0 1 0 418396370 49582080 11593 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12105 11593 603 41 0 12064 0
vsize: 48420
[startup+320 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 12259 0 0 0 31966 37 0 0 25 0 1 0 418396370 49582080 11593 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12105 11593 603 41 0 12064 0
vsize: 48420
[startup+330 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 12259 0 0 0 32966 37 0 0 25 0 1 0 418396370 49582080 11593 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12105 11593 603 41 0 12064 0
vsize: 48420
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 12463 0 0 0 33966 38 0 0 25 0 1 0 418396370 50393088 11797 4294967295 134512640 134672761 3221224624 3221223760 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12303 11797 603 41 0 12262 0
vsize: 49212
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 13059 0 0 0 34965 39 0 0 25 0 1 0 418396370 52805632 12393 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12892 12393 603 41 0 12851 0
vsize: 51568
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 13592 0 0 0 35964 40 0 0 25 0 1 0 418396370 54939648 12926 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13413 12926 603 41 0 13372 0
vsize: 53652
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 14081 0 0 0 36963 42 0 0 25 0 1 0 418396370 56954880 13415 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13905 13415 603 41 0 13864 0
vsize: 55620
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 14678 0 0 0 37961 44 0 0 25 0 1 0 418396370 59375616 14012 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14496 14012 603 41 0 14455 0
vsize: 57984
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 15367 0 0 0 38959 46 0 0 25 0 1 0 418396370 62324736 14701 4294967295 134512640 134672761 3221224624 3221223808 134559516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15216 14701 603 41 0 15175 0
vsize: 60864
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 16135 0 0 0 39957 48 0 0 25 0 1 0 418396370 65404928 15469 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15968 15469 603 41 0 15927 0
vsize: 63872
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 16917 0 0 0 40955 50 0 0 25 0 1 0 418396370 68595712 16251 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16747 16251 603 41 0 16706 0
vsize: 66988
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 17647 0 0 0 41952 53 0 0 25 0 1 0 418396370 71643136 16981 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17491 16981 603 41 0 17450 0
vsize: 69964
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 18377 0 0 0 42950 55 0 0 25 0 1 0 418396370 74596352 17711 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18212 17711 603 41 0 18171 0
vsize: 72848
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 19142 0 0 0 43948 58 0 0 25 0 1 0 418396370 77664256 18476 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18961 18476 603 41 0 18920 0
vsize: 75844
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 19942 0 0 0 44946 60 0 0 25 0 1 0 418396370 80977920 19276 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19770 19276 603 41 0 19729 0
vsize: 79080
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 20504 0 0 0 45945 61 0 0 25 0 1 0 418396370 83255296 19838 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20326 19838 603 41 0 20285 0
vsize: 81304
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 20799 0 0 0 46944 62 0 0 25 0 1 0 418396370 84987904 20133 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20749 20133 603 41 0 20708 0
vsize: 82996
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21003 0 0 0 47943 63 0 0 25 0 1 0 418396370 85798912 20337 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20947 20337 603 41 0 20906 0
vsize: 83788
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 48943 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 49943 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 50943 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 51943 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 52944 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 53943 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223808 134559683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 54944 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 55944 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 56944 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 57944 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223808 134559400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 58944 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 59944 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223808 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 60944 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 61944 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223808 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21046 0 0 0 62944 64 0 0 25 0 1 0 418396370 85929984 20380 4294967295 134512640 134672761 3221224624 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20979 20380 603 41 0 20938 0
vsize: 83916
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 21458 0 0 0 63942 66 0 0 25 0 1 0 418396370 87658496 20792 4294967295 134512640 134672761 3221224624 3221223728 134560250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21401 20792 603 41 0 21360 0
vsize: 85604
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 22144 0 0 0 64941 68 0 0 25 0 1 0 418396370 90460160 21478 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22085 21478 603 41 0 22044 0
vsize: 88340
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 22785 0 0 0 65939 70 0 0 25 0 1 0 418396370 93134848 22119 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22738 22119 603 41 0 22697 0
vsize: 90952
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 23463 0 0 0 66937 71 0 0 25 0 1 0 418396370 95825920 22797 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23395 22797 603 41 0 23354 0
vsize: 93580
[startup+680.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 24111 0 0 0 67936 73 0 0 25 0 1 0 418396370 98488320 23445 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24045 23445 603 41 0 24004 0
vsize: 96180
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 24747 0 0 0 68935 74 0 0 25 0 1 0 418396370 101130240 24081 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24690 24081 603 41 0 24649 0
vsize: 98760
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 25407 0 0 0 69933 76 0 0 25 0 1 0 418396370 103809024 24741 4294967295 134512640 134672761 3221224624 3221223808 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25344 24741 603 41 0 25303 0
vsize: 101376
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 26079 0 0 0 70932 77 0 0 25 0 1 0 418396370 106618880 25413 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26030 25413 603 41 0 25989 0
vsize: 104120
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 26748 0 0 0 71930 80 0 0 25 0 1 0 418396370 109268992 26082 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26677 26082 603 41 0 26636 0
vsize: 106708
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 27380 0 0 0 72928 81 0 0 25 0 1 0 418396370 111943680 26714 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27330 26714 603 41 0 27289 0
vsize: 109320
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 28012 0 0 0 73927 83 0 0 25 0 1 0 418396370 114503680 27346 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27955 27346 603 41 0 27914 0
vsize: 111820
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 28642 0 0 0 74925 85 0 0 25 0 1 0 418396370 117075968 27976 4294967295 134512640 134672761 3221224624 3221223728 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28583 27976 603 41 0 28542 0
vsize: 114332
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 29291 0 0 0 75924 86 0 0 25 0 1 0 418396370 119713792 28625 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29227 28625 603 41 0 29186 0
vsize: 116908
[startup+770.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 30054 0 0 0 76922 88 0 0 25 0 1 0 418396370 122912768 29388 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30008 29388 603 41 0 29967 0
vsize: 120032
[startup+780.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 30666 0 0 0 77921 90 0 0 25 0 1 0 418396370 125440000 30000 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30625 30000 603 41 0 30584 0
vsize: 122500
[startup+790.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 31267 0 0 0 78919 92 0 0 25 0 1 0 418396370 127799296 30601 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31201 30601 603 41 0 31160 0
vsize: 124804
[startup+800.007 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 31878 0 0 0 79918 93 0 0 25 0 1 0 418396370 130420736 31212 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31841 31212 603 41 0 31800 0
vsize: 127364
[startup+810.007 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 32465 0 0 0 80917 94 0 0 25 0 1 0 418396370 132812800 31799 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32425 31799 603 41 0 32384 0
vsize: 129700
[startup+820.007 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 33036 0 0 0 81916 95 0 0 25 0 1 0 418396370 135061504 32370 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32974 32370 603 41 0 32933 0
vsize: 131896
[startup+830.008 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 33659 0 0 0 82915 96 0 0 25 0 1 0 418396370 137601024 32993 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33594 32993 603 41 0 33553 0
vsize: 134376
[startup+840.007 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 34245 0 0 0 83914 98 0 0 25 0 1 0 418396370 140107776 33579 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34206 33579 603 41 0 34165 0
vsize: 136824
[startup+850.007 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 34834 0 0 0 84913 98 0 0 25 0 1 0 418396370 142524416 34168 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34796 34168 603 41 0 34755 0
vsize: 139184
[startup+860.007 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 35356 0 0 0 85912 99 0 0 25 0 1 0 418396370 144658432 34690 4294967295 134512640 134672761 3221224624 3221223728 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35317 34690 603 41 0 35276 0
vsize: 141268
[startup+870.007 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 35878 0 0 0 86911 101 0 0 25 0 1 0 418396370 146780160 35212 4294967295 134512640 134672761 3221224624 3221223808 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35835 35212 603 41 0 35794 0
vsize: 143340
[startup+880.008 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 36428 0 0 0 87911 101 0 0 25 0 1 0 418396370 149024768 35762 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36383 35762 603 41 0 36342 0
vsize: 145532
[startup+890.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 36958 0 0 0 88910 102 0 0 25 0 1 0 418396370 151171072 36292 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36907 36292 603 41 0 36866 0
vsize: 147628
[startup+900.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 37462 0 0 0 89909 104 0 0 25 0 1 0 418396370 153305088 36796 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37428 36796 603 41 0 37387 0
vsize: 149712
[startup+910.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 37988 0 0 0 90908 105 0 0 25 0 1 0 418396370 155422720 37322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37945 37322 603 41 0 37904 0
vsize: 151780
[startup+920.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 38514 0 0 0 91907 106 0 0 25 0 1 0 418396370 157663232 37848 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38492 37848 603 41 0 38451 0
vsize: 153968
[startup+930.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 39157 0 0 0 92906 107 0 0 25 0 1 0 418396370 160317440 38491 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39140 38491 603 41 0 39099 0
vsize: 156560
[startup+940.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 39693 0 0 0 93905 108 0 0 25 0 1 0 418396370 162435072 39027 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39657 39027 603 41 0 39616 0
vsize: 158628
[startup+950.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 40230 0 0 0 94905 109 0 0 25 0 1 0 418396370 164728832 39564 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40217 39564 603 41 0 40176 0
vsize: 160868
[startup+960.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 40767 0 0 0 95904 110 0 0 25 0 1 0 418396370 166834176 40101 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40731 40101 603 41 0 40690 0
vsize: 162924
[startup+970.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 41262 0 0 0 96903 111 0 0 25 0 1 0 418396370 168824832 40596 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41217 40596 603 41 0 41176 0
vsize: 164868
[startup+980.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 41829 0 0 0 97902 112 0 0 25 0 1 0 418396370 171249664 41163 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41809 41163 603 41 0 41768 0
vsize: 167236
[startup+990.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 42380 0 0 0 98900 114 0 0 25 0 1 0 418396370 173404160 41714 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42335 41714 603 41 0 42294 0
vsize: 169340
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 42981 0 0 0 99900 115 0 0 25 0 1 0 418396370 175878144 42315 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42939 42315 603 41 0 42898 0
vsize: 171756
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 43531 0 0 0 100899 116 0 0 25 0 1 0 418396370 178114560 42865 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43485 42865 603 41 0 43444 0
vsize: 173940
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 44055 0 0 0 101897 118 0 0 25 0 1 0 418396370 180346880 43389 4294967295 134512640 134672761 3221224624 3221223728 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44030 43389 603 41 0 43989 0
vsize: 176120
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 44599 0 0 0 102896 119 0 0 25 0 1 0 418396370 182476800 43933 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44550 43933 603 41 0 44509 0
vsize: 178200
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 45087 0 0 0 103895 120 0 0 25 0 1 0 418396370 184487936 44421 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45041 44421 603 41 0 45000 0
vsize: 180164
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 45572 0 0 0 104894 121 0 0 25 0 1 0 418396370 186507264 44906 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45534 44906 603 41 0 45493 0
vsize: 182136
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 46074 0 0 0 105893 122 0 0 25 0 1 0 418396370 188506112 45408 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46022 45408 603 41 0 45981 0
vsize: 184088
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 46582 0 0 0 106891 124 0 0 25 0 1 0 418396370 190640128 45916 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46543 45916 603 41 0 46502 0
vsize: 186172
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 47091 0 0 0 107890 125 0 0 25 0 1 0 418396370 192724992 46425 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47052 46425 603 41 0 47011 0
vsize: 188208
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 47576 0 0 0 108889 127 0 0 25 0 1 0 418396370 194719744 46910 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47539 46910 603 41 0 47498 0
vsize: 190156
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 48103 0 0 0 109888 127 0 0 25 0 1 0 418396370 196882432 47437 4294967295 134512640 134672761 3221224624 3221223808 134559489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48067 47437 603 41 0 48026 0
vsize: 192268
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 48594 0 0 0 110887 129 0 0 25 0 1 0 418396370 198950912 47928 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48572 47928 603 41 0 48531 0
vsize: 194288
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 49080 0 0 0 111885 131 0 0 25 0 1 0 418396370 200929280 48414 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49055 48414 603 41 0 49014 0
vsize: 196220
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 49585 0 0 0 112884 132 0 0 25 0 1 0 418396370 203091968 48919 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49583 48919 603 41 0 49542 0
vsize: 198332
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 50031 0 0 0 113884 133 0 0 25 0 1 0 418396370 204824576 49365 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50006 49365 603 41 0 49965 0
vsize: 200024
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 50538 0 0 0 114882 135 0 0 25 0 1 0 418396370 206909440 49872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50515 49872 603 41 0 50474 0
vsize: 202060
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 50843 0 0 0 115881 135 0 0 25 0 1 0 418396370 208257024 50177 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50844 50177 603 41 0 50803 0
vsize: 203376
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 51093 0 0 0 116881 136 0 0 25 0 1 0 418396370 209199104 50427 4294967295 134512640 134672761 3221224624 3221223888 134562145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51074 50427 603 41 0 51033 0
vsize: 204296
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 51753 0 0 0 117879 138 0 0 25 0 1 0 418396370 212029440 51087 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51765 51087 603 41 0 51724 0
vsize: 207060
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 52283 0 0 0 118877 140 0 0 25 0 1 0 418396370 214183936 51617 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52291 51617 603 41 0 52250 0
vsize: 209164
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32396
Raw data (stat): 32396 (minisat+) R 32395 30927 30926 0 -1 0 52750 0 0 0 119876 141 0 0 25 0 1 0 418396370 216059904 52084 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52749 52084 603 41 0 52708 0
vsize: 210996
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 32396
Raw data (stat): 32396 (minisat+) Z 32395 30927 30926 0 -1 12 52753 0 0 0 119877 151 0 0 25 0 1 0 418396370 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.12
CPU time (s): 1200.29
CPU user time (s): 1198.77
CPU system time (s): 1.51277
CPU usage (%): 100.014
Max. virtual memory (Kb): 210996
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####