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 14797

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        877420 kB
Buffers:          9352 kB
Cached:         119584 kB
SwapCached:        604 kB
Active:          18984 kB
Inactive:       111936 kB
HighTotal:      131008 kB
HighFree:        59416 kB
LowTotal:       903652 kB
LowFree:        818004 kB
SwapTotal:     2097892 kB
SwapFree:      2096484 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5232 kB
Slab:            20692 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 01:42:26 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 19290 7 1200.23 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   51720   175587 |   15515       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9959          
c   -- var.elim.:  2000/9959          
c   -- var.elim.:  3000/9959          
c   -- var.elim.:  4000/9959          
c   -- var.elim.:  5000/9959          
c   -- var.elim.:  6000/9959          
c   -- var.elim.:  7000/9959          
c   -- var.elim.:  8000/9959          
c   -- var.elim.:  9000/9959          
c   -- var.elim.:  9959/9959          
c   -- var.elim.:  1000/2664          
c   -- var.elim.:  2000/2664          
c   -- var.elim.:  2664/2664          
c   -- subsuming                       
c   -- var.elim.:  780/780          
c   -- var.elim.:  733/733          
c   -- subsuming                       
c   -- var.elim.:  41/41          
c   -- var.elim.:  27/27          
c |         0 |   46079   156205 |      --       0       --      -- |     --   | -3801/-9230
c |         0 |   46079   156205 |   18431       0        0     nan |  0.000 % |
c |       100 |   46031   156031 |   20253      96      496     5.2 | 25.560 % |
c |       250 |   46031   156031 |   22279     246      946     3.8 | 25.560 % |
c |       475 |   46031   156031 |   24506     471     1733     3.7 | 25.560 % |
c |       812 |   46031   156031 |   26957     808     2929     3.6 | 25.560 % |
c |      1318 |   46020   155994 |   29646    1311     4983     3.8 | 25.569 % |
c |      2077 |   46009   155957 |   32603    2068     8487     4.1 | 25.578 % |
c |      3216 |   45961   155778 |   35825    3204    16901     5.3 | 25.631 % |
c |      4925 |   45961   155778 |   39408    4913    42001     8.5 | 25.631 % |
c |      7487 |   45928   155667 |   43318    7471    61321     8.2 | 25.658 % |
c |     11331 |   45906   155593 |   47627   11312    93946     8.3 | 25.675 % |
c |     17098 |   45895   155556 |   52377   17078   210770    12.3 | 25.684 % |
c |     25747 |   45776   155146 |   57465   25720   306583    11.9 | 25.825 % |
c |     38721 |   45776   155146 |   63212   38694   848162    21.9 | 25.825 % |
c ==============================================================================
c (current CPU-time: 36.0855 s)
c ==============================================================================
c [1mFound solution: 3923956[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 6663   maxlim: 1768838   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     48043 |   92026   320373 |   27607   48008  1102538    23.0 | 25.825 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8904          
c   -- var.elim.:  2000/8904          
c   -- var.elim.:  3000/8904          
c   -- var.elim.:  4000/8904          
c   -- var.elim.:  5000/8904          
c   -- var.elim.:  6000/8904          
c   -- var.elim.:  7000/8904          
c   -- var.elim.:  8000/8904          
c   -- var.elim.:  8904/8904          
c   -- var.elim.:  288/288          
c   -- var.elim.:  50/50          
c   -- subsuming                       
c   -- var.elim.:  49/49          
c   -- var.elim.:  3/3          
c |     48043 |   91795   319669 |      --   48008       --      -- |     --   | -231/-690
c |     48043 |   91795   319669 |   36718   47531  1093568    23.0 | 25.825 % |
c |     48143 |   91738   319434 |   40364   17465   386324    22.1 | 16.723 % |
c |     48293 |   91738   319434 |   44401   17615   386950    22.0 | 16.723 % |
c |     48518 |   91738   319434 |   48841   17840   388088    21.8 | 16.723 % |
c |     48855 |   91663   319150 |   53681   18168   390058    21.5 | 16.785 % |
c |     49362 |   91663   319150 |   59049   18675   393355    21.1 | 16.785 % |
c |     50121 |   91663   319150 |   64954   19434   398405    20.5 | 16.785 % |
c |     51261 |   91636   319063 |   71429   20572   406044    19.7 | 16.801 % |
c |     52969 |   91636   319063 |   78571   22280   419059    18.8 | 16.801 % |
c ==============================================================================
c (current CPU-time: 52.0551 s)
c ==============================================================================
c [1mFound solution: 3833939[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1858855   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     55044 |   91712   319428 |   27513   24355   439089    18.0 | 16.801 % |
c   -- subsuming                       
c   -- var.elim.:  180/180          
c   -- var.elim.:  89/89          
c |     55044 |   91678   319438 |      --   24355       --      -- |     --   | -34/18
c |     55044 |   91678   319438 |   36671   24317   438573    18.0 | 16.801 % |
c |     55144 |   91668   319403 |   40333   24416   438917    18.0 | 16.849 % |
c |     55294 |   91668   319403 |   44367   24566   439615    17.9 | 16.849 % |
c |     55521 |   91668   319403 |   48804   24793   440828    17.8 | 16.849 % |
c |     55858 |   91668   319403 |   53684   25130   445494    17.7 | 16.849 % |
c |     56364 |   91634   319285 |   59030   25635   448739    17.5 | 16.871 % |
c |     57123 |   91634   319285 |   64934   26394   454748    17.2 | 16.871 % |
c |     58262 |   91611   319200 |   71409   27529   467189    17.0 | 16.882 % |
c |     59970 |   91576   319076 |   78520   29234   483831    16.6 | 16.904 % |
c |     62532 |   91566   319041 |   86363   31794   508956    16.0 | 16.910 % |
c ==============================================================================
c (current CPU-time: 68.4806 s)
c ==============================================================================
c [1mFound solution: 3598177[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2094617   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     64986 |   91617   319326 |   27485   34248   540410    15.8 | 16.910 % |
c   -- subsuming                       
c   -- var.elim.:  142/142          
c   -- var.elim.:  64/64          
c |     64986 |   91588   319182 |      --   34248       --      -- |     --   | -29/-133
c |     64986 |   91588   319182 |   36635   34206   539978    15.8 | 16.910 % |
c |     65086 |   91588   319182 |   40298   34306   541136    15.8 | 16.977 % |
c |     65236 |   91588   319182 |   44328   34456   542207    15.7 | 16.977 % |
c |     65461 |   91588   319182 |   48761   34681   545375    15.7 | 16.977 % |
c |     65798 |   91578   319147 |   53631   35017   548577    15.7 | 16.982 % |
c |     66304 |   91578   319147 |   58994   35523   577477    16.3 | 16.982 % |
c |     67063 |   91578   319147 |   64894   36282   584305    16.1 | 16.982 % |
c ==============================================================================
c (current CPU-time: 73.5578 s)
c ==============================================================================
c [1mFound solution: 3386371[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 2306423   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     67266 |   91617   319379 |   27485   36485   585919    16.1 | 16.982 % |
c   -- subsuming                       
c   -- var.elim.:  64/64          
c   -- var.elim.:  24/24          
c |     67266 |   91593   319144 |      --   36485       --      -- |     --   | -24/-225
c |     67266 |   91593   319144 |   36637   36480   585845    16.1 | 16.982 % |
c |     67366 |   91593   319144 |   40300   36580   586719    16.0 | 17.030 % |
c |     67516 |   91593   319144 |   44331   36730   590262    16.1 | 17.030 % |
c |     67741 |   91593   319144 |   48764   36955   598614    16.2 | 17.030 % |
c |     68078 |   91593   319144 |   53640   37292   601131    16.1 | 17.030 % |
c |     68584 |   91593   319144 |   59004   37798   615289    16.3 | 17.030 % |
c |     69344 |   91593   319144 |   64905   38558   627906    16.3 | 17.030 % |
c |     70484 |   91583   319109 |   71387   39697   654984    16.5 | 17.036 % |
c |     72194 |   91583   319109 |   78526   41407   677219    16.4 | 17.036 % |
c ==============================================================================
c (current CPU-time: 81.0677 s)
c ==============================================================================
c [1mFound solution: 3074664[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2618130   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     72409 |   91522   318967 |   27456   41617   687600    16.5 | 17.036 % |
c   -- subsuming                       
c   -- var.elim.:  127/127          
c   -- var.elim.:  78/78          
c   -- var.elim.:  7/7          
c   -- var.elim.:  19/19          
c   -- var.elim.:  15/15          
c |     72409 |   91463   318857 |      --   41617       --      -- |     --   | -59/-98
c |     72409 |   91463   318857 |   36585   41617   687600    16.5 | 17.036 % |
c |     72509 |   91463   318857 |   40243   20240   226541    11.2 | 17.193 % |
c |     72659 |   91449   318784 |   44261   20389   227367    11.2 | 17.198 % |
c |     72884 |   91449   318784 |   48687   20614   229799    11.1 | 17.198 % |
c |     73221 |   91439   318753 |   53550   20950   231776    11.1 | 17.210 % |
c |     73727 |   91429   318718 |   58898   21454   235542    11.0 | 17.215 % |
c |     74487 |   91418   318681 |   64781   22213   242799    10.9 | 17.221 % |
c |     75626 |   91407   318644 |   71250   23351   250252    10.7 | 17.226 % |
c |     77336 |   91407   318644 |   78375   25061   264964    10.6 | 17.226 % |
c |     79899 |   91407   318644 |   86213   27624   414321    15.0 | 17.226 % |
c |     83744 |   91376   318537 |   94802   31466   525256    16.7 | 17.243 % |
c |     89511 |   91354   318463 |  104257   37227   675025    18.1 | 17.254 % |
c |     98163 |   91354   318463 |  114683   45879  1118450    24.4 | 17.254 % |
c |    111138 |   91343   318426 |  126136   58853  1792783    30.5 | 17.260 % |
c |    130600 |   91343   318426 |  138749   78315  3689243    47.1 | 17.260 % |
c ==============================================================================
c (current CPU-time: 158.936 s)
c ==============================================================================
c [1mFound solution: 3070397[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2622397   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    131406 |   91359   318602 |   27407   79121  3704483    46.8 | 17.260 % |
c   -- subsuming                       
c   -- var.elim.:  133/133          
c   -- var.elim.:  46/46          
c |    131406 |   91335   318365 |      --   79121       --      -- |     --   | -11/-78
c |    131406 |   91335   318365 |   36534   79102  3698365    46.8 | 17.260 % |
c |    131506 |   91335   318365 |   40187   21581  1001914    46.4 | 17.306 % |
c |    131656 |   91325   318330 |   44201   21730  1003210    46.2 | 17.311 % |
c |    131881 |   91325   318330 |   48621   21955  1004843    45.8 | 17.311 % |
c |    132218 |   91325   318330 |   53483   22292  1006985    45.2 | 17.311 % |
c |    132724 |   91325   318330 |   58831   22798  1011981    44.4 | 17.311 % |
c |    133483 |   91304   318258 |   64700   23554  1016815    43.2 | 17.323 % |
c |    134622 |   91276   318164 |   71148   24689  1025895    41.6 | 17.339 % |
c |    136330 |   91257   318074 |   78246   26395  1039944    39.4 | 17.350 % |
c |    138893 |   91222   317935 |   86038   28951  1069854    37.0 | 17.384 % |
c |    142739 |   91222   317935 |   94642   32797  1151335    35.1 | 17.384 % |
c |    148506 |   91222   317935 |  104106   38564  1434386    37.2 | 17.384 % |
c |    157155 |   91222   317935 |  114517   47213  1851887    39.2 | 17.384 % |
c |    170130 |   91213   317907 |  125956   60185  2779596    46.2 | 17.389 % |
c |    189591 |   91203   317872 |  138537   79645  3991083    50.1 | 17.395 % |
c |    218783 |   91203   317872 |  152391  108837  6014530    55.3 | 17.395 % |
c |    262573 |   91193   317837 |  167611  152626  9594718    62.9 | 17.401 % |
c |    328257 |   91193   317837 |  184372   70340  5618250    79.9 | 17.401 % |
c ==============================================================================
c (current CPU-time: 630.873 s)
c ==============================================================================
c [1mFound solution: 2845518[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2847276   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    389749 |   91077   317548 |   27323  131826  9082814    68.9 | 17.401 % |
c   -- subsuming                       
c   -- var.elim.:  187/187          
c   -- var.elim.:  139/139          
c   -- subsuming                       
c   -- var.elim.:  60/60          
c   -- var.elim.:  34/34          
c |    389749 |   90964   317137 |      --  131826       --      -- |     --   | -113/-401
c |    389749 |   90964   317137 |   36385  131459  9045148    68.8 | 17.401 % |
c |    389849 |   90964   317137 |   40024   20679   863401    41.8 | 17.620 % |
c |    389999 |   90964   317137 |   44026   20829   864163    41.5 | 17.620 % |
c |    390225 |   90964   317137 |   48429   21055   865400    41.1 | 17.620 % |
c |    390562 |   90964   317137 |   53272   21392   867635    40.6 | 17.620 % |
c |    391068 |   90964   317137 |   58599   21898   871672    39.8 | 17.620 % |
c |    391827 |   90964   317137 |   64459   22657   875658    38.6 | 17.620 % |
c |    392966 |   90964   317137 |   70905   23796   885107    37.2 | 17.620 % |
c |    394674 |   90964   317137 |   77995   25504   918767    36.0 | 17.620 % |
c |    397236 |   90936   317039 |   85768   28064   936529    33.4 | 17.637 % |
c |    401080 |   90936   317039 |   94345   31908   970508    30.4 | 17.637 % |
c |    406846 |   90936   317039 |  103780   37674  1042610    27.7 | 17.637 % |
c |    415495 |   90870   316782 |  114075   46319  1318733    28.5 | 17.681 % |
c |    428470 |   90849   316710 |  125454   59287  1646037    27.8 | 17.692 % |
c ==============================================================================
c (current CPU-time: 700.779 s)
c ==============================================================================
c [1mFound solution: 1752642[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3940152   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    439223 |   90876   316913 |   27262   70039  2128055    30.4 | 17.692 % |
c   -- subsuming                       
c   -- var.elim.:  154/154          
c   -- var.elim.:  71/71          
c   -- var.elim.:  5/5          
c |    439223 |   90818   316719 |      --   70039       --      -- |     --   | -38/-8
c |    439223 |   90818   316719 |   36327   69686  2083508    29.9 | 17.692 % |
c |    439323 |   90818   316719 |   39959   21486   627604    29.2 | 17.781 % |
c |    439474 |   90818   316719 |   43955   21637   628310    29.0 | 17.781 % |
c |    439699 |   90818   316719 |   48351   21862   629907    28.8 | 17.781 % |
c |    440036 |   90818   316719 |   53186   22199   631824    28.5 | 17.781 % |
c |    440543 |   90818   316719 |   58505   22706   634610    27.9 | 17.781 % |
c |    441302 |   90818   316719 |   64355   23465   638788    27.2 | 17.781 % |
c |    442442 |   90818   316719 |   70791   24605   645480    26.2 | 17.781 % |
c |    444150 |   90818   316719 |   77870   26313   657164    25.0 | 17.781 % |
c |    446712 |   90794   316622 |   85635   28873   682651    23.6 | 17.798 % |
c |    450556 |   90743   316356 |   94145   32709   718969    22.0 | 17.826 % |
c |    456323 |   90743   316356 |  103560   38476   930645    24.2 | 17.826 % |
c |    464972 |   90743   316356 |  113916   47125  1680878    35.7 | 17.826 % |
c |    477949 |   90743   316356 |  125307   60102  1984674    33.0 | 17.826 % |
c |    497410 |   90743   316356 |  137838   79563  4060082    51.0 | 17.826 % |
c |    526604 |   90743   316356 |  151622  108757  5640924    51.9 | 17.826 % |
c |    570393 |   90743   316356 |  166784  152546  9466088    62.1 | 17.826 % |
c |    636078 |   90732   316319 |  183440   68438  3880919    56.7 | 17.832 % |
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 -X16#### 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.91 0.95 0.90 2/54 10454
Raw data (stat): 10454 (runsolver) R 10453 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541081481 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.0009 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 2666 0 0 0 991 7 0 0 25 0 1 0 541081481 11714560 2380 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2860 2380 603 41 0 2819 0
vsize: 11440
[startup+20.0014 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 3006 0 0 0 1990 9 0 0 25 0 1 0 541081481 13197312 2720 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3222 2720 603 41 0 3181 0
vsize: 12888
[startup+30.002 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 3891 0 0 0 2989 10 0 0 25 0 1 0 541081481 16818176 3605 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4106 3605 603 41 0 4065 0
vsize: 16424
[startup+40.0031 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 9327 0 0 0 3975 24 0 0 25 0 1 0 541081481 35385344 7837 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8639 7837 603 41 0 8598 0
vsize: 34556
[startup+50.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 9329 0 0 0 4976 24 0 0 25 0 1 0 541081481 35385344 7839 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8639 7839 603 41 0 8598 0
vsize: 34556
[startup+60.0035 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 10081 0 0 0 5973 26 0 0 25 0 1 0 541081481 36524032 8132 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8917 8132 603 41 0 8876 0
vsize: 35668
[startup+70.0043 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 10587 0 0 0 6971 27 0 0 25 0 1 0 541081481 36048896 8026 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8801 8026 603 41 0 8760 0
vsize: 35204
[startup+80.0047 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 11232 0 0 0 7969 30 0 0 25 0 1 0 541081481 35917824 7995 4294967295 134512640 134672761 3221224544 3221223728 134616011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8769 7995 603 41 0 8728 0
vsize: 35076
[startup+90.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 11777 0 0 0 8966 32 0 0 25 0 1 0 541081481 37187584 8232 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9079 8232 603 41 0 9038 0
vsize: 36316
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 11777 0 0 0 9967 32 0 0 25 0 1 0 541081481 37187584 8232 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9079 8232 603 41 0 9038 0
vsize: 36316
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 11777 0 0 0 10967 32 0 0 25 0 1 0 541081481 37187584 8232 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9079 8232 603 41 0 9038 0
vsize: 36316
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 11910 0 0 0 11966 32 0 0 25 0 1 0 541081481 37453824 8365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9144 8365 603 41 0 9103 0
vsize: 36576
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 12656 0 0 0 12964 35 0 0 25 0 1 0 541081481 40501248 9111 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9888 9111 603 41 0 9847 0
vsize: 39552
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 13608 0 0 0 13961 38 0 0 25 0 1 0 541081481 44605440 10063 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10890 10063 603 41 0 10849 0
vsize: 43560
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 14367 0 0 0 14960 40 0 0 25 0 1 0 541081481 47775744 10822 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11664 10822 603 41 0 11623 0
vsize: 46656
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 15391 0 0 0 15957 43 0 0 25 0 1 0 541081481 49401856 11256 4294967295 134512640 134672761 3221224544 3221220976 134523140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12061 11256 603 41 0 12020 0
vsize: 48244
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 15614 0 0 0 16956 43 0 0 25 0 1 0 541081481 49664000 11313 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12125 11313 603 41 0 12084 0
vsize: 48500
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 15614 0 0 0 17956 43 0 0 25 0 1 0 541081481 49664000 11313 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12125 11313 603 41 0 12084 0
vsize: 48500
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 15614 0 0 0 18956 43 0 0 25 0 1 0 541081481 49664000 11313 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12125 11313 603 41 0 12084 0
vsize: 48500
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 15614 0 0 0 19956 43 0 0 25 0 1 0 541081481 49664000 11313 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12125 11313 603 41 0 12084 0
vsize: 48500
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 15614 0 0 0 20956 43 0 0 25 0 1 0 541081481 49664000 11313 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12125 11313 603 41 0 12084 0
vsize: 48500
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 15614 0 0 0 21957 43 0 0 25 0 1 0 541081481 49664000 11313 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12125 11313 603 41 0 12084 0
vsize: 48500
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 15675 0 0 0 22957 43 0 0 25 0 1 0 541081481 49938432 11374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12192 11374 603 41 0 12151 0
vsize: 48768
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 16160 0 0 0 23955 45 0 0 25 0 1 0 541081481 51974144 11859 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12689 11859 603 41 0 12648 0
vsize: 50756
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 16717 0 0 0 24954 46 0 0 25 0 1 0 541081481 54222848 12416 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13238 12416 603 41 0 13197 0
vsize: 52952
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 17215 0 0 0 25954 47 0 0 25 0 1 0 541081481 56221696 12914 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13726 12914 603 41 0 13685 0
vsize: 54904
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 17625 0 0 0 26953 48 0 0 25 0 1 0 541081481 57982976 13324 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14156 13324 603 41 0 14115 0
vsize: 56624
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 18024 0 0 0 27951 50 0 0 25 0 1 0 541081481 59584512 13723 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14547 13723 603 41 0 14506 0
vsize: 58188
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 18363 0 0 0 28950 51 0 0 25 0 1 0 541081481 60903424 14062 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14869 14062 603 41 0 14828 0
vsize: 59476
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 18753 0 0 0 29950 52 0 0 25 0 1 0 541081481 62488576 14452 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15256 14452 603 41 0 15215 0
vsize: 61024
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 19013 0 0 0 30949 52 0 0 25 0 1 0 541081481 63565824 14712 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15519 14712 603 41 0 15478 0
vsize: 62076
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 19335 0 0 0 31948 54 0 0 25 0 1 0 541081481 64888832 15034 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15842 15034 603 41 0 15801 0
vsize: 63368
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 19665 0 0 0 32947 55 0 0 25 0 1 0 541081481 66224128 15364 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16168 15364 603 41 0 16127 0
vsize: 64672
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 19957 0 0 0 33946 56 0 0 25 0 1 0 541081481 67411968 15656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16458 15656 603 41 0 16417 0
vsize: 65832
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 20271 0 0 0 34945 57 0 0 25 0 1 0 541081481 69275648 15970 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16913 15970 603 41 0 16872 0
vsize: 67652
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 20574 0 0 0 35945 57 0 0 25 0 1 0 541081481 70471680 16273 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17205 16273 603 41 0 17164 0
vsize: 68820
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 20894 0 0 0 36944 58 0 0 25 0 1 0 541081481 71786496 16593 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17526 16594 603 41 0 17485 0
vsize: 70104
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 21204 0 0 0 37943 59 0 0 25 0 1 0 541081481 73134080 16903 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17855 16903 603 41 0 17814 0
vsize: 71420
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 21513 0 0 0 38942 61 0 0 25 0 1 0 541081481 74362880 17212 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17212 603 41 0 18114 0
vsize: 72620
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 21788 0 0 0 39942 61 0 0 25 0 1 0 541081481 75546624 17487 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18444 17487 603 41 0 18403 0
vsize: 73776
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 22047 0 0 0 40941 62 0 0 25 0 1 0 541081481 76619776 17746 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18706 17746 603 41 0 18665 0
vsize: 74824
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 22292 0 0 0 41941 63 0 0 25 0 1 0 541081481 77586432 17991 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18942 17991 603 41 0 18901 0
vsize: 75768
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 22698 0 0 0 42941 63 0 0 25 0 1 0 541081481 79192064 18397 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19334 18397 603 41 0 19293 0
vsize: 77336
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 22987 0 0 0 43940 64 0 0 25 0 1 0 541081481 80400384 18686 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19629 18686 603 41 0 19588 0
vsize: 78516
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 23367 0 0 0 44939 65 0 0 25 0 1 0 541081481 81981440 19066 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20015 19066 603 41 0 19974 0
vsize: 80060
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24008 0 0 0 45938 67 0 0 25 0 1 0 541081481 84602880 19707 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20655 19707 603 41 0 20614 0
vsize: 82620
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 46936 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 47937 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 48937 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 49937 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 50937 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 51937 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223648 134604352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 52938 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 53938 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 54938 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 55938 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 56938 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 57939 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 58939 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 59939 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 60939 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24596 0 0 0 61939 68 0 0 25 0 1 0 541081481 86503424 20093 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20093 603 41 0 21078 0
vsize: 84476
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 24598 0 0 0 62940 68 0 0 25 0 1 0 541081481 86503424 20095 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 20095 603 41 0 21078 0
vsize: 84476
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 25550 0 0 0 63936 71 0 0 25 0 1 0 541081481 86499328 20100 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20100 603 41 0 21077 0
vsize: 84472
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 25550 0 0 0 64937 71 0 0 25 0 1 0 541081481 86499328 20100 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20100 603 41 0 21077 0
vsize: 84472
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 25550 0 0 0 65937 71 0 0 25 0 1 0 541081481 86499328 20100 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20100 603 41 0 21077 0
vsize: 84472
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 25550 0 0 0 66937 71 0 0 25 0 1 0 541081481 86499328 20100 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20100 603 41 0 21077 0
vsize: 84472
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 25550 0 0 0 67937 71 0 0 25 0 1 0 541081481 86499328 20100 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20100 603 41 0 21077 0
vsize: 84472
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 25550 0 0 0 68937 71 0 0 25 0 1 0 541081481 86499328 20100 4294967295 134512640 134672761 3221224544 3221223688 134616247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20100 603 41 0 21077 0
vsize: 84472
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 25550 0 0 0 69937 71 0 0 25 0 1 0 541081481 86499328 20100 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20100 603 41 0 21077 0
vsize: 84472
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 70935 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 71936 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 72936 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 73936 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 74936 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 75936 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 76937 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 77937 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 78937 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+800.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 79937 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 80937 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 81938 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 82938 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 83938 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 84938 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 85938 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 86938 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 87939 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 88939 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 89939 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 90939 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+920.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 91939 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 92940 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 93940 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26032 0 0 0 94940 73 0 0 25 0 1 0 541081481 86499328 20103 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21118 20103 603 41 0 21077 0
vsize: 84472
[startup+960.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26499 0 0 0 95939 74 0 0 25 0 1 0 541081481 87597056 20371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20371 603 41 0 21345 0
vsize: 85544
[startup+970.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26499 0 0 0 96939 74 0 0 25 0 1 0 541081481 87597056 20371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20371 603 41 0 21345 0
vsize: 85544
[startup+980.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26499 0 0 0 97939 74 0 0 25 0 1 0 541081481 87597056 20371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20371 603 41 0 21345 0
vsize: 85544
[startup+990.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26499 0 0 0 98940 74 0 0 25 0 1 0 541081481 87597056 20371 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20371 603 41 0 21345 0
vsize: 85544
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26499 0 0 0 99940 74 0 0 25 0 1 0 541081481 87597056 20371 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20371 603 41 0 21345 0
vsize: 85544
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 100940 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 101940 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 102940 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 103941 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223584 134612851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 104941 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 105941 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 106941 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 107941 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 108941 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 109942 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 110942 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 111942 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 112942 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 113942 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 114942 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 115942 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 116943 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 117943 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26502 0 0 0 118943 74 0 0 25 0 1 0 541081481 87597056 20374 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 20374 603 41 0 21345 0
vsize: 85544
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10454
Raw data (stat): 10454 (minisat+) R 10453 18865 18864 0 -1 0 26829 0 0 0 119943 74 0 0 25 0 1 0 541081481 89047040 20701 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21740 20701 603 41 0 21699 0
vsize: 86960
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 10454
Raw data (stat): 10454 (minisat+) Z 10453 18865 18864 0 -1 12 26830 0 0 0 119943 78 0 0 25 0 1 0 541081481 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.09
CPU time (s): 1200.23
CPU user time (s): 1199.44
CPU system time (s): 0.78888
CPU usage (%): 100.011
Max. virtual memory (Kb): 86960
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####