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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-mkc.opb
MD5SUM	087a7cd0fdb8b0bf40fe6b459b39a663
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	2946
Biggest coefficient in the objective function	20000
Number of bits for the biggest coefficient in the objective function	15
Sum of the numbers in the objective function	31442101
Number of bits of the sum of numbers in the objective function	25
Biggest number in a constraint	67108864000
Number of bits of the biggest number in a constraint	36
Biggest sum of numbers in a constraint	138201238403
Number of bits of the biggest sum of numbers	38
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1230.15
Number of variables	5383
Total number of constraints	8734
Number of constraints which are clauses	2977
Number of constraints which are cardinality constraints (but not clauses)	5731
Number of constraints which are nor clauses,nor cardinality constraints	26
Minimum length of a constraint	1
Maximum length of a constraint	2952
Trace number 28222

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-05-25 01:33:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13612 boxname=wulflinc18 idbench=1048 idsolver=1 numberseed=0
MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef  /oldhome/oroussel/solvers/bsolo_lpr
MD5SUM BENCH:  087a7cd0fdb8b0bf40fe6b459b39a663  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-mkc.opb
REAL COMMAND:  bsolo_lpr /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-mkc.opb
IDLAUNCH: 13612
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        688236 kB
Buffers:          8116 kB
Cached:         307360 kB
SwapCached:        588 kB
Active:          26060 kB
Inactive:       294788 kB
HighTotal:      131008 kB
HighFree:         1344 kB
LowTotal:       903652 kB
LowFree:        686892 kB
SwapTotal:     2097892 kB
SwapFree:      2096632 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5660 kB
Slab:            19944 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 01:33:11 (client local time) WITH STATUS 0 IN 2.6096 SECONDS
stats: 13612 7 2.6096 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c ERROR Parsing file!!!
c ERROR parsing line: +1280000*x0000_bit0 +1920000*x0100_bit0 +1920000*x0300_bit0 +1280000*x0400_bit0 +1280000*x0500_bit0 +1280000*x0600_bit0 +1280000*x0700_bit0 +640000*x0800_bit0 +1536000*x0900_bit0 +1920000*x1000_bit0 +1280000*x1100_bit0 +640000*x1300_bit0 +1280000*x1400_bit0 +1280000*x1500_bit0 +640000*x1600_bit0 +640000*x1700_bit0 +1280000*x1800_bit0 +1280000*x1900_bit0 +921600*x2000_bit0 +1280000*x2200_bit0 +2560000*x2300_bit0 +1920000*x2400_bit0 +640000*x2500_bit0 +1280000*x2600_bit0 +1280000*x2700_bit0 +640000*x2800_bit0 +1280000*x2900_bit0 +640000*x3000_bit0 +1024000*x3100_bit0 +1920000*x3300_bit0 +1280000*x3400_bit0 +1152000*x3500_bit0 +1920000*x3600_bit0 +1920000*x3700_bit0 +1920000*x3800_bit0 +1536000*x3900_bit0 +640000*x4000_bit0 +1280000*x4100_bit0 +640000*x4200_bit0 +1920000*x4300_bit0 +1920000*x4400_bit0 +1280000*x4500_bit0 +1920000*x4600_bit0 +1152000*x4700_bit0 +640000*x4800_bit0 +1280000*x4900_bit0 +1280000*x5000_bit0 +640000*x5100_bit0 +1280000*x5200_bit0 +1920000*x5500_bit0 +1280000*x5600_bit0 +640000*x5700_bit0 +1920000*x5800_bit0 +1920000*x6000_bit0 +1920000*x6100_bit0 +640000*x6200_bit0 +640000*x6300_bit0 +640000*x6500_bit0 +1920000*x6600_bit0 +2560000*x6700_bit0 +1280000*x6800_bit0 +1280000*x6900_bit0 +2560000*x7000_bit0 +1280000*x7100_bit0 +1600000*x7200_bit0 +1536000*x7300_bit0 +1280000*x7400_bit0 +1280000*x7500_bit0 +2240000*x7700_bit0 +1920000*x7800_bit0 +640000*x7900_bit0 +1907200*x8000_bit0 +640000*x8100_bit0 +640000*x8300_bit0 +640000*x8400_bit0 +1280000*x8500_bit0 +1920000*x8600_bit0 +640000*x8700_bit0 +640000*x8800_bit0 +1280000*x9000_bit0 +1536000*x9100_bit0 +1139200*x9200_bit0 +1920000*x9300_bit0 +1920000*x9400_bit0 +678400*x9500_bit0 +1920000*x9600_bit0 +1280000*x9700_bit0 +1280000*x9800_bit0 +1920000*x10000_bit0 +2240000*x10200_bit0 +1280000*x10300_bit0 +2304000*x10500_bit0 +1280000*x10600_bit0 +1280000*x10700_bit0 +1753600*x10900_bit0 +921600*x11000_bit0 +1280000*x11300_bit0 +640000*x11400_bit0 +2304000*x11500_bit0 +640000*x11600_bit0 +1920000*x11700_bit0 +1792000*x11800_bit0 +1920000*x13000_bit0 +1920000*x13100_bit0 +2560000*x13200_bit0 +1920000*x13300_bit0 +2240000*x13500_bit0 +2240000*x13600_bit0 +1920000*x13700_bit0 +1280000*x13900_bit0 +1920000*x14200_bit0 +1920000*x14300_bit0 +2240000*x14400_bit0 +1920000*x14500_bit0 +2240000*x14600_bit0 +2240000*x14700_bit0 +2560000*x14800_bit0 +2560000*x14900_bit0 +640000*x15200_bit0 +1920000*x15300_bit0 +2240000*x15400_bit0 +2560000*x15500_bit0 +1920000*x15600_bit0 +640000*x15700_bit0 +2560000*x15800_bit0 +2560000*x15900_bit0 +1920000*x16000_bit0 +2560000*x16100_bit0 +1920000*x16200_bit0 +640000*x16300_bit0 +640000*x16400_bit0 +1907200*x16500_bit0 +640000*x16600_bit0 +1689600*x16700_bit0 +1075200*x16900_bit0 +1049600*x17000_bit0 +1036800*x17200_bit0 +1536000*x18000_bit0 +1075200*x18100_bit0 +1036800*x18200_bit0 +1075200*x18300_bit0 +1536000*x18400_bit0 +1036800*x19000_bit0 +1920000*x19100_bit0 +1036800*x19500_bit0 +1536000*x19600_bit0 +1024000*x23500_bit0 +1920000*x23600_bit0 +1920000*x23800_bit0 +1920000*x23900_bit0 +1830400*x24300_bit0 +691200*x24800_bit0 +512000*x24900_bit0 +1280000*x25100_bit0 +1280000*x25200_bit0 +1664000*x25300_bit0 +1920000*x25400_bit0 +1280000*x25500_bit0 +1920000*x25600_bit0 +1920000*x25700_bit0 +2560000*x25800_bit0 +2560000*x25900_bit0 +1664000*x26000_bit0 +1664000*x26100_bit0 +1190400*x26200_bit0 +1190400*x26300_bit0 +1190400*x26400_bit0 +1920000*x26500_bit0 +1920000*x26600_bit0 +1152000*x26700_bit0 +1152000*x26800_bit0 +1664000*x26900_bit0 +1152000*x27000_bit0 +1664000*x27100_bit0 +1152000*x27200_bit0 +1152000*x27300_bit0 +1152000*x27400_bit0 +1920000*x27500_bit0 +1920000*x27600_bit0 +1920000*x27700_bit0 +2560000*x27800_bit0 +2560000*x27900_bit0 +1152000*x28000_bit0 +1920000*x28200_bit0 +1920000*x28300_bit0 +1920000*x28400_bit0 +1920000*x28500_bit0 +1920000*x28600_bit0 +1920000*x28700_bit0 +1920000*x28800_bit0 +1920000*x29000_bit0 +1920000*x29100_bit0 +2560000*x29200_bit0 +1280000*x29300_bit0 +2176000*x29400_bit0 +1920000*x29500_bit0 +1920000*x29600_bit0 +1920000*x29700_bit0 +1856000*x29800_bit0 +1113600*x30000_bit0 +1920000*x30100_bit0 +499200*x30300_bit0 +1267200*x30400_bit0 +1267200*x30600_bit0 +1267200*x30700_bit0 +1267200*x30800_bit0 +1267200*x30900_bit0 +1267200*x31000_bit0 +1267200*x31100_bit0 +1267200*x31200_bit0 +1267200*x31300_bit0 +1267200*x31400_bit0 +1267200*x31500_bit0 +1395200*x31600_bit0 +1395200*x31700_bit0 +1267200*x31800_bit0 +1267200*x31900_bit0 +1267200*x32000_bit0 +1267200*x32100_bit0 +1267200*x32200_bit0 +1267200*x32300_bit0 +1267200*x32400_bit0 +1267200*x32500_bit0 +1267200*x32600_bit0 +1267200*x32700_bit0 +1267200*x32800_bit0 +1523200*x34800_bit0 +1523200*x34900_bit0 +1523200*x35000_bit0 +1523200*x35100_bit0 +1907200*x35200_bit0 +1907200*x35300_bit0 +372224*x35400_bit0 +363520*x35500_bit0 +1267200*x35600_bit0 +239616*x35700_bit0 +1523200*x35800_bit0 +239616*x35900_bit0 +1267200*x36000_bit0 +1049600*x36100_bit0 +716800*x36200_bit0 +1018880*x36500_bit0 +1273600*x36600_bit0 +1273600*x36700_bit0 +1273600*x36800_bit0 +1145600*x36900_bit0 +635520*x37000_bit0 +1273600*x37100_bit0 +1267200*x37300_bit0 +1267200*x37400_bit0 +1267200*x37500_bit0 +883200*x37600_bit0 +1267200*x39700_bit0 +1267200*x39900_bit0 +1267200*x40000_bit0 +1267200*x40100_bit0 +1267200*x40200_bit0 +1267200*x40300_bit0 +1267200*x40400_bit0 +1139200*x40500_bit0 +1139200*x40600_bit0 +1139200*x40700_bit0 +1139200*x40800_bit0 +1139200*x41100_bit0 +1267200*x41200_bit0 +436480*x41300_bit0 +603648*x41400_bit0 +592768*x41500_bit0 +947200*x41600_bit0 +614400*x41700_bit0 +1267200*x41800_bit0 +716800*x41900_bit0 +494208*x42000_bit0 +742400*x42100_bit0 +627200*x42200_bit0 +1273600*x42400_bit0 +1273600*x42500_bit0 +1529600*x42600_bit0 +1145600*x42700_bit0 +993280*x42800_bit0 +712960*x42900_bit0 +1273600*x43000_bit0 +1273600*x43100_bit0 +1273600*x43200_bit0 +1273600*x43300_bit0 +1273600*x43400_bit0 +1273600*x43500_bit0 +1145600*x43600_bit0 +1273600*x43700_bit0 +1273600*x43800_bit0 +1920000*x0101_bit0 +1920000*x0301_bit0 +1280000*x0401_bit0 +640000*x0801_bit0 +1280000*x1101_bit0 +1280000*x1501_bit0 +640000*x1601_bit0 +1280000*x1901_bit0 +921600*x2001_bit0 +1280000*x2201_bit0 +2560000*x2301_bit0 +1280000*x2901_bit0 +640000*x3001_bit0 +1280000*x3401_bit0 +1920000*x3801_bit0 +640000*x4001_bit0 +1280000*x4101_bit0 +1920000*x4401_bit0 +640000*x4801_bit0 +1280000*x5001_bit0 +640000*x5101_bit0 +1280000*x5201_bit0 +1920000*x5501_bit0 +1280000*x5601_bit0 +640000*x6501_bit0 +1920000*x6601_bit0 +1536000*x7301_bit0 +1280000*x7401_bit0 +2240000*x7701_bit0 +640000*x8301_bit0 +640000*x8401_bit0 +1280000*x9001_bit0 +1536000*x9101_bit0 +1139200*x9201_bit0 +678400*x9501_bit0 +1920000*x9601_bit0 +1920000*x10001_bit0 +2240000*x10201_bit0 +1280000*x10301_bit0 +2304000*x10501_bit0 +1280000*x10601_bit0 +1280000*x10701_bit0 +1753600*x10901_bit0 +1280000*x11301_bit0 +640000*x11401_bit0 +640000*x11601_bit0 +1920000*x11701_bit0 +1792000*x11801_bit0 +1920000*x13101_bit0 +1920000*x13301_bit0 +1920000*x13701_bit0 +1280000*x13901_bit0 +1920000*x14201_bit0 +1920000*x14301_bit0 +1920000*x14501_bit0 +640000*x15201_bit0 +1920000*x15301_bit0 +1920000*x15601_bit0 +1920000*x16001_bit0 +1920000*x16201_bit0 +1920000*x19101_bit0 +1920000*x23601_bit0 +1920000*x25601_bit0 +1190400*x26201_bit0 +1190400*x26301_bit0 +1190400*x26401_bit0 +1920000*x26601_bit0 +1152000*x26701_bit0 +1664000*x26901_bit0 +1152000*x27001_bit0 +1664000*x27101_bit0 +1152000*x27201_bit0 +1152000*x27301_bit0 +1152000*x27401_bit0 +1920000*x27501_bit0 +1920000*x27601_bit0 +1920000*x27701_bit0 +2560000*x27801_bit0 +2560000*x27901_bit0 +1920000*x28201_bit0 +1920000*x29101_bit0 +2560000*x29201_bit0 +2176000*x29401_bit0 +1920000*x29501_bit0 +1920000*x29601_bit0 +1920000*x29701_bit0 +1856000*x29801_bit0 +1920000*x30101_bit0 +499200*x30301_bit0 +1267200*x30401_bit0 +1267200*x30801_bit0 +1267200*x30901_bit0 +1267200*x31201_bit0 +1267200*x31301_bit0 +1267200*x31501_bit0 +1267200*x31801_bit0 +1267200*x32101_bit0 +1267200*x32201_bit0 +1267200*x32301_bit0 +1267200*x32401_bit0 +1267200*x32501_bit0 +1267200*x32601_bit0 +1267200*x32701_bit0 +1267200*x32801_bit0 +1907200*x35301_bit0 +363520*x35501_bit0 +1523200*x35801_bit0 +1049600*x36101_bit0 +716800*x36201_bit0 +1145600*x36901_bit0 +1267200*x37301_bit0 +1267200*x37401_bit0 +1267200*x37501_bit0 +883200*x37601_bit0 +1139200*x40501_bit0 +1139200*x40601_bit0 +1139200*x40701_bit0 +1139200*x40801_bit0 +1139200*x41101_bit0 +592768*x41501_bit0 +947200*x41601_bit0 +614400*x41701_bit0 +716800*x41901_bit0 +742400*x42101_bit0 +627200*x42201_bit0 +1273600*x42501_bit0 +1529600*x42601_bit0 +1273600*x43501_bit0 +1273600*x43701_bit0 +1920000*x0102_bit0 +1920000*x0302_bit0 +1280000*x0402_bit0 +640000*x0802_bit0 +1280000*x1102_bit0 +1920000*x1202_bit0 +1280000*x1502_bit0 +640000*x1602_bit0 +1280000*x1902_bit0 +921600*x2002_bit0 +1280000*x2202_bit0 +2560000*x2302_bit0 +1280000*x2902_bit0 +640000*x3002_bit0 +2112000*x3202_bit0 +1280000*x3402_bit0 +1920000*x3802_bit0 +640000*x4002_bit0 +1280000*x4102_bit0 +1920000*x4402_bit0 +640000*x4802_bit0 +1280000*x5002_bit0 +640000*x5102_bit0 +1280000*x5202_bit0 +1280000*x5302_bit0 +2112000*x5402_bit0 +1920000*x5502_bit0 +1280000*x5602_bit0 +640000*x6502_bit0 +1920000*x6602_bit0 +1536000*x7302_bit0 +1280000*x7402_bit0 +1920000*x7602_bit0 +2240000*x7702_bit0 +640000*x8302_bit0 +640000*x8402_bit0 +1280000*x9002_bit0 +1536000*x9102_bit0 +1139200*x9202_bit0 +678400*x9502_bit0 +1920000*x9602_bit0 +1920000*x10002_bit0 +1920000*x10102_bit0 +2240000*x10202_bit0 +1280000*x10302_bit0 +2304000*x10502_bit0 +1280000*x10802_bit0 +1753600*x10902_bit0 +1280000*x11202_bit0 +640000*x11402_bit0 +640000*x11602_bit0 +1920000*x11702_bit0 +1792000*x11802_bit0 +1920000*x12202_bit0 +1280000*x12902_bit0 +1920000*x13102_bit0 +1280000*x13902_bit0 +1920000*x14202_bit0 +1920000*x14302_bit0 +640000*x15202_bit0 +1920000*x15302_bit0 +1625600*x16802_bit0 +768000*x17102_bit0 +1536000*x17302_bit0 +1536000*x17402_bit0 +1536000*x17502_bit0 +1536000*x17602_bit0 +1536000*x17702_bit0 +1536000*x17802_bit0 +1536000*x17902_bit0 +1779200*x18502_bit0 +768000*x18602_bit0 +768000*x18702_bit0 +1536000*x18802_bit0 +1280000*x18902_bit0 +1920000*x19102_bit0 +896000*x19202_bit0 +768000*x19302_bit0 +1536000*x19402_bit0 +1280000*x19802_bit0 +1920000*x19902_bit0 +1920000*x20002_bit0 +1920000*x20202_bit0 +1280000*x20302_bit0 +1408000*x20502_bit0 +1280000*x20702_bit0 +1280000*x20902_bit0 +1280000*x21002_bit0 +1280000*x21302_bit0 +1280000*x21502_bit0 +1625600*x21802_bit0 +1779200*x21902_bit0 +768000*x22002_bit0 +1408000*x22102_bit0 +1344000*x22302_bit0 +1344000*x22402_bit0 +1344000*x22502_bit0 +1779200*x22702_bit0 +263296*x22902_bit0 +1600000*x23002_bit0 +1920000*x23602_bit0 +1536000*x24402_bit0 +1920000*x25602_bit0 +1190400*x26202_bit0 +1190400*x26302_bit0 +1190400*x26402_bit0 +1920000*x26602_bit0 +1152000*x26702_bit0 +1664000*x26902_bit0 +1152000*x27002_bit0 +1664000*x27102_bit0 +1152000*x27202_bit0 +1152000*x27302_bit0 +1152000*x27402_bit0 +1920000*x27502_bit0 +1920000*x27602_bit0 +1920000*x27702_bit0 +2560000*x27802_bit0 +2560000*x27902_bit0 +1920000*x28202_bit0 +1920000*x29102_bit0 +2560000*x29202_bit0 +2176000*x29402_bit0 +1920000*x29502_bit0 +1920000*x29602_bit0 +1920000*x29702_bit0 +1856000*x29802_bit0 +1920000*x30102_bit0 +768000*x30202_bit0 +499200*x30302_bit0 +1267200*x30402_bit0 +1267200*x30802_bit0 +1267200*x30902_bit0 +1267200*x31202_bit0 +1267200*x31302_bit0 +1267200*x31502_bit0 +1267200*x31802_bit0 +1267200*x32102_bit0 +1267200*x32202_bit0 +1267200*x32302_bit0 +1267200*x32402_bit0 +1267200*x32502_bit0 +1267200*x32602_bit0 +1267200*x32702_bit0 +1267200*x32802_bit0 +1273600*x33002_bit0 +1273600*x33102_bit0 +890880*x33302_bit0 +636160*x33402_bit0 +636160*x33602_bit0 +636160*x34002_bit0 +636160*x34202_bit0 +762880*x34502_bit0 +1907200*x35302_bit0 +363520*x35502_bit0 +1523200*x35802_bit0 +1049600*x36102_bit0 +716800*x36202_bit0 +244352*x36302_bit0 +1273600*x36402_bit0 +1267200*x37302_bit0 +1267200*x37402_bit0 +1267200*x37502_bit0 +883200*x37602_bit0 +636160*x37702_bit0 +636160*x37802_bit0 +1273600*x38102_bit0 +1273600*x38202_bit0 +636160*x38402_bit0 +636160*x38502_bit0 +1273600*x38802_bit0 +636160*x38902_bit0 +1273600*x39202_bit0 +1139200*x40502_bit0 +1139200*x40602_bit0 +1139200*x40702_bit0 +1139200*x40802_bit0 +1139200*x41102_bit0 +592768*x41502_bit0 +947200*x41602_bit0 +614400*x41702_bit0 +716800*x41902_bit0 +742400*x42102_bit0 +627200*x42202_bit0 +640000*x42302_bit0 +1273600*x42502_bit0 +1529600*x42602_bit0 +1273600*x43502_bit0 +1273600*x43702_bit0 +1920000*x0103_bit0 +1920000*x0303_bit0 +1280000*x0403_bit0 +640000*x0803_bit0 +1280000*x1103_bit0 +1920000*x1203_bit0 +1280000*x1503_bit0 +640000*x1603_bit0 +1280000*x1903_bit0 +921600*x2003_bit0 +1280000*x2203_bit0 +2560000*x2303_bit0 +1280000*x2903_bit0 +640000*x3003_bit0 +2112000*x3203_bit0 +1280000*x3403_bit0 +1920000*x3803_bit0 +640000*x4003_bit0 +1280000*x4103_bit0 +1920000*x4403_bit0 +640000*x4803_bit0 +1280000*x5003_bit0 +640000*x5103_bit0 +1280000*x5203_bit0 +1280000*x5303_bit0 +2112000*x5403_bit0 +1920000*x5503_bit0 +1280000*x5603_bit0 +640000*x6503_bit0 +1920000*x6603_bit0 +1536000*x7303_bit0 +1280000*x7403_bit0 +1920000*x7603_bit0 +2240000*x7703_bit0 +640000*x8303_bit0 +640000*x8403_bit0 +1280000*x9003_bit0 +1536000*x9103_bit0 +1139200*x9203_bit0 +678400*x9503_bit0 +1920000*x9603_bit0 +1920000*x10003_bit0 +1920000*x10103_bit0 +2240000*x10203_bit0 +1280000*x10303_bit0 +2304000*x10503_bit0 +1280000*x10803_bit0 +1753600*x10903_bit0 +1280000*x11203_bit0 +640000*x11403_bit0 +640000*x11603_bit0 +1920000*x11703_bit0 +1792000*x11803_bit0 +1920000*x12203_bit0 +1280000*x12903_bit0 +1920000*x13103_bit0 +1280000*x13903_bit0 +1920000*x14203_bit0 +1920000*x14303_bit0 +640000*x15203_bit0 +1920000*x15303_bit0 +1625600*x16803_bit0 +768000*x17103_bit0 +1536000*x17303_bit0 +1536000*x17403_bit0 +1536000*x17503_bit0 +1536000*x17603_bit0 +1536000*x17703_bit0 +1536000*x17803_bit0 +1536000*x17903_bit0 +1779200*x18503_bit0 +768000*x18603_bit0 +768000*x18703_bit0 +1536000*x18803_bit0 +1280000*x18903_bit0 +1920000*x19103_bit0 +896000*x19203_bit0 +768000*x19303_bit0 +1536000*x19403_bit0 +1280000*x19803_bit0 +1920000*x19903_bit0 +1920000*x20003_bit0 +1920000*x20203_bit0 +1280000*x20303_bit0 +1408000*x20503_bit0 +1280000*x20703_bit0 +1280000*x20903_bit0 +1280000*x21003_bit0 +1280000*x21303_bit0 +1280000*x21503_bit0 +1625600*x21803_bit0 +1779200*x21903_bit0 +768000*x22003_bit0 +1408000*x22103_bit0 +1344000*x22303_bit0 +1344000*x22403_bit0 +1344000*x22503_bit0 +1779200*x22703_bit0 +263296*x22903_bit0 +1600000*x23003_bit0 +1920000*x23603_bit0 +1536000*x24403_bit0 +1920000*x25603_bit0 +1190400*x26203_bit0 +1190400*x26303_bit0 +1190400*x26403_bit0 +1920000*x26603_bit0 +1152000*x26703_bit0 +1664000*x26903_bit0 +1152000*x27003_bit0 +1664000*x27103_bit0 +1152000*x27203_bit0 +1152000*x27303_bit0 +1152000*x27403_bit0 +1920000*x27503_bit0 +1920000*x27603_bit0 +1920000*x27703_bit0 +2560000*x27803_bit0 +2560000*x27903_bit0 +1920000*x28203_bit0 +1920000*x29103_bit0 +2560000*x29203_bit0 +2176000*x29403_bit0 +1920000*x29503_bit0 +1920000*x29603_bit0 +1920000*x29703_bit0 +1856000*x29803_bit0 +1920000*x30103_bit0 +768000*x30203_bit0 +499200*x30303_bit0 +1267200*x30403_bit0 +1267200*x30803_bit0 +1267200*x30903_bit0 +1267200*x31203_bit0 +1267200*x31303_bit0 +1267200*x31503_bit0 +1267200*x31803_bit0 +1267200*x32103_bit0 +1267200*x32203_bit0 +1267200*x32303_bit0 +1267200*x32403_bit0 +1267200*x32503_bit0 +1267200*x32603_bit0 +1267200*x32703_bit0 +1267200*x32803_bit0 +1273600*x33003_bit0 +1273600*x33103_bit0 +890880*x33303_bit0 +636160*x33403_bit0 +636160*x33603_bit0 +636160*x34003_bit0 +636160*x34203_bit0 +762880*x34503_bit0 +1907200*x35303_bit0 +363520*x35503_bit0 +1523200*x35803_bit0 +1049600*x36103_bit0 +716800*x36203_bit0 +244352*x36303_bit0 +1273600*x36403_bit0 +1267200*x37303_bit0 +1267200*x37403_bit0 +1267200*x37503_bit0 +883200*x37603_bit0 +636160*x37703_bit0 +636160*x37803_bit0 +1273600*x38103_bit0 +1273600*x38203_bit0 +636160*x38403_bit0 +636160*x38503_bit0 +1273600*x38803_bit0 +636160*x38903_bit0 +1273600*x39203_bit0 +1139200*x40503_bit0 +1139200*x40603_bit0 +1139200*x40703_bit0 +1139200*x40803_bit0 +1139200*x41103_bit0 +592768*x41503_bit0 +947200*x41603_bit0 +614400*x41703_bit0 +716800*x41903_bit0 +742400*x42103_bit0 +627200*x42203_bit0 +640000*x42303_bit0 +1273600*x42503_bit0 +1529600*x42603_bit0 +1273600*x43503_bit0 +1273600*x43703_bit0 +1920000*x0104_bit0 +1920000*x0304_bit0 +1280000*x0404_bit0 +1280000*x0704_bit0 +1920000*x1004_bit0 +1280000*x1104_bit0 +1920000*x1204_bit0 +1280000*x1504_bit0 +1280000*x1904_bit0 +921600*x2004_bit0 +1280000*x2204_bit0 +2560000*x2304_bit0 +1280000*x2904_bit0 +640000*x3004_bit0 +1280000*x3404_bit0 +1920000*x3804_bit0 +1536000*x3904_bit0 +640000*x4004_bit0 +1280000*x4104_bit0 +1920000*x4404_bit0 +1152000*x4704_bit0 +640000*x4804_bit0 +1280000*x5004_bit0 +640000*x5104_bit0 +1280000*x5204_bit0 +1280000*x5604_bit0 +1920000*x5804_bit0 +640000*x6504_bit0 +1920000*x6604_bit0 +1280000*x6904_bit0 +1536000*x7304_bit0 +1280000*x7404_bit0 +1280000*x7504_bit0 +1920000*x7604_bit0 +2240000*x7704_bit0 +640000*x8304_bit0 +1280000*x8504_bit0 +1920000*x8604_bit0 +1280000*x9004_bit0 +1536000*x9104_bit0 +1139200*x9204_bit0 +678400*x9504_bit0 +1920000*x9604_bit0 +1280000*x9704_bit0 +1280000*x9804_bit0 +2240000*x10204_bit0 +1280000*x10304_bit0 +2304000*x10504_bit0 +1280000*x10804_bit0 +1753600*x10904_bit0 +1280000*x11204_bit0 +640000*x11404_bit0 +640000*x11604_bit0 +1920000*x11704_bit0 +1792000*x11804_bit0 +1920000*x12204_bit0 +1280000*x12904_bit0 +1280000*x13904_bit0 +1920000*x14204_bit0 +1920000*x14304_bit0 +640000*x15204_bit0 +1920000*x15304_bit0 +640000*x16604_bit0 +1689600*x16704_bit0 +1625600*x16804_bit0 +768000*x17104_bit0 +1536000*x17304_bit0 +1536000*x17404_bit0 +1536000*x17504_bit0 +1536000*x17604_bit0 +1536000*x17704_bit0 +1536000*x17804_bit0 +1536000*x17904_bit0 +1779200*x18504_bit0 +768000*x18604_bit0 +768000*x18704_bit0 +1536000*x18804_bit0 +1280000*x18904_bit0 +1920000*x19104_bit0 +896000*x19204_bit0 +768000*x19304_bit0 +1536000*x19404_bit0 +1280000*x19804_bit0 +1920000*x19904_bit0 +1920000*x20004_bit0 +1920000*x20204_bit0 +1280000*x20304_bit0 +1408000*x20504_bit0 +1280000*x20704_bit0 +1280000*x20904_bit0 +1280000*x21004_bit0 +1280000*x21304_bit0 +1280000*x21504_bit0 +1625600*x21804_bit0 +1779200*x21904_bit0 +768000*x22004_bit0 +1408000*x22104_bit0 +1344000*x22304_bit0 +1344000*x22404_bit0 +1344000*x22504_bit0 +1779200*x22704_bit0 +263296*x22904_bit0 +1600000*x23004_bit0 +1920000*x23604_bit0 +1920000*x23904_bit0 +1536000*x24404_bit0 +1664000*x25304_bit0 +1920000*x25404_bit0 +1920000*x25604_bit0 +1920000*x25704_bit0 +2560000*x25804_bit0 +2560000*x25904_bit0 +1664000*x26004_bit0 +1664000*x26104_bit0 +1190400*x26204_bit0 +1190400*x26304_bit0 +1190400*x26404_bit0 +1920000*x26504_bit0 +1920000*x26604_bit0 +1152000*x26704_bit0 +1664000*x26904_bit0 +1152000*x27004_bit0 +1664000*x27104_bit0 +1152000*x27204_bit0 +1152000*x27304_bit0 +1152000*x27404_bit0 +1920000*x27504_bit0 +1920000*x27604_bit0 +1920000*x27704_bit0 +2560000*x27804_bit0 +2560000*x27904_bit0 +1920000*x28204_bit0 +1920000*x28304_bit0 +1920000*x28404_bit0 +1920000*x28504_bit0 +1920000*x28604_bit0 +1920000*x28704_bit0 +1920000*x28804_bit0 +1920000*x29004_bit0 +1920000*x29104_bit0 +2560000*x29204_bit0 +2176000*x29404_bit0 +1920000*x29504_bit0 +1920000*x29604_bit0 +1920000*x29704_bit0 +1856000*x29804_bit0 +1920000*x30104_bit0 +768000*x30204_bit0 +499200*x30304_bit0 +1267200*x30404_bit0 +1267200*x30804_bit0 +1267200*x30904_bit0 +1267200*x31204_bit0 +1267200*x31304_bit0 +1267200*x31404_bit0 +1267200*x31504_bit0 +1267200*x32104_bit0 +1267200*x32204_bit0 +1267200*x32304_bit0 +1267200*x32404_bit0 +1267200*x32504_bit0 +1267200*x32604_bit0 +1267200*x32704_bit0 +1267200*x32804_bit0 +1273600*x33004_bit0 +1273600*x33104_bit0 +890880*x33304_bit0 +636160*x33404_bit0 +636160*x33604_bit0 +636160*x34004_bit0 +636160*x34204_bit0 +762880*x34504_bit0 +1907200*x35304_bit0 +363520*x35504_bit0 +1049600*x36104_bit0 +716800*x36204_bit0 +1267200*x37304_bit0 +1267200*x37404_bit0 +1267200*x37504_bit0 +883200*x37604_bit0 +636160*x37704_bit0 +636160*x37804_bit0 +1273600*x38104_bit0 +1273600*x38204_bit0 +636160*x38404_bit0 +636160*x38504_bit0 +1273600*x38804_bit0 +636160*x38904_bit0 +1273600*x39204_bit0 +1139200*x40504_bit0 +1139200*x40604_bit0 +1139200*x40704_bit0 +1139200*x40804_bit0 +592768*x41504_bit0 +947200*x41604_bit0 +614400*x41704_bit0 +716800*x41904_bit0 +627200*x42204_bit0 +640000*x42304_bit0 +1529600*x42604_bit0 +1920000*x0105_bit0 +1920000*x0305_bit0 +1280000*x0405_bit0 +640000*x0805_bit0 +1280000*x1105_bit0 +1920000*x1205_bit0 +1280000*x1505_bit0 +640000*x1605_bit0 +1280000*x1905_bit0 +921600*x2005_bit0 +1280000*x2205_bit0 +2560000*x2305_bit0 +1280000*x2905_bit0 +640000*x3005_bit0 +2112000*x3205_bit0 +1280000*x3405_bit0 +1920000*x3805_bit0 +640000*x4005_bit0 +1280000*x4105_bit0 +1920000*x4405_bit0 +640000*x4805_bit0 +1280000*x5005_bit0 +640000*x5105_bit0 +1280000*x5205_bit0 +1280000*x5305_bit0 +2112000*x5405_bit0 +1920000*x5505_bit0 +1280000*x5605_bit0 +640000*x6505_bit0 +1920000*x6605_bit0 +1536000*x7305_bit0 +1280000*x7405_bit0 +1920000*x7605_bit0 +2240000*x7705_bit0 +640000*x8305_bit0 +640000*x8405_bit0 +1280000*x9005_bit0 +1536000*x9105_bit0 +1139200*x9205_bit0 +678400*x9505_bit0 +1920000*x9605_bit0 +1920000*x10005_bit0 +1920000*x10105_bit0 +2240000*x10205_bit0 +1280000*x10305_bit0 +2304000*x10505_bit0 +1280000*x10805_bit0 +1753600*x10905_bit0 +1280000*x11205_bit0 +640000*x11405_bit0 +640000*x11605_bit0 +1920000*x11705_bit0 +1792000*x11805_bit0 +1920000*x12205_bit0 +1280000*x12905_bit0 +1920000*x13105_bit0 +1280000*x13905_bit0 +1920000*x14205_bit0 +1920000*x14305_bit0 +640000*x15205_bit0 +1920000*x15305_bit0 +1625600*x16805_bit0 +768000*x17105_bit0 +1536000*x17305_bit0 +1536000*x17405_bit0 +1536000*x17505_bit0 +1536000*x17605_bit0 +1536000*x17705_bit0 +1536000*x17805_bit0 +1536000*x17905_bit0 +1779200*x18505_bit0 +768000*x18605_bit0 +768000*x18705_bit0 +1536000*x18805_bit0 +1280000*x18905_bit0 +1920000*x19105_bit0 +896000*x19205_bit0 +768000*x19305_bit0 +1536000*x19405_bit0 +1280000*x19805_bit0 +1920000*x19905_bit0 +1920000*x20005_bit0 +1920000*x20205_bit0 +1280000*x20305_bit0 +1408000*x20505_bit0 +1280000*x20705_bit0 +1280000*x20905_bit0 +1280000*x21005_bit0 +1280000*x21305_bit0 +1280000*x21505_bit0 +1625600*x21805_bit0 +1779200*x21905_bit0 +768000*x22005_bit0 +1408000*x22105_bit0 +1344000*x22305_bit0 +1344000*x22405_bit0 +1344000*x22505_bit0 +1779200*x22705_bit0 +263296*x22905_bit0 +1600000*x23005_bit0 +1920000*x23605_bit0 +1536000*x24405_bit0 +1920000*x25605_bit0 +1190400*x26205_bit0 +1190400*x26305_bit0 +1190400*x26405_bit0 +1920000*x26605_bit0 +1152000*x26705_bit0 +1664000*x26905_bit0 +1152000*x27005_bit0 +1664000*x27105_bit0 +1152000*x27205_bit0 +1152000*x27305_bit0 +1152000*x27405_bit0 +1920000*x27505_bit0 +1920000*x27605_bit0 +1920000*x27705_bit0 +2560000*x27805_bit0 +2560000*x27905_bit0 +1920000*x28205_bit0 +1920000*x29105_bit0 +2560000*x29205_bit0 +2176000*x29405_bit0 +1920000*x29505_bit0 +1920000*x29605_bit0 +1920000*x29705_bit0 +1856000*x29805_bit0 +1920000*x30105_bit0 +768000*x30205_bit0 +499200*x30305_bit0 +1267200*x30405_bit0 +1267200*x30805_bit0 +1267200*x30905_bit0 +1267200*x31205_bit0 +1267200*x31305_bit0 +1267200*x31505_bit0 +1267200*x31805_bit0 +1267200*x32105_bit0 +1267200*x32205_bit0 +1267200*x32305_bit0 +1267200*x32405_bit0 +1267200*x32505_bit0 +1267200*x32605_bit0 +1267200*x32705_bit0 +1267200*x32805_bit0 +1273600*x33005_bit0 +1273600*x33105_bit0 +890880*x33305_bit0 +636160*x33405_bit0 +636160*x33605_bit0 +636160*x34005_bit0 +636160*x34205_bit0 +762880*x34505_bit0 +1907200*x35305_bit0 +363520*x35505_bit0 +1523200*x35805_bit0 +1049600*x36105_bit0 +716800*x36205_bit0 +244352*x36305_bit0 +1273600*x36405_bit0 +1267200*x37305_bit0 +1267200*x37405_bit0 +1267200*x37505_bit0 +883200*x37605_bit0 +636160*x37705_bit0 +636160*x37805_bit0 +1273600*x38105_bit0 +1273600*x38205_bit0 +636160*x38405_bit0 +636160*x38505_bit0 +1273600*x38805_bit0 +636160*x38905_bit0 +1273600*x39205_bit0 +1139200*x40505_bit0 +1139200*x40605_bit0 +1139200*x40705_bit0 +1139200*x40805_bit0 +1139200*x41105_bit0 +592768*x41505_bit0 +947200*x41605_bit0 +614400*x41705_bit0 +716800*x41905_bit0 +742400*x42105_bit0 +627200*x42205_bit0 +640000*x42305_bit0 +1273600*x42505_bit0 +1529600*x42605_bit0 +1273600*x43505_bit0 +1273600*x43705_bit0 +1920000*x0106_bit0 +1920000*x0306_bit0 +1280000*x0406_bit0 +640000*x0806_bit0 +1280000*x1106_bit0 +1920000*x1206_bit0 +1280000*x1506_bit0 +640000*x1606_bit0 +1280000*x1906_bit0 +921600*x2006_bit0 +1280000*x2206_bit0 +2560000*x2306_bit0 +1280000*x2906_bit0 +640000*x3006_bit0 +2112000*x3206_bit0 +1280000*x3406_bit0 +1920000*x3806_bit0 +640000*x4006_bit0 +1280000*x4106_bit0 +1920000*x4406_bit0 +640000*x4806_bit0 +1280000*x5006_bit0 +640000*x5106_bit0 +1280000*x5206_bit0 +1280000*x5306_bit0 +2112000*x5406_bit0 +1920000*x5506_bit0 +1280000*x5606_bit0 +640000*x6506_bit0 +1920000*x6606_bit0 +1536000*x7306_bit0 +1280000*x7406_bit0 +1920000*x7606_bit0 +2240000*x7706_bit0 +640000*x8306_bit0 +640000*x8406_bit0 +1280000*x9006_bit0 +1536000*x9106_bit0 +1139200*x9206_bit0 +678400*x9506_bit0 +1920000*x9606_bit0 +1920000*x10006_bit0 +1920000*x10106_bit0 +2240000*x10206_bit0 +1280000*x10306_bit0 +2304000*x10506_bit0 +1280000*x10806_bit0 +1753600*x10906_bit0 +1280000*x11206_bit0 +640000*x11406_bit0 +640000*x11606_bit0 +1920000*x11706_bit0 +1792000*x11806_bit0 +1920000*x12206_bit0 +1280000*x12906_bit0 +1920000*x13106_bit0 +1280000*x13906_bit0 +1920000*x14206_bit0 +1920000*x14306_bit0 +640000*x15206_bit0 +1920000*x15306_bit0 +1625600*x16806_bit0 +768000*x17106_bit0 +1536000*x17306_bit0 +1536000*x17406_bit0 +1536000*x17506_bit0 +1536000*x17606_bit0 +1536000*x17706_bit0 +1536000*x17806_bit0 +1536000*x17906_bit0 +1779200*x18506_bit0 +768000*x18606_bit0 +768000*x18706_bit0 +1536000*x18806_bit0 +1280000*x18906_bit0 +1920000*x19106_bit0 +896000*x19206_bit0 +768000*x19306_bit0 +1536000*x19406_bit0 +1280000*x19806_bit0 +1920000*x19906_bit0 +1920000*x20006_bit0 +1920000*x20206_bit0 +1280000*x20306_bit0 +1408000*x20506_bit0 +1280000*x20706_bit0 +1280000*x20906_bit0 +1280000*x21006_bit0 +1280000*x21306_bit0 +1280000*x21506_bit0 +1625600*x21806_bit0 +1779200*x21906_bit0 +768000*x22006_bit0 +1408000*x22106_bit0 +1344000*x22306_bit0 +1344000*x22406_bit0 +1344000*x22506_bit0 +1779200*x22706_bit0 +263296*x22906_bit0 +1600000*x23006_bit0 +1920000*x23606_bit0 +1536000*x24406_bit0 +1920000*x25606_bit0 +1190400*x26206_bit0 +1190400*x26306_bit0 +1190400*x26406_bit0 +1920000*x26606_bit0 +1152000*x26706_bit0 +1664000*x26906_bit0 +1152000*x27006_bit0 +1664000*x27106_bit0 +1152000*x27206_bit0 +1152000*x27306_bit0 +1152000*x27406_bit0 +1920000*x27506_bit0 +1920000*x27606_bit0 +1920000*x27706_bit0 +2560000*x27806_bit0 +2560000*x27906_bit0 +1920000*x28206_bit0 +1920000*x29106_bit0 +2560000*x29206_bit0 +2176000*x29406_bit0 +1920000*x29506_bit0 +1920000*x29606_bit0 +1920000*x29706_bit0 +1856000*x29806_bit0 +1920000*x30106_bit0 +768000*x30206_bit0 +499200*x30306_bit0 +1267200*x30406_bit0 +1267200*x30806_bit0 +1267200*x30906_bit0 +1267200*x31206_bit0 +1267200*x31306_bit0 +1267200*x31506_bit0 +1267200*x31806_bit0 +1267200*x32106_bit0 +1267200*x32206_bit0 +1267200*x32306_bit0 +1267200*x32406_bit0 +1267200*x32506_bit0 +1267200*x32606_bit0 +1267200*x32706_bit0 +1267200*x32806_bit0 +1273600*x33006_bit0 +1273600*x33106_bit0 +890880*x33306_bit0 +636160*x33406_bit0 +636160*x33606_bit0 +636160*x34006_bit0 +636160*x34206_bit0 +762880*x34506_bit0 +1907200*x35306_bit0 +363520*x35506_bit0 +1523200*x35806_bit0 +1049600*x36106_bit0 +716800*x36206_bit0 +244352*x36306_bit0 +1273600*x36406_bit0 +1267200*x37306_bit0 +1267200*x37406_bit0 +1267200*x37506_bit0 +883200*x37606_bit0 +636160*x37706_bit0 +636160*x37806_bit0 +1273600*x38106_bit0 +1273600*x38206_bit0 +636160*x38406_bit0 +636160*x38506_bit0 +1273600*x38806_bit0 +636160*x38906_bit0 +1273600*x39206_bit0 +1139200*x40506_bit0 +1139200*x40606_bit0 +1139200*x40706_bit0 +1139200*x40806_bit0 +1139200*x41106_bit0 +592768*x41506_bit0 +947200*x41606_bit0 +614400*x41706_bit0 +716800*x41906_bit0 +742400*x42106_bit0 +627200*x42206_bit0 +640000*x42306_bit0 +1273600*x42506_bit0 +1529600*x42606_bit0 +1273600*x43506_bit0 +1273600*x43706_bit0 +1920000*x0107_bit0 +1920000*x0307_bit0 +1280000*x0407_bit0 +640000*x0807_bit0 +1280000*x1107_bit0 +1920000*x1207_bit0 +1280000*x1507_bit0 +640000*x1607_bit0 +1280000*x1907_bit0 +921600*x2007_bit0 +1280000*x2207_bit0 +2560000*x2307_bit0 +1280000*x2907_bit0 +640000*x3007_bit0 +2112000*x3207_bit0 +1280000*x3407_bit0 +1920000*x3807_bit0 +640000*x4007_bit0 +1280000*x4107_bit0 +1920000*x4407_bit0 +640000*x4807_bit0 +1280000*x5007_bit0 +640000*x5107_bit0 +1280000*x5207_bit0 +1280000*x5307_bit0 +2112000*x5407_bit0 +1920000*x5507_bit0 +1280000*x5607_bit0 +640000*x6507_bit0 +1920000*x6607_bit0 +1536000*x7307_bit0 +1280000*x7407_bit0 +1920000*x7607_bit0 +2240000*x7707_bit0 +640000*x8307_bit0 +640000*x8407_bit0 +1280000*x9007_bit0 +1536000*x9107_bit0 +1139200*x9207_bit0 +678400*x9507_bit0 +1920000*x9607_bit0 +1920000*x10007_bit0 +1920000*x10107_bit0 +2240000*x10207_bit0 +1280000*x10307_bit0 +2304000*x10507_bit0 +1280000*x10807_bit0 +1753600*x10907_bit0 +1280000*x11207_bit0 +640000*x11407_bit0 +640000*x11607_bit0 +1920000*x11707_bit0 +1792000*x11807_bit0 +1920000*x12207_bit0 +1280000*x12907_bit0 +1920000*x13107_bit0 +1280000*x13907_bit0 +1920000*x14207_bit0 +1920000*x14307_bit0 +640000*x15207_bit0 +1920000*x15307_bit0 +1625600*x16807_bit0 +768000*x17107_bit0 +1536000*x17307_bit0 +1536000*x17407_bit0 +1536000*x17507_bit0 +1536000*x17607_bit0 +1536000*x17707_bit0 +1536000*x17807_bit0 +1536000*x17907_bit0 +1779200*x18507_bit0 +768000*x18607_bit0 +768000*x18707_bit0 +1536000*x18807_bit0 +1280000*x18907_bit0 +1920000*x19107_bit0 +896000*x19207_bit0 +768000*x19307_bit0 +1536000*x19407_bit0 +1280000*x19807_bit0 +1920000*x19907_bit0 +1920000*x20007_bit0 +1920000*x20207_bit0 +1280000*x20307_bit0 +1408000*x20507_bit0 +1280000*x20707_bit0 +1280000*x20907_bit0 +1280000*x21007_bit0 +1280000*x21307_bit0 +1280000*x21507_bit0 +1625600*x21807_bit0 +1779200*x21907_bit0 +768000*x22007_bit0 +1408000*x22107_bit0 +1344000*x22307_bit0 +1344000*x22407_bit0 +1344000*x22507_bit0 +1779200*x22707_bit0 +263296*x22907_bit0 +1600000*x23007_bit0 +1920000*x23607_bit0 +1536000*x24407_bit0 +1920000*x25607_bit0 +1190400*x26207_bit0 +1190400*x26307_bit0 +1190400*x26407_bit0 +1920000*x26607_bit0 +1152000*x26707_bit0 +1664000*x26907_bit0 +1152000*x27007_bit0 +1664000*x27107_bit0 +1152000*x27207_bit0 +1152000*x27307_bit0 +1152000*x27407_bit0 +1920000*x27507_bit0 +1920000*x27607_bit0 +1920000*x27707_bit0 +2560000*x27807_bit0 +2560000*x27907_bit0 +1920000*x28207_bit0 +1920000*x29107_bit0 +2560000*x29207_bit0 +2176000*x29407_bit0 +1920000*x29507_bit0 +1920000*x29607_bit0 +1920000*x29707_bit0 +1856000*x29807_bit0 +1920000*x30107_bit0 +768000*x30207_bit0 +499200*x30307_bit0 +1267200*x30407_bit0 +1267200*x30807_bit0 +1267200*x30907_bit0 +1267200*x31207_bit0 +1267200*x31307_bit0 +1267200*x31507_bit0 +1267200*x31807_bit0 +1267200*x32107_bit0 +1267200*x32207_bit0 +1267200*x32307_bit0 +1267200*x32407_bit0 +1267200*x32507_bit0 +1267200*x32607_bit0 +1267200*x32707_bit0 +1267200*x32807_bit0 +1273600*x33007_bit0 +1273600*x33107_bit0 +890880*x33307_bit0 +636160*x33407_bit0 +636160*x33607_bit0 +636160*x34007_bit0 +636160*x34207_bit0 +762880*x34507_bit0 +1907200*x35307_bit0 +363520*x35507_bit0 +1523200*x35807_bit0 +1049600*x36107_bit0 +716800*x36207_bit0 +244352*x36307_bit0 +1273600*x36407_bit0 +1267200*x37307_bit0 +1267200*x37407_bit0 +1267200*x37507_bit0 +883200*x37607_bit0 +636160*x37707_bit0 +636160*x37807_bit0 +1273600*x38107_bit0 +1273600*x38207_bit0 +636160*x38407_bit0 +636160*x38507_bit0 +1273600*x38807_bit0 +636160*x38907_bit0 +1273600*x39207_bit0 +1139200*x40507_bit0 +1139200*x40607_bit0 +1139200*x40707_bit0 +1139200*x40807_bit0 +1139200*x41107_bit0 +592768*x41507_bit0 +947200*x41607_bit0 +614400*x41707_bit0 +716800*x41907_bit0 +742400*x42107_bit0 +627200*x42207_bit0 +640000*x42307_bit0 +1273600*x42507_bit0 +1529600*x42607_bit0 +1273600*x43507_bit0 +1273600*x43707_bit0 +1920000*x0108_bit0 +1920000*x0308_bit0 +1280000*x0708_bit0 +1920000*x1008_bit0 +1280000*x1108_bit0 +640000*x1308_bit0 +1280000*x1508_bit0 +1280000*x1908_bit0 +921600*x2008_bit0 +1280000*x2208_bit0 +640000*x3008_bit0 +1280000*x3408_bit0 +1920000*x3608_bit0 +1920000*x3808_bit0 +1536000*x3908_bit0 +640000*x4008_bit0 +1280000*x4108_bit0 +1920000*x4408_bit0 +640000*x4808_bit0 +1280000*x5008_bit0 +1280000*x5608_bit0 +1920000*x5808_bit0 +832000*x5908_bit0 +640000*x6208_bit0 +640000*x6508_bit0 +1280000*x6908_bit0 +1536000*x7308_bit0 +1280000*x7408_bit0 +1280000*x7508_bit0 +640000*x8108_bit0 +640000*x8308_bit0 +1280000*x8508_bit0 +1920000*x8608_bit0 +640000*x8708_bit0 +640000*x8808_bit0 +1920000*x9308_bit0 +1920000*x9408_bit0 +678400*x9508_bit0 +1920000*x9608_bit0 +1280000*x9708_bit0 +1280000*x9808_bit0 +1280000*x10308_bit0 +819200*x10408_bit0 +2304000*x10508_bit0 +1280000*x10808_bit0 +1753600*x10908_bit0 +1280000*x11208_bit0 +640000*x11408_bit0 +640000*x11608_bit0 +1920000*x11708_bit0 +1792000*x11808_bit0 +1920000*x12108_bit0 +1920000*x12208_bit0 +1920000*x12308_bit0 +1920000*x12408_bit0 +1920000*x12508_bit0 +1920000*x12608_bit0 +1920000*x12708_bit0 +1920000*x12808_bit0 +1280000*x12908_bit0 +1280000*x13908_bit0 +640000*x16408_bit0 +640000*x16608_bit0 +1689600*x16708_bit0 +1625600*x16808_bit0 +768000*x17108_bit0 +1536000*x17308_bit0 +1536000*x17408_bit0 +1536000*x17508_bit0 +1536000*x17608_bit0 +1536000*x17708_bit0 +1536000*x17808_bit0 +1536000*x17908_bit0 +1779200*x18508_bit0 +768000*x18608_bit0 +768000*x18708_bit0 +1536000*x18808_bit0 +1280000*x18908_bit0 +1920000*x19108_bit0 +896000*x19208_bit0 +768000*x19308_bit0 +1536000*x19408_bit0 +1664000*x19708_bit0 +1280000*x19808_bit0 +1920000*x19908_bit0 +1920000*x20008_bit0 +1280000*x20108_bit0 +1920000*x20208_bit0 +1280000*x20308_bit0 +1280000*x20408_bit0 +1408000*x20508_bit0 +1280000*x20708_bit0 +1280000*x20908_bit0 +1280000*x21008_bit0 +1280000*x21308_bit0 +1280000*x21508_bit0 +1664000*x21708_bit0 +1625600*x21808_bit0 +1779200*x21908_bit0 +768000*x22008_bit0 +1408000*x22108_bit0 +1344000*x22308_bit0 +1344000*x22408_bit0 +1344000*x22508_bit0 +1779200*x22708_bit0 +1920000*x22808_bit0 +263296*x22908_bit0 +1600000*x23008_bit0 +1920000*x23108_bit0 +1024000*x23508_bit0 +1920000*x23608_bit0 +1920000*x23908_bit0 +1280000*x24208_bit0 +1536000*x24408_bit0 +1664000*x25308_bit0 +1920000*x25408_bit0 +1920000*x25608_bit0 +1920000*x25708_bit0 +2560000*x25808_bit0 +2560000*x25908_bit0 +1664000*x26008_bit0 +1664000*x26108_bit0 +1190400*x26208_bit0 +1190400*x26308_bit0 +1190400*x26408_bit0 +1920000*x26508_bit0 +1920000*x26608_bit0 +1152000*x26708_bit0 +1664000*x26908_bit0 +1152000*x27008_bit0 +1664000*x27108_bit0 +1152000*x27208_bit0 +1152000*x27308_bit0 +1152000*x27408_bit0 +1920000*x27508_bit0 +1920000*x27608_bit0 +1920000*x27708_bit0 +2560000*x27808_bit0 +2560000*x27908_bit0 +1920000*x28108_bit0 +1920000*x28208_bit0 +1920000*x28308_bit0 +1920000*x28408_bit0 +1920000*x28508_bit0 +1920000*x28608_bit0 +1920000*x28708_bit0 +1920000*x28808_bit0 +1920000*x29008_bit0 +1920000*x29108_bit0 +2176000*x29408_bit0 +1920000*x29508_bit0 +1920000*x29608_bit0 +1920000*x29708_bit0 +1856000*x29808_bit0 +1920000*x29908_bit0 +1920000*x30108_bit0 +768000*x30208_bit0 +499200*x30308_bit0 +1267200*x30408_bit0 +1267200*x30808_bit0 +1267200*x30908_bit0 +1267200*x31208_bit0 +1267200*x31308_bit0 +1267200*x31408_bit0 +1267200*x31508_bit0 +1267200*x32108_bit0 +1267200*x32208_bit0 +1267200*x32308_bit0 +1267200*x32408_bit0 +1267200*x32508_bit0 +1267200*x32608_bit0 +1267200*x32708_bit0 +636160*x32908_bit0 +1273600*x33008_bit0 +1273600*x33108_bit0 +890880*x33308_bit0 +636160*x33408_bit0 +636160*x33508_bit0 +636160*x33608_bit0 +636160*x33708_bit0 +636160*x33808_bit0 +636160*x34008_bit0 +636160*x34208_bit0 +762880*x34508_bit0 +372224*x35408_bit0 +363520*x35508_bit0 +1267200*x35608_bit0 +1049600*x36108_bit0 +1280000*x37208_bit0 +1267200*x37308_bit0 +1267200*x37408_bit0 +1267200*x37508_bit0 +883200*x37608_bit0 +636160*x37708_bit0 +636160*x37808_bit0 +636160*x37908_bit0 +636160*x38008_bit0 +1273600*x38108_bit0 +1273600*x38208_bit0 +636160*x38408_bit0 +636160*x38508_bit0 +636160*x38608_bit0 +1273600*x38808_bit0 +636160*x38908_bit0 +1273600*x39208_bit0 +1267200*x39708_bit0 +1267200*x40108_bit0 +1139200*x40608_bit0 +1139200*x40708_bit0 +592768*x41508_bit0 +947200*x41608_bit0 +614400*x41708_bit0 +627200*x42208_bit0 +640000*x42308_bit0 +1920000*x0109_bit0 +1920000*x0309_bit0 +1280000*x0409_bit0 +1280000*x0709_bit0 +1920000*x1009_bit0 +1280000*x1109_bit0 +1920000*x1209_bit0 +640000*x1309_bit0 +1280000*x1509_bit0 +1280000*x1909_bit0 +921600*x2009_bit0 +1280000*x2209_bit0 +2560000*x2309_bit0 +1280000*x2909_bit0 +640000*x3009_bit0 +1280000*x3409_bit0 +1920000*x3609_bit0 +1920000*x3809_bit0 +1536000*x3909_bit0 +640000*x4009_bit0 +1280000*x4109_bit0 +1920000*x4409_bit0 +1152000*x4709_bit0 +640000*x4809_bit0 +1280000*x5009_bit0 +640000*x5109_bit0 +1280000*x5209_bit0 +1280000*x5609_bit0 +1920000*x5809_bit0 +640000*x6209_bit0 +640000*x6509_bit0 +1920000*x6609_bit0 +1280000*x6909_bit0 +1536000*x7309_bit0 +1280000*x7409_bit0 +1280000*x7509_bit0 +1920000*x7609_bit0 +2240000*x7709_bit0 +640000*x8109_bit0 +640000*x8309_bit0 +1280000*x8509_bit0 +1920000*x8609_bit0 +640000*x8709_bit0 +640000*x8809_bit0 +1280000*x9009_bit0 +1536000*x9109_bit0 +1139200*x9209_bit0 +1920000*x9309_bit0 +1920000*x9409_bit0 +678400*x9509_bit0 +1920000*x9609_bit0 +1280000*x9709_bit0 +1280000*x9809_bit0 +2240000*x10209_bit0 +1280000*x10309_bit0 +2304000*x10509_bit0 +1280000*x10809_bit0 +1753600*x10909_bit0 +1280000*x11209_bit0 +640000*x11409_bit0 +640000*x11609_bit0 +1920000*x11709_bit0 +1792000*x11809_bit0 +1920000*x12109_bit0 +1920000*x12209_bit0 +1920000*x12309_bit0 +1920000*x12409_bit0 +1920000*x12509_bit0 +1920000*x12609_bit0 +1920000*x12709_bit0 +1920000*x12809_bit0 +1280000*x12909_bit0 +1280000*x13909_bit0 +1920000*x14209_bit0 +1920000*x14309_bit0 +640000*x15209_bit0 +1920000*x15309_bit0 +640000*x16409_bit0 +640000*x16609_bit0 +1689600*x16709_bit0 +1625600*x16809_bit0 +768000*x17109_bit0 +1536000*x17309_bit0 +1536000*x17409_bit0 +1536000*x17509_bit0 +1536000*x17609_bit0 +1536000*x17709_bit0 +1536000*x17809_bit0 +1536000*x17909_bit0 +1779200*x18509_bit0 +768000*x18609_bit0 +768000*x18709_bit0 +1536000*x18809_bit0 +1280000*x18909_bit0 +1920000*x19109_bit0 +896000*x19209_bit0 +768000*x19309_bit0 +1536000*x19409_bit0 +1664000*x19709_bit0 +1280000*x19809_bit0 +1920000*x19909_bit0 +1920000*x20009_bit0 +1920000*x20209_bit0 +1280000*x20309_bit0 +1408000*x20509_bit0 +1280000*x20709_bit0 +1280000*x20909_bit0 +1280000*x21009_bit0 +1280000*x21309_bit0 +1280000*x21509_bit0 +1664000*x21709_bit0 +1625600*x21809_bit0 +1779200*x21909_bit0 +768000*x22009_bit0 +1408000*x22109_bit0 +1344000*x22309_bit0 +1344000*x22409_bit0 +1344000*x22509_bit0 +1779200*x22709_bit0 +263296*x22909_bit0 +1600000*x23009_bit0 +1024000*x23509_bit0 +1920000*x23609_bit0 +1920000*x23909_bit0 +1280000*x24209_bit0 +1536000*x24409_bit0 +1664000*x25309_bit0 +1920000*x25409_bit0 +1920000*x25609_bit0 +1920000*x25709_bit0 +2560000*x25809_bit0 +2560000*x25909_bit0 +1664000*x26009_bit0 +1664000*x26109_bit0 +1190400*x26209_bit0 +1190400*x26309_bit0 +1190400*x26409_bit0 +1920000*x26509_bit0 +1920000*x26609_bit0 +1152000*x26709_bit0 +1664000*x26909_bit0 +1152000*x27009_bit0 +1664000*x27109_bit0 +1152000*x27209_bit0 +1152000*x27309_bit0 +1152000*x27409_bit0 +1920000*x27509_bit0 +1920000*x27609_bit0 +1920000*x27709_bit0 +2560000*x27809_bit0 +2560000*x27909_bit0 +1920000*x28209_bit0 +1920000*x28309_bit0 +1920000*x28409_bit0 +1920000*x28509_bit0 +1920000*x28609_bit0 +1920000*x28709_bit0 +1920000*x28809_bit0 +1920000*x29009_bit0 +1920000*x29109_bit0 +2560000*x29209_bit0 +2176000*x29409_bit0 +1920000*x29509_bit0 +1920000*x29609_bit0 +1920000*x29709_bit0 +1856000*x29809_bit0 +1920000*x30109_bit0 +768000*x30209_bit0 +499200*x30309_bit0 +1267200*x30409_bit0 +1267200*x30809_bit0 +1267200*x30909_bit0 +1267200*x31209_bit0 +1267200*x31309_bit0 +1267200*x31409_bit0 +1267200*x31509_bit0 +1267200*x32109_bit0 +1267200*x32209_bit0 +1267200*x32309_bit0 +1267200*x32409_bit0 +1267200*x32509_bit0 +1267200*x32609_bit0 +1267200*x32709_bit0 +1267200*x32809_bit0 +1273600*x33009_bit0 +1273600*x33109_bit0 +890880*x33309_bit0 +636160*x33409_bit0 +636160*x33609_bit0 +636160*x34009_bit0 +636160*x34209_bit0 +762880*x34509_bit0 +1907200*x35309_bit0 +372224*x35409_bit0 +363520*x35509_bit0 +1267200*x35609_bit0 +1049600*x36109_bit0 +716800*x36209_bit0 +1267200*x37309_bit0 +1267200*x37409_bit0 +1267200*x37509_bit0 +883200*x37609_bit0 +636160*x37709_bit0 +636160*x37809_bit0 +1273600*x38109_bit0 +1273600*x38209_bit0 +636160*x38409_bit0 +636160*x38509_bit0 +1273600*x38809_bit0 +636160*x38909_bit0 +1273600*x39209_bit0 +1267200*x39709_bit0 +1267200*x39909_bit0 +1267200*x40009_bit0 +1267200*x40109_bit0 +1139200*x40509_bit0 +1139200*x40609_bit0 +1139200*x40709_bit0 +1139200*x40809_bit0 +592768*x41509_bit0 +947200*x41609_bit0 +614400*x41709_bit0 +716800*x41909_bit0 +627200*x42209_bit0 +640000*x42309_bit0 +1529600*x42609_bit0 +1920000*x0110_bit0 +640000*x0210_bit0 +1920000*x0310_bit0 +1280000*x0710_bit0 +1920000*x1010_bit0 +1280000*x1110_bit0 +1280000*x1510_bit0 +1280000*x1910_bit0 +921600*x2010_bit0 +1280000*x2110_bit0 +1280000*x2210_bit0 +640000*x3010_bit0 +1280000*x3410_bit0 +1920000*x3810_bit0 +1536000*x3910_bit0 +640000*x4010_bit0 +1280000*x4110_bit0 +1920000*x4410_bit0 +640000*x4810_bit0 +1280000*x5010_bit0 +1280000*x5610_bit0 +1920000*x5810_bit0 +896000*x6410_bit0 +640000*x6510_bit0 +1280000*x6910_bit0 +1536000*x7310_bit0 +1280000*x7410_bit0 +1280000*x7510_bit0 +1881600*x8210_bit0 +640000*x8310_bit0 +1280000*x8510_bit0 +1920000*x8610_bit0 +678400*x9510_bit0 +1920000*x9610_bit0 +1280000*x9710_bit0 +1280000*x9810_bit0 +640000*x9910_bit0 +1280000*x10310_bit0 +2304000*x10510_bit0 +1280000*x10810_bit0 +1753600*x10910_bit0 +1920000*x11110_bit0 +1280000*x11210_bit0 +640000*x11410_bit0 +640000*x11610_bit0 +1920000*x11710_bit0 +1792000*x11810_bit0 +1920000*x11910_bit0 +1561600*x12010_bit0 +1920000*x12210_bit0 +1280000*x12910_bit0 +1280000*x13410_bit0 +1804800*x13810_bit0 +1280000*x13910_bit0 +896000*x15010_bit0 +640000*x15210_bit0 +640000*x16610_bit0 +1689600*x16710_bit0 +1625600*x16810_bit0 +768000*x17110_bit0 +1536000*x17310_bit0 +1536000*x17410_bit0 +1536000*x17510_bit0 +1536000*x17610_bit0 +1536000*x17710_bit0 +1536000*x17810_bit0 +1536000*x17910_bit0 +1779200*x18510_bit0 +768000*x18610_bit0 +768000*x18710_bit0 +1536000*x18810_bit0 +1280000*x18910_bit0 +1920000*x19110_bit0 +896000*x19210_bit0 +768000*x19310_bit0 +1536000*x19410_bit0 +1280000*x19810_bit0 +1920000*x19910_bit0 +1408000*x20510_bit0 +768000*x20610_bit0 +1280000*x20710_bit0 +1280000*x20810_bit0 +1280000*x20910_bit0 +1280000*x21010_bit0 +1280000*x21110_bit0 +1280000*x21210_bit0 +1280000*x21310_bit0 +768000*x21410_bit0 +1280000*x21510_bit0 +1280000*x21610_bit0 +1625600*x21810_bit0 +1779200*x21910_bit0 +1408000*x22110_bit0 +1280000*x22210_bit0 +1408000*x22610_bit0 +1779200*x22710_bit0 +263296*x22910_bit0 +1600000*x23010_bit0 +1689600*x23210_bit0 +1459200*x23310_bit0 +1267200*x23410_bit0 +1920000*x23610_bit0 +1894400*x23710_bit0 +1920000*x23910_bit0 +1536000*x24410_bit0 +1664000*x25310_bit0 +1920000*x25410_bit0 +1920000*x25610_bit0 +1920000*x25710_bit0 +2560000*x25810_bit0 +2560000*x25910_bit0 +1664000*x26010_bit0 +1664000*x26110_bit0 +1190400*x26210_bit0 +1190400*x26310_bit0 +1190400*x26410_bit0 +1920000*x26510_bit0 +1920000*x26610_bit0 +1152000*x26710_bit0 +1664000*x26910_bit0 +1152000*x27010_bit0 +1664000*x27110_bit0 +1152000*x27210_bit0 +1152000*x27310_bit0 +1152000*x27410_bit0 +1920000*x27510_bit0 +1920000*x27610_bit0 +1920000*x27710_bit0 +2560000*x27810_bit0 +2560000*x27910_bit0 +1920000*x28210_bit0 +1920000*x28310_bit0 +1920000*x28410_bit0 +1920000*x28510_bit0 +1920000*x28610_bit0 +1920000*x28710_bit0 +1920000*x28810_bit0 +1843200*x28910_bit0 +1920000*x29010_bit0 +1920000*x29110_bit0 +2176000*x29410_bit0 +1920000*x29510_bit0 +1920000*x29610_bit0 +1920000*x29710_bit0 +1856000*x29810_bit0 +1920000*x30110_bit0 +768000*x30210_bit0 +499200*x30310_bit0 +1267200*x30410_bit0 +1267200*x30510_bit0 +1267200*x30810_bit0 +1267200*x30910_bit0 +1267200*x31210_bit0 +1267200*x31310_bit0 +1267200*x31410_bit0 +1267200*x31510_bit0 +1267200*x32110_bit0 +1267200*x32210_bit0 +1267200*x32310_bit0 +1267200*x32410_bit0 +1267200*x32510_bit0 +1267200*x32610_bit0 +1267200*x32710_bit0 +1273600*x33010_bit0 +1273600*x33110_bit0 +1273600*x33210_bit0 +636160*x33410_bit0 +636160*x33610_bit0 +1273600*x33910_bit0 +636160*x34110_bit0 +636160*x34210_bit0 +1273600*x34310_bit0 +1273600*x34410_bit0 +762880*x34510_bit0 +363520*x35510_bit0 +1049600*x36110_bit0 +1267200*x37310_bit0 +1267200*x37410_bit0 +1267200*x37510_bit0 +883200*x37610_bit0 +636160*x37810_bit0 +1273600*x38110_bit0 +1273600*x38210_bit0 +1273600*x38310_bit0 +636160*x38410_bit0 +636160*x38510_bit0 +1273600*x38710_bit0 +1273600*x38810_bit0 +635520*x39010_bit0 +1273600*x39110_bit0 +1273600*x39210_bit0 +1139200*x40610_bit0 +1139200*x40710_bit0 +592768*x41510_bit0 +947200*x41610_bit0 +614400*x41710_bit0 +627200*x42210_bit0 +640000*x42310_bit0 +1920000*x0311_bit0 +1280000*x0411_bit0 +1280000*x1111_bit0 +1920000*x1211_bit0 +1280000*x1511_bit0 +1280000*x1911_bit0 +921600*x2011_bit0 +2560000*x2311_bit0 +1280000*x2911_bit0 +640000*x3011_bit0 +1280000*x3411_bit0 +1920000*x3811_bit0 +640000*x4011_bit0 +1920000*x4411_bit0 +640000*x4811_bit0 +1280000*x5011_bit0 +640000*x5111_bit0 +1280000*x5211_bit0 +1280000*x5611_bit0 +640000*x6511_bit0 +1920000*x6611_bit0 +1536000*x7311_bit0 +1280000*x7411_bit0 +1920000*x7611_bit0 +2240000*x7711_bit0 +640000*x8311_bit0 +1280000*x9011_bit0 +1536000*x9111_bit0 +1139200*x9211_bit0 +678400*x9511_bit0 +1920000*x9611_bit0 +2240000*x10211_bit0 +2304000*x10511_bit0 +1280000*x10811_bit0 +1280000*x11211_bit0 +640000*x11411_bit0 +640000*x11611_bit0 +1920000*x11711_bit0 +1792000*x11811_bit0 +1280000*x12911_bit0 +1280000*x13911_bit0 +1920000*x14211_bit0 +1920000*x14311_bit0 +640000*x15211_bit0 +1920000*x15311_bit0 +768000*x17111_bit0 +1536000*x17311_bit0 +1536000*x17411_bit0 +1536000*x17511_bit0 +1536000*x17611_bit0 +1536000*x17711_bit0 +1536000*x17811_bit0 +1536000*x17911_bit0 +1779200*x18511_bit0 +768000*x18611_bit0 +768000*x18711_bit0 +1536000*x18811_bit0 +1280000*x18911_bit0 +1920000*x19111_bit0 +896000*x19211_bit0 +768000*x19311_bit0 +1536000*x19411_bit0 +1920000*x20011_bit0 +1920000*x20211_bit0 +1280000*x20311_bit0 +1408000*x20511_bit0 +1280000*x20711_bit0 +1280000*x20911_bit0 +1280000*x21011_bit0 +1280000*x21511_bit0 +1779200*x21911_bit0 +768000*x22011_bit0 +1408000*x22111_bit0 +1344000*x22311_bit0 +1344000*x22411_bit0 +1344000*x22511_bit0 +1779200*x22711_bit0 +263296*x22911_bit0 +1536000*x24411_bit0 +1664000*x26911_bit0 +1152000*x27011_bit0 +1664000*x27111_bit0 +1152000*x27211_bit0 +1152000*x27311_bit0 +1152000*x27411_bit0 +1920000*x28211_bit0 +1920000*x29111_bit0 +2560000*x29211_bit0 +2176000*x29411_bit0 +1920000*x29711_bit0 +1856000*x29811_bit0 +1920000*x30111_bit0 +768000*x30211_bit0 +499200*x30311_bit0 +1267200*x30411_bit0 +1267200*x30811_bit0 +1267200*x30911_bit0 +1267200*x31211_bit0 +1267200*x31311_bit0 +1267200*x32111_bit0 +1267200*x32211_bit0 +1267200*x32311_bit0 +1267200*x32411_bit0 +1267200*x32511_bit0 +1267200*x32611_bit0 +1267200*x32711_bit0 +1267200*x32811_bit0 +1273600*x33011_bit0 +1273600*x33111_bit0 +890880*x33311_bit0 +636160*x33411_bit0 +636160*x33611_bit0 +636160*x34011_bit0 +636160*x34211_bit0 +762880*x34511_bit0 +1907200*x35311_bit0 +1049600*x36111_bit0 +716800*x36211_bit0 +1267200*x37311_bit0 +1267200*x37411_bit0 +1267200*x37511_bit0 +883200*x37611_bit0 +636160*x37711_bit0 +636160*x37811_bit0 +1273600*x38111_bit0 +1273600*x38211_bit0 +636160*x38411_bit0 +636160*x38511_bit0 +1273600*x38811_bit0 +636160*x38911_bit0 +1139200*x40511_bit0 +1139200*x40611_bit0 +1139200*x40711_bit0 +1139200*x40811_bit0 +592768*x41511_bit0 +614400*x41711_bit0 +716800*x41911_bit0 +627200*x42211_bit0 +640000*x42311_bit0 +1529600*x42611_bit0 +1920000*x0312_bit0 +1280000*x0412_bit0 +1280000*x0712_bit0 +1920000*x1012_bit0 +1280000*x1112_bit0 +1920000*x1212_bit0 +640000*x1312_bit0 +1280000*x1512_bit0 +1280000*x1912_bit0 +921600*x2012_bit0 +2560000*x2312_bit0 +1280000*x2912_bit0 +640000*x3012_bit0 +1280000*x3412_bit0 +1920000*x3612_bit0 +1920000*x3812_bit0 +1536000*x3912_bit0 +640000*x4012_bit0 +1920000*x4412_bit0 +1152000*x4712_bit0 +640000*x4812_bit0 +1280000*x5012_bit0 +640000*x5112_bit0 +1280000*x5212_bit0 +1280000*x5612_bit0 +1920000*x5812_bit0 +640000*x6212_bit0 +640000*x6512_bit0 +1920000*x6612_bit0 +2560000*x6712_bit0 +1280000*x6912_bit0 +1536000*x7312_bit0 +1280000*x7412_bit0 +1280000*x7512_bit0 +1920000*x7612_bit0 +2240000*x7712_bit0 +640000*x8112_bit0 +640000*x8312_bit0 +640000*x8712_bit0 +640000*x8812_bit0 +1280000*x9012_bit0 +1536000*x9112_bit0 +1139200*x9212_bit0 +1920000*x9312_bit0 +1920000*x9412_bit0 +678400*x9512_bit0 +1920000*x9612_bit0 +1280000*x9712_bit0 +1280000*x9812_bit0 +2240000*x10212_bit0 +2304000*x10512_bit0 +1280000*x10812_bit0 +1280000*x11212_bit0 +640000*x11412_bit0 +640000*x11612_bit0 +1920000*x11712_bit0 +1792000*x11812_bit0 +1920000*x12112_bit0 +1920000*x12412_bit0 +1920000*x12512_bit0 +1920000*x12712_bit0 +1920000*x12812_bit0 +1280000*x12912_bit0 +1280000*x13912_bit0 +1920000*x14212_bit0 +1920000*x14312_bit0 +640000*x15212_bit0 +1920000*x15312_bit0 +640000*x16412_bit0 +640000*x16612_bit0 +768000*x17112_bit0 +1536000*x17312_bit0 +1536000*x17412_bit0 +1536000*x17712_bit0 +1536000*x17812_bit0 +1536000*x17912_bit0 +1779200*x18512_bit0 +768000*x18712_bit0 +1536000*x18812_bit0 +1280000*x18912_bit0 +1920000*x19112_bit0 +896000*x19212_bit0 +1536000*x19412_bit0 +1664000*x19712_bit0 +1920000*x20012_bit0 +1920000*x20212_bit0 +1280000*x20312_bit0 +1408000*x20512_bit0 +1280000*x20712_bit0 +1280000*x20912_bit0 +1280000*x21012_bit0 +1280000*x21512_bit0 +1664000*x21712_bit0 +1779200*x21912_bit0 +768000*x22012_bit0 +1408000*x22112_bit0 +1344000*x22312_bit0 +1344000*x22412_bit0 +1344000*x22512_bit0 +1779200*x22712_bit0 +263296*x22912_bit0 +1920000*x23912_bit0 +1280000*x24212_bit0 +1664000*x25312_bit0 +1920000*x25412_bit0 +1664000*x26912_bit0 +1152000*x27012_bit0 +1664000*x27112_bit0 +1152000*x27212_bit0 +1152000*x27312_bit0 +1152000*x27412_bit0 +1920000*x28212_bit0 +1920000*x28312_bit0 +1920000*x28712_bit0 +1920000*x28812_bit0 +1920000*x29112_bit0 +2560000*x29212_bit0 +2176000*x29412_bit0 +1920000*x29712_bit0 +1856000*x29812_bit0 +1920000*x30112_bit0 +768000*x30212_bit0 +499200*x30312_bit0 +1267200*x30412_bit0 +1267200*x30912_bit0 +1267200*x31312_bit0 +1267200*x31412_bit0 +1267200*x32112_bit0 +1267200*x32212_bit0 +1267200*x32312_bit0 +1267200*x32412_bit0 +1267200*x32512_bit0 +1267200*x32612_bit0 +1267200*x32712_bit0 +1267200*x32812_bit0 +1273600*x33012_bit0 +1273600*x33112_bit0 +890880*x33312_bit0 +636160*x33412_bit0 +636160*x33612_bit0 +636160*x34012_bit0 +636160*x34212_bit0 +762880*x34512_bit0 +1907200*x35312_bit0 +1049600*x36112_bit0 +716800*x36212_bit0 +1267200*x37312_bit0 +1267200*x37412_bit0 +1267200*x37512_bit0 +883200*x37612_bit0 +636160*x37712_bit0 +636160*x37812_bit0 +1273600*x38112_bit0 +1273600*x38212_bit0 +636160*x38412_bit0 +636160*x38512_bit0 +636160*x38912_bit0 +1267200*x39912_bit0 +1267200*x40012_bit0 +1267200*x40112_bit0 +1139200*x40512_bit0 +1139200*x40612_bit0 +1139200*x40812_bit0 +592768*x41512_bit0 +614400*x41712_bit0 +716800*x41912_bit0 +742400*x42112_bit0 +627200*x42212_bit0 +640000*x42312_bit0 +1529600*x42612_bit0 +1280000*x0413_bit0 +1280000*x0613_bit0 +1280000*x0713_bit0 +1920000*x1013_bit0 +1280000*x1413_bit0 +1280000*x1513_bit0 +921600*x2013_bit0 +2560000*x2313_bit0 +1920000*x2413_bit0 +1280000*x2613_bit0 +1280000*x2713_bit0 +640000*x2813_bit0 +1024000*x3113_bit0 +1152000*x3513_bit0 +1920000*x3713_bit0 +1920000*x3813_bit0 +1536000*x3913_bit0 +640000*x4013_bit0 +1920000*x4313_bit0 +1280000*x4513_bit0 +1920000*x4613_bit0 +1152000*x4713_bit0 +640000*x4813_bit0 +1280000*x4913_bit0 +1280000*x5013_bit0 +1280000*x5213_bit0 +1920000*x5813_bit0 +1920000*x6013_bit0 +1920000*x6113_bit0 +640000*x6313_bit0 +640000*x6513_bit0 +1920000*x6613_bit0 +1280000*x6913_bit0 +1536000*x7313_bit0 +2240000*x7713_bit0 +1920000*x7813_bit0 +640000*x8313_bit0 +1280000*x9013_bit0 +1536000*x9113_bit0 +1139200*x9213_bit0 +678400*x9513_bit0 +1920000*x9613_bit0 +1280000*x9713_bit0 +2240000*x10213_bit0 +921600*x11013_bit0 +640000*x11413_bit0 +640000*x11613_bit0 +1920000*x11713_bit0 +1792000*x11813_bit0 +2240000*x13513_bit0 +2240000*x13613_bit0 +1920000*x14213_bit0 +1920000*x14313_bit0 +2240000*x14413_bit0 +640000*x15213_bit0 +1920000*x15313_bit0 +2560000*x15813_bit0 +2560000*x16113_bit0 +640000*x16613_bit0 +1036800*x17213_bit0 +1036800*x19513_bit0 +896000*x24513_bit0 +768000*x24613_bit0 +768000*x24713_bit0 +896000*x25013_bit0 +1664000*x25313_bit0 +1152000*x26813_bit0 +1664000*x26913_bit0 +1152000*x27013_bit0 +1664000*x27113_bit0 +1152000*x27213_bit0 +1152000*x27313_bit0 +1152000*x28013_bit0 +1920000*x28813_bit0 +2560000*x29213_bit0 +2176000*x29413_bit0 +1920000*x29713_bit0 +1920000*x30113_bit0 +499200*x30313_bit0 +1267200*x31013_bit0 +1267200*x31413_bit0 +1395200*x31613_bit0 +1395200*x31713_bit0 +1267200*x32013_bit0 +1267200*x32113_bit0 +1267200*x32213_bit0 +1267200*x32313_bit0 +1267200*x32413_bit0 +1267200*x32613_bit0 +1267200*x32713_bit0 +1267200*x32813_bit0 +1024000*x34613_bit0 +1024000*x34713_bit0 +1523200*x34813_bit0 +1523200*x35013_bit0 +1907200*x35313_bit0 +1267200*x36013_bit0 +1018880*x36513_bit0 +1273600*x36613_bit0 +1273600*x36713_bit0 +1273600*x36813_bit0 +1267200*x37313_bit0 +1267200*x37413_bit0 +1267200*x37513_bit0 +883200*x37613_bit0 +1024000*x39313_bit0 +896000*x39413_bit0 +896000*x39513_bit0 +896000*x39613_bit0 +1267200*x39813_bit0 +1267200*x40113_bit0 +1139200*x40513_bit0 +1139200*x40913_bit0 +1139200*x41013_bit0 +436480*x41313_bit0 +614400*x41713_bit0 +627200*x42213_bit0 +1529600*x42613_bit0 +1145600*x42713_bit0 +712960*x42913_bit0 +1273600*x43013_bit0 +1273600*x43113_bit0 +1273600*x43213_bit0 +1273600*x43313_bit0 +1273600*x43413_bit0 +1280000*x0414_bit0 +640000*x0814_bit0 +1920000*x1214_bit0 +1280000*x1514_bit0 +640000*x1614_bit0 +921600*x2014_bit0 +2560000*x2314_bit0 +1280000*x2914_bit0 +2112000*x3214_bit0 +1920000*x3814_bit0 +640000*x4014_bit0 +640000*x4814_bit0 +1280000*x5014_bit0 +640000*x5114_bit0 +1280000*x5214_bit0 +1280000*x5314_bit0 +2112000*x5414_bit0 +1920000*x5514_bit0 +640000*x6514_bit0 +1920000*x6614_bit0 +1920000*x7614_bit0 +2240000*x7714_bit0 +640000*x8314_bit0 +640000*x8414_bit0 +1280000*x9014_bit0 +1536000*x9114_bit0 +1139200*x9214_bit0 +678400*x9514_bit0 +1920000*x9614_bit0 +1920000*x10014_bit0 +1920000*x10114_bit0 +2240000*x10214_bit0 +1280000*x11214_bit0 +640000*x11414_bit0 +640000*x11614_bit0 +1920000*x11714_bit0 +1792000*x11814_bit0 +1280000*x12914_bit0 +1920000*x13114_bit0 +1920000*x14214_bit0 +1920000*x14314_bit0 +640000*x15214_bit0 +1920000*x15314_bit0 +1920000*x20014_bit0 +1920000*x20214_bit0 +1280000*x20314_bit0 +768000*x22014_bit0 +1344000*x22414_bit0 +1344000*x22514_bit0 +1664000*x26914_bit0 +1152000*x27014_bit0 +1664000*x27114_bit0 +1152000*x27214_bit0 +1152000*x27314_bit0 +2560000*x29214_bit0 +2176000*x29414_bit0 +1920000*x29714_bit0 +1920000*x30114_bit0 +499200*x30314_bit0 +1267200*x31814_bit0 +1267200*x32114_bit0 +1267200*x32214_bit0 +1267200*x32314_bit0 +1267200*x32414_bit0 +1267200*x32714_bit0 +1267200*x32814_bit0 +890880*x33314_bit0 +1907200*x35314_bit0 +1523200*x35814_bit0 +716800*x36214_bit0 +244352*x36314_bit0 +1273600*x36414_bit0 +1267200*x37314_bit0 +1267200*x37414_bit0 +1267200*x37514_bit0 +883200*x37614_bit0 +636160*x37714_bit0 +636160*x37814_bit0 +636160*x38914_bit0 +1139200*x40514_bit0 +1139200*x40814_bit0 +1139200*x41114_bit0 +614400*x41714_bit0 +716800*x41914_bit0 +742400*x42114_bit0 +1273600*x42514_bit0 +1529600*x42614_bit0 +1273600*x43514_bit0 +1273600*x43714_bit0 +1280000*x0415_bit0 +921600*x2015_bit0 +2560000*x2315_bit0 +1280000*x2915_bit0 +1920000*x3815_bit0 +640000*x4015_bit0 +640000*x4815_bit0 +1280000*x5015_bit0 +640000*x5115_bit0 +1280000*x5215_bit0 +1920000*x5515_bit0 +640000*x6515_bit0 +1920000*x6615_bit0 +2240000*x7715_bit0 +640000*x8315_bit0 +1280000*x9015_bit0 +1536000*x9115_bit0 +1139200*x9215_bit0 +678400*x9515_bit0 +1920000*x9615_bit0 +2240000*x10215_bit0 +1280000*x11315_bit0 +640000*x11415_bit0 +640000*x11615_bit0 +1920000*x11715_bit0 +1792000*x11815_bit0 +1920000*x13115_bit0 +1920000*x13315_bit0 +1920000*x13715_bit0 +1920000*x14215_bit0 +1920000*x14315_bit0 +1920000*x14515_bit0 +640000*x15215_bit0 +1920000*x15315_bit0 +1920000*x15615_bit0 +1920000*x16015_bit0 +1920000*x16215_bit0 +1664000*x26915_bit0 +1152000*x27015_bit0 +1664000*x27115_bit0 +1152000*x27215_bit0 +1152000*x27315_bit0 +2560000*x29215_bit0 +2176000*x29415_bit0 +1920000*x29715_bit0 +1920000*x30115_bit0 +499200*x30315_bit0 +1267200*x32115_bit0 +1267200*x32215_bit0 +1267200*x32315_bit0 +1267200*x32415_bit0 +1267200*x32715_bit0 +1267200*x32815_bit0 +1907200*x35315_bit0 +1523200*x35815_bit0 +716800*x36215_bit0 +1145600*x36915_bit0 +1267200*x37315_bit0 +1267200*x37415_bit0 +1267200*x37515_bit0 +883200*x37615_bit0 +1139200*x40515_bit0 +1139200*x40815_bit0 +1139200*x41115_bit0 +614400*x41715_bit0 +716800*x41915_bit0 +742400*x42115_bit0 +1273600*x42515_bit0 +1529600*x42615_bit0 +1273600*x43515_bit0 +1273600*x43715_bit0 +1280000*x0416_bit0 +1920000*x1216_bit0 +2560000*x2316_bit0 +1280000*x2916_bit0 +1152000*x4716_bit0 +640000*x5116_bit0 +1280000*x5216_bit0 +1920000*x6616_bit0 +2560000*x6716_bit0 +1920000*x7616_bit0 +2240000*x7716_bit0 +1280000*x9016_bit0 +1536000*x9116_bit0 +1139200*x9216_bit0 +2240000*x10216_bit0 +1920000*x14216_bit0 +1920000*x14316_bit0 +1920000*x15316_bit0 +2560000*x29216_bit0 +1267200*x32816_bit0 +1907200*x35316_bit0 +716800*x36216_bit0 +1267200*x39916_bit0 +1267200*x40016_bit0 +1139200*x40516_bit0 +1139200*x40816_bit0 +716800*x41916_bit0 +742400*x42116_bit0 +1529600*x42616_bit0 +1280000*x0417_bit0 +1920000*x1217_bit0 +2560000*x2317_bit0 +1280000*x2917_bit0 +640000*x5117_bit0 +1280000*x5217_bit0 +1920000*x7617_bit0 +1280000*x9017_bit0 +1920000*x14217_bit0 +1920000*x14317_bit0 +1920000*x15317_bit0 +716800*x36217_bit0 +1267200*x39917_bit0 +1267200*x40017_bit0 +1139200*x40517_bit0 +1139200*x40817_bit0 +716800*x41917_bit0 +640000*x0818_bit0 +640000*x1618_bit0 +2112000*x3218_bit0 +1280000*x5318_bit0 +2112000*x5418_bit0 +1920000*x5518_bit0 +2560000*x6718_bit0 +640000*x8418_bit0 +1920000*x10018_bit0 +1920000*x10118_bit0 +1920000*x13118_bit0 +1267200*x31818_bit0 +1523200*x35818_bit0 +244352*x36318_bit0 +1273600*x36418_bit0 +1267200*x40318_bit0 +1139200*x41118_bit0 +742400*x42118_bit0 +1273600*x42518_bit0 +1273600*x43518_bit0 +1273600*x43718_bit0 +640000*x0819_bit0 +640000*x1619_bit0 +2112000*x3219_bit0 +1280000*x5319_bit0 +2112000*x5419_bit0 +1920000*x5519_bit0 +640000*x8419_bit0 +1920000*x10019_bit0 +1920000*x10119_bit0 +1920000*x13119_bit0 +1267200*x31819_bit0 +1523200*x35819_bit0 +244352*x36319_bit0 +1273600*x36419_bit0 +1139200*x41119_bit0 +1273600*x42519_bit0 +1273600*x43519_bit0 +640000*x0820_bit0 +640000*x1620_bit0 +2112000*x3220_bit0 +1280000*x5320_bit0 +2112000*x5420_bit0 +640000*x8420_bit0 +1920000*x10020_bit0 +1920000*x10120_bit0 +1920000*x13120_bit0 +1267200*x31820_bit0 +1523200*x35820_bit0 +244352*x36320_bit0 +1273600*x36420_bit0 +1280000*x2921_bit0 +640000*x8921_bit0 +2304000*x14021_bit0 +2304000*x14121_bit0 +2304000*x15121_bit0 +1075200*x16921_bit0 +1049600*x17021_bit0 +1075200*x18121_bit0 +1075200*x18321_bit0 +1280000*x24021_bit0 +1280000*x24121_bit0 +1267200*x39921_bit0 +1267200*x40021_bit0 +1920000*x5522_bit0 +1920000*x10122_bit0 +1523200*x35822_bit0 +1139200*x41122_bit0 +742400*x42122_bit0 +1273600*x42522_bit0 +1273600*x43522_bit0 +1273600*x43722_bit0 +1920000*x5523_bit0 +1920000*x10123_bit0 +1920000*x13123_bit0 +1523200*x35823_bit0 +1139200*x41123_bit0 +1273600*x42523_bit0 +1273600*x43523_bit0 -125*a_bit_10 -250*a_bit_9 -500*a_bit_8 -1000*a_bit_7 -2000*a_bit_6 -4000*a_bit_5 -8000*a_bit_4 -16000*a_bit_3 -32000*a_bit_2 -64000*a_bit_1 -128000*a_bit0 -256000*a_bit1 -512000*a_bit2 -1024000*a_bit3 -2048000*a_bit4 -4096000*a_bit5 -8192000*a_bit6 -16384000*a_bit7 -32768000*a_bit8 -65536000*a_bit9 -131072000*a_bit10 -262144000*a_bit11 -524288000*a_bit12 -1048576000*a_bit13 -2097152000*a_bit14 -4194304000*a_bit15 -8388608000*a_bit16 -16777216000*a_bit17 -33554432000*a_bit18 -67108864000*a_bit19 = +0;
c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-mkc.opb
s UNKNOWN
c Exit Code: 0
c Total time: 2.567 s
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.80 0.95 1.00 2/54 28551
Raw data (stat): 28551 (runsolver) R 28550 24172 24171 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 834934121 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+2.63087 s]
Raw data (loadavg): 0.80 0.95 1.00 1/53 28551
Raw data (stat): 28551 (runsolver) R 28550 24172 24171 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 834934121 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 0

Child status: 0
Real time (s): 2.63033
CPU time (s): 2.6096
CPU user time (s): 2.17567
CPU system time (s): 0.433934
CPU usage (%): 99.2121
Max. virtual memory (Kb): 1028
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####