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/miplib2003/normalized-mps-v2-20-10-mkc.opb
MD5SUM	6ef3eff2fef1e9f71734c5cb8b6e12e4
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	1231.25
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 26493

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-05-24 16:09:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12702 boxname=wulflinc17 idbench=978 idsolver=1 numberseed=0
MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef  /oldhome/oroussel/solvers/bsolo_lpr
MD5SUM BENCH:  6ef3eff2fef1e9f71734c5cb8b6e12e4  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-mkc.opb
REAL COMMAND:  bsolo_lpr /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-mkc.opb
IDLAUNCH: 12702
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        893896 kB
Buffers:         34424 kB
Cached:          84232 kB
SwapCached:        480 kB
Active:          59992 kB
Inactive:        61404 kB
HighTotal:      131008 kB
HighFree:        45556 kB
LowTotal:       903652 kB
LowFree:        848340 kB
SwapTotal:     2097892 kB
SwapFree:      2097148 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6040 kB
Slab:            13940 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-24 16:09:49 (client local time) WITH STATUS 0 IN 2.5946 SECONDS
stats: 12702 7 2.5946 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c ERROR Parsing file!!!
c ERROR parsing line: +1280000*x1_bit0 +1920000*x2_bit0 +1920000*x3_bit0 +1280000*x4_bit0 +1280000*x5_bit0 +1280000*x6_bit0 +1280000*x7_bit0 +640000*x8_bit0 +1536000*x9_bit0 +1920000*x10_bit0 +1280000*x11_bit0 +640000*x12_bit0 +1280000*x13_bit0 +1280000*x14_bit0 +640000*x15_bit0 +640000*x16_bit0 +1280000*x17_bit0 +1280000*x18_bit0 +921600*x19_bit0 +1280000*x20_bit0 +2560000*x21_bit0 +1920000*x22_bit0 +640000*x23_bit0 +1280000*x24_bit0 +1280000*x25_bit0 +640000*x26_bit0 +1280000*x27_bit0 +640000*x28_bit0 +1024000*x29_bit0 +1920000*x30_bit0 +1280000*x31_bit0 +1152000*x32_bit0 +1920000*x33_bit0 +1920000*x34_bit0 +1920000*x35_bit0 +1536000*x36_bit0 +640000*x37_bit0 +1280000*x38_bit0 +640000*x39_bit0 +1920000*x40_bit0 +1920000*x41_bit0 +1280000*x42_bit0 +1920000*x43_bit0 +1152000*x44_bit0 +640000*x45_bit0 +1280000*x46_bit0 +1280000*x47_bit0 +640000*x48_bit0 +1280000*x49_bit0 +1920000*x50_bit0 +1280000*x51_bit0 +640000*x52_bit0 +1920000*x53_bit0 +1920000*x54_bit0 +1920000*x55_bit0 +640000*x56_bit0 +640000*x57_bit0 +640000*x58_bit0 +1920000*x59_bit0 +2560000*x60_bit0 +1280000*x61_bit0 +1280000*x62_bit0 +2560000*x63_bit0 +1280000*x64_bit0 +1600000*x65_bit0 +1536000*x66_bit0 +1280000*x67_bit0 +1280000*x68_bit0 +2240000*x69_bit0 +1920000*x70_bit0 +640000*x71_bit0 +1907200*x72_bit0 +640000*x73_bit0 +640000*x74_bit0 +640000*x75_bit0 +1280000*x76_bit0 +1920000*x77_bit0 +640000*x78_bit0 +640000*x79_bit0 +1280000*x80_bit0 +1536000*x81_bit0 +1139200*x82_bit0 +1920000*x83_bit0 +1920000*x84_bit0 +678400*x85_bit0 +1920000*x86_bit0 +1280000*x87_bit0 +1280000*x88_bit0 +1920000*x89_bit0 +2240000*x90_bit0 +1280000*x91_bit0 +2304000*x92_bit0 +1280000*x93_bit0 +1280000*x94_bit0 +1753600*x95_bit0 +921600*x96_bit0 +1280000*x97_bit0 +640000*x98_bit0 +2304000*x99_bit0 +640000*x100_bit0 +1920000*x101_bit0 +1792000*x102_bit0 +1920000*x103_bit0 +1920000*x104_bit0 +2560000*x105_bit0 +1920000*x106_bit0 +2240000*x107_bit0 +2240000*x108_bit0 +1920000*x109_bit0 +1280000*x110_bit0 +1920000*x111_bit0 +1920000*x112_bit0 +2240000*x113_bit0 +1920000*x114_bit0 +2240000*x115_bit0 +2240000*x116_bit0 +2560000*x117_bit0 +2560000*x118_bit0 +640000*x119_bit0 +1920000*x120_bit0 +2240000*x121_bit0 +2560000*x122_bit0 +1920000*x123_bit0 +640000*x124_bit0 +2560000*x125_bit0 +2560000*x126_bit0 +1920000*x127_bit0 +2560000*x128_bit0 +1920000*x129_bit0 +640000*x130_bit0 +640000*x131_bit0 +1907200*x132_bit0 +640000*x133_bit0 +1689600*x134_bit0 +1075200*x135_bit0 +1049600*x136_bit0 +1036800*x137_bit0 +1536000*x138_bit0 +1075200*x139_bit0 +1036800*x140_bit0 +1075200*x141_bit0 +1536000*x142_bit0 +1036800*x143_bit0 +1920000*x144_bit0 +1036800*x145_bit0 +1536000*x146_bit0 +1024000*x147_bit0 +1920000*x148_bit0 +1920000*x149_bit0 +1920000*x150_bit0 +1830400*x151_bit0 +691200*x152_bit0 +512000*x153_bit0 +1280000*x154_bit0 +1280000*x155_bit0 +1664000*x156_bit0 +1920000*x157_bit0 +1280000*x158_bit0 +1920000*x159_bit0 +1920000*x160_bit0 +2560000*x161_bit0 +2560000*x162_bit0 +1664000*x163_bit0 +1664000*x164_bit0 +1190400*x165_bit0 +1190400*x166_bit0 +1190400*x167_bit0 +1920000*x168_bit0 +1920000*x169_bit0 +1152000*x170_bit0 +1152000*x171_bit0 +1664000*x172_bit0 +1152000*x173_bit0 +1664000*x174_bit0 +1152000*x175_bit0 +1152000*x176_bit0 +1152000*x177_bit0 +1920000*x178_bit0 +1920000*x179_bit0 +1920000*x180_bit0 +2560000*x181_bit0 +2560000*x182_bit0 +1152000*x183_bit0 +1920000*x184_bit0 +1920000*x185_bit0 +1920000*x186_bit0 +1920000*x187_bit0 +1920000*x188_bit0 +1920000*x189_bit0 +1920000*x190_bit0 +1920000*x191_bit0 +1920000*x192_bit0 +2560000*x193_bit0 +1280000*x194_bit0 +2176000*x195_bit0 +1920000*x196_bit0 +1920000*x197_bit0 +1920000*x198_bit0 +1856000*x199_bit0 +1113600*x200_bit0 +1920000*x201_bit0 +499200*x202_bit0 +1267200*x203_bit0 +1267200*x204_bit0 +1267200*x205_bit0 +1267200*x206_bit0 +1267200*x207_bit0 +1267200*x208_bit0 +1267200*x209_bit0 +1267200*x210_bit0 +1267200*x211_bit0 +1267200*x212_bit0 +1267200*x213_bit0 +1395200*x214_bit0 +1395200*x215_bit0 +1267200*x216_bit0 +1267200*x217_bit0 +1267200*x218_bit0 +1267200*x219_bit0 +1267200*x220_bit0 +1267200*x221_bit0 +1267200*x222_bit0 +1267200*x223_bit0 +1267200*x224_bit0 +1267200*x225_bit0 +1267200*x226_bit0 +1523200*x227_bit0 +1523200*x228_bit0 +1523200*x229_bit0 +1523200*x230_bit0 +1907200*x231_bit0 +1907200*x232_bit0 +372224*x233_bit0 +363520*x234_bit0 +1267200*x235_bit0 +239616*x236_bit0 +1523200*x237_bit0 +239616*x238_bit0 +1267200*x239_bit0 +1049600*x240_bit0 +716800*x241_bit0 +1018880*x242_bit0 +1273600*x243_bit0 +1273600*x244_bit0 +1273600*x245_bit0 +1145600*x246_bit0 +635520*x247_bit0 +1273600*x248_bit0 +1267200*x249_bit0 +1267200*x250_bit0 +1267200*x251_bit0 +883200*x252_bit0 +1267200*x253_bit0 +1267200*x254_bit0 +1267200*x255_bit0 +1267200*x256_bit0 +1267200*x257_bit0 +1267200*x258_bit0 +1267200*x259_bit0 +1139200*x260_bit0 +1139200*x261_bit0 +1139200*x262_bit0 +1139200*x263_bit0 +1139200*x264_bit0 +1267200*x265_bit0 +436480*x266_bit0 +603648*x267_bit0 +592768*x268_bit0 +947200*x269_bit0 +614400*x270_bit0 +1267200*x271_bit0 +716800*x272_bit0 +494208*x273_bit0 +742400*x274_bit0 +627200*x275_bit0 +1273600*x276_bit0 +1273600*x277_bit0 +1529600*x278_bit0 +1145600*x279_bit0 +993280*x280_bit0 +712960*x281_bit0 +1273600*x282_bit0 +1273600*x283_bit0 +1273600*x284_bit0 +1273600*x285_bit0 +1273600*x286_bit0 +1273600*x287_bit0 +1145600*x288_bit0 +1273600*x289_bit0 +1273600*x290_bit0 +1920000*x291_bit0 +1920000*x292_bit0 +1280000*x293_bit0 +640000*x294_bit0 +1280000*x295_bit0 +1280000*x296_bit0 +640000*x297_bit0 +1280000*x298_bit0 +921600*x299_bit0 +1280000*x300_bit0 +2560000*x301_bit0 +1280000*x302_bit0 +640000*x303_bit0 +1280000*x304_bit0 +1920000*x305_bit0 +640000*x306_bit0 +1280000*x307_bit0 +1920000*x308_bit0 +640000*x309_bit0 +1280000*x310_bit0 +640000*x311_bit0 +1280000*x312_bit0 +1920000*x313_bit0 +1280000*x314_bit0 +640000*x315_bit0 +1920000*x316_bit0 +1536000*x317_bit0 +1280000*x318_bit0 +2240000*x319_bit0 +640000*x320_bit0 +640000*x321_bit0 +1280000*x322_bit0 +1536000*x323_bit0 +1139200*x324_bit0 +678400*x325_bit0 +1920000*x326_bit0 +1920000*x327_bit0 +2240000*x328_bit0 +1280000*x329_bit0 +2304000*x330_bit0 +1280000*x331_bit0 +1280000*x332_bit0 +1753600*x333_bit0 +1280000*x334_bit0 +640000*x335_bit0 +640000*x336_bit0 +1920000*x337_bit0 +1792000*x338_bit0 +1920000*x339_bit0 +1920000*x340_bit0 +1920000*x341_bit0 +1280000*x342_bit0 +1920000*x343_bit0 +1920000*x344_bit0 +1920000*x345_bit0 +640000*x346_bit0 +1920000*x347_bit0 +1920000*x348_bit0 +1920000*x349_bit0 +1920000*x350_bit0 +1920000*x351_bit0 +1920000*x352_bit0 +1920000*x353_bit0 +1190400*x354_bit0 +1190400*x355_bit0 +1190400*x356_bit0 +1920000*x357_bit0 +1152000*x358_bit0 +1664000*x359_bit0 +1152000*x360_bit0 +1664000*x361_bit0 +1152000*x362_bit0 +1152000*x363_bit0 +1152000*x364_bit0 +1920000*x365_bit0 +1920000*x366_bit0 +1920000*x367_bit0 +2560000*x368_bit0 +2560000*x369_bit0 +1920000*x370_bit0 +1920000*x371_bit0 +2560000*x372_bit0 +2176000*x373_bit0 +1920000*x374_bit0 +1920000*x375_bit0 +1920000*x376_bit0 +1856000*x377_bit0 +1920000*x378_bit0 +499200*x379_bit0 +1267200*x380_bit0 +1267200*x381_bit0 +1267200*x382_bit0 +1267200*x383_bit0 +1267200*x384_bit0 +1267200*x385_bit0 +1267200*x386_bit0 +1267200*x387_bit0 +1267200*x388_bit0 +1267200*x389_bit0 +1267200*x390_bit0 +1267200*x391_bit0 +1267200*x392_bit0 +1267200*x393_bit0 +1267200*x394_bit0 +1907200*x395_bit0 +363520*x396_bit0 +1523200*x397_bit0 +1049600*x398_bit0 +716800*x399_bit0 +1145600*x400_bit0 +1267200*x401_bit0 +1267200*x402_bit0 +1267200*x403_bit0 +883200*x404_bit0 +1139200*x405_bit0 +1139200*x406_bit0 +1139200*x407_bit0 +1139200*x408_bit0 +1139200*x409_bit0 +592768*x410_bit0 +947200*x411_bit0 +614400*x412_bit0 +716800*x413_bit0 +742400*x414_bit0 +627200*x415_bit0 +1273600*x416_bit0 +1529600*x417_bit0 +1273600*x418_bit0 +1273600*x419_bit0 +1920000*x420_bit0 +1920000*x421_bit0 +1280000*x422_bit0 +640000*x423_bit0 +1280000*x424_bit0 +1920000*x425_bit0 +1280000*x426_bit0 +640000*x427_bit0 +1280000*x428_bit0 +921600*x429_bit0 +1280000*x430_bit0 +2560000*x431_bit0 +1280000*x432_bit0 +640000*x433_bit0 +2112000*x434_bit0 +1280000*x435_bit0 +1920000*x436_bit0 +640000*x437_bit0 +1280000*x438_bit0 +1920000*x439_bit0 +640000*x440_bit0 +1280000*x441_bit0 +640000*x442_bit0 +1280000*x443_bit0 +1280000*x444_bit0 +2112000*x445_bit0 +1920000*x446_bit0 +1280000*x447_bit0 +640000*x448_bit0 +1920000*x449_bit0 +1536000*x450_bit0 +1280000*x451_bit0 +1920000*x452_bit0 +2240000*x453_bit0 +640000*x454_bit0 +640000*x455_bit0 +1280000*x456_bit0 +1536000*x457_bit0 +1139200*x458_bit0 +678400*x459_bit0 +1920000*x460_bit0 +1920000*x461_bit0 +1920000*x462_bit0 +2240000*x463_bit0 +1280000*x464_bit0 +2304000*x465_bit0 +1280000*x466_bit0 +1753600*x467_bit0 +1280000*x468_bit0 +640000*x469_bit0 +640000*x470_bit0 +1920000*x471_bit0 +1792000*x472_bit0 +1920000*x473_bit0 +1280000*x474_bit0 +1920000*x475_bit0 +1280000*x476_bit0 +1920000*x477_bit0 +1920000*x478_bit0 +640000*x479_bit0 +1920000*x480_bit0 +1625600*x481_bit0 +768000*x482_bit0 +1536000*x483_bit0 +1536000*x484_bit0 +1536000*x485_bit0 +1536000*x486_bit0 +1536000*x487_bit0 +1536000*x488_bit0 +1536000*x489_bit0 +1779200*x490_bit0 +768000*x491_bit0 +768000*x492_bit0 +1536000*x493_bit0 +1280000*x494_bit0 +1920000*x495_bit0 +896000*x496_bit0 +768000*x497_bit0 +1536000*x498_bit0 +1280000*x499_bit0 +1920000*x500_bit0 +1920000*x501_bit0 +1920000*x502_bit0 +1280000*x503_bit0 +1408000*x504_bit0 +1280000*x505_bit0 +1280000*x506_bit0 +1280000*x507_bit0 +1280000*x508_bit0 +1280000*x509_bit0 +1625600*x510_bit0 +1779200*x511_bit0 +768000*x512_bit0 +1408000*x513_bit0 +1344000*x514_bit0 +1344000*x515_bit0 +1344000*x516_bit0 +1779200*x517_bit0 +263296*x518_bit0 +1600000*x519_bit0 +1920000*x520_bit0 +1536000*x521_bit0 +1920000*x522_bit0 +1190400*x523_bit0 +1190400*x524_bit0 +1190400*x525_bit0 +1920000*x526_bit0 +1152000*x527_bit0 +1664000*x528_bit0 +1152000*x529_bit0 +1664000*x530_bit0 +1152000*x531_bit0 +1152000*x532_bit0 +1152000*x533_bit0 +1920000*x534_bit0 +1920000*x535_bit0 +1920000*x536_bit0 +2560000*x537_bit0 +2560000*x538_bit0 +1920000*x539_bit0 +1920000*x540_bit0 +2560000*x541_bit0 +2176000*x542_bit0 +1920000*x543_bit0 +1920000*x544_bit0 +1920000*x545_bit0 +1856000*x546_bit0 +1920000*x547_bit0 +768000*x548_bit0 +499200*x549_bit0 +1267200*x550_bit0 +1267200*x551_bit0 +1267200*x552_bit0 +1267200*x553_bit0 +1267200*x554_bit0 +1267200*x555_bit0 +1267200*x556_bit0 +1267200*x557_bit0 +1267200*x558_bit0 +1267200*x559_bit0 +1267200*x560_bit0 +1267200*x561_bit0 +1267200*x562_bit0 +1267200*x563_bit0 +1267200*x564_bit0 +1273600*x565_bit0 +1273600*x566_bit0 +890880*x567_bit0 +636160*x568_bit0 +636160*x569_bit0 +636160*x570_bit0 +636160*x571_bit0 +762880*x572_bit0 +1907200*x573_bit0 +363520*x574_bit0 +1523200*x575_bit0 +1049600*x576_bit0 +716800*x577_bit0 +244352*x578_bit0 +1273600*x579_bit0 +1267200*x580_bit0 +1267200*x581_bit0 +1267200*x582_bit0 +883200*x583_bit0 +636160*x584_bit0 +636160*x585_bit0 +1273600*x586_bit0 +1273600*x587_bit0 +636160*x588_bit0 +636160*x589_bit0 +1273600*x590_bit0 +636160*x591_bit0 +1273600*x592_bit0 +1139200*x593_bit0 +1139200*x594_bit0 +1139200*x595_bit0 +1139200*x596_bit0 +1139200*x597_bit0 +592768*x598_bit0 +947200*x599_bit0 +614400*x600_bit0 +716800*x601_bit0 +742400*x602_bit0 +627200*x603_bit0 +640000*x604_bit0 +1273600*x605_bit0 +1529600*x606_bit0 +1273600*x607_bit0 +1273600*x608_bit0 +1920000*x609_bit0 +1920000*x610_bit0 +1280000*x611_bit0 +640000*x612_bit0 +1280000*x613_bit0 +1920000*x614_bit0 +1280000*x615_bit0 +640000*x616_bit0 +1280000*x617_bit0 +921600*x618_bit0 +1280000*x619_bit0 +2560000*x620_bit0 +1280000*x621_bit0 +640000*x622_bit0 +2112000*x623_bit0 +1280000*x624_bit0 +1920000*x625_bit0 +640000*x626_bit0 +1280000*x627_bit0 +1920000*x628_bit0 +640000*x629_bit0 +1280000*x630_bit0 +640000*x631_bit0 +1280000*x632_bit0 +1280000*x633_bit0 +2112000*x634_bit0 +1920000*x635_bit0 +1280000*x636_bit0 +640000*x637_bit0 +1920000*x638_bit0 +1536000*x639_bit0 +1280000*x640_bit0 +1920000*x641_bit0 +2240000*x642_bit0 +640000*x643_bit0 +640000*x644_bit0 +1280000*x645_bit0 +1536000*x646_bit0 +1139200*x647_bit0 +678400*x648_bit0 +1920000*x649_bit0 +1920000*x650_bit0 +1920000*x651_bit0 +2240000*x652_bit0 +1280000*x653_bit0 +2304000*x654_bit0 +1280000*x655_bit0 +1753600*x656_bit0 +1280000*x657_bit0 +640000*x658_bit0 +640000*x659_bit0 +1920000*x660_bit0 +1792000*x661_bit0 +1920000*x662_bit0 +1280000*x663_bit0 +1920000*x664_bit0 +1280000*x665_bit0 +1920000*x666_bit0 +1920000*x667_bit0 +640000*x668_bit0 +1920000*x669_bit0 +1625600*x670_bit0 +768000*x671_bit0 +1536000*x672_bit0 +1536000*x673_bit0 +1536000*x674_bit0 +1536000*x675_bit0 +1536000*x676_bit0 +1536000*x677_bit0 +1536000*x678_bit0 +1779200*x679_bit0 +768000*x680_bit0 +768000*x681_bit0 +1536000*x682_bit0 +1280000*x683_bit0 +1920000*x684_bit0 +896000*x685_bit0 +768000*x686_bit0 +1536000*x687_bit0 +1280000*x688_bit0 +1920000*x689_bit0 +1920000*x690_bit0 +1920000*x691_bit0 +1280000*x692_bit0 +1408000*x693_bit0 +1280000*x694_bit0 +1280000*x695_bit0 +1280000*x696_bit0 +1280000*x697_bit0 +1280000*x698_bit0 +1625600*x699_bit0 +1779200*x700_bit0 +768000*x701_bit0 +1408000*x702_bit0 +1344000*x703_bit0 +1344000*x704_bit0 +1344000*x705_bit0 +1779200*x706_bit0 +263296*x707_bit0 +1600000*x708_bit0 +1920000*x709_bit0 +1536000*x710_bit0 +1920000*x711_bit0 +1190400*x712_bit0 +1190400*x713_bit0 +1190400*x714_bit0 +1920000*x715_bit0 +1152000*x716_bit0 +1664000*x717_bit0 +1152000*x718_bit0 +1664000*x719_bit0 +1152000*x720_bit0 +1152000*x721_bit0 +1152000*x722_bit0 +1920000*x723_bit0 +1920000*x724_bit0 +1920000*x725_bit0 +2560000*x726_bit0 +2560000*x727_bit0 +1920000*x728_bit0 +1920000*x729_bit0 +2560000*x730_bit0 +2176000*x731_bit0 +1920000*x732_bit0 +1920000*x733_bit0 +1920000*x734_bit0 +1856000*x735_bit0 +1920000*x736_bit0 +768000*x737_bit0 +499200*x738_bit0 +1267200*x739_bit0 +1267200*x740_bit0 +1267200*x741_bit0 +1267200*x742_bit0 +1267200*x743_bit0 +1267200*x744_bit0 +1267200*x745_bit0 +1267200*x746_bit0 +1267200*x747_bit0 +1267200*x748_bit0 +1267200*x749_bit0 +1267200*x750_bit0 +1267200*x751_bit0 +1267200*x752_bit0 +1267200*x753_bit0 +1273600*x754_bit0 +1273600*x755_bit0 +890880*x756_bit0 +636160*x757_bit0 +636160*x758_bit0 +636160*x759_bit0 +636160*x760_bit0 +762880*x761_bit0 +1907200*x762_bit0 +363520*x763_bit0 +1523200*x764_bit0 +1049600*x765_bit0 +716800*x766_bit0 +244352*x767_bit0 +1273600*x768_bit0 +1267200*x769_bit0 +1267200*x770_bit0 +1267200*x771_bit0 +883200*x772_bit0 +636160*x773_bit0 +636160*x774_bit0 +1273600*x775_bit0 +1273600*x776_bit0 +636160*x777_bit0 +636160*x778_bit0 +1273600*x779_bit0 +636160*x780_bit0 +1273600*x781_bit0 +1139200*x782_bit0 +1139200*x783_bit0 +1139200*x784_bit0 +1139200*x785_bit0 +1139200*x786_bit0 +592768*x787_bit0 +947200*x788_bit0 +614400*x789_bit0 +716800*x790_bit0 +742400*x791_bit0 +627200*x792_bit0 +640000*x793_bit0 +1273600*x794_bit0 +1529600*x795_bit0 +1273600*x796_bit0 +1273600*x797_bit0 +1920000*x798_bit0 +1920000*x799_bit0 +1280000*x800_bit0 +1280000*x801_bit0 +1920000*x802_bit0 +1280000*x803_bit0 +1920000*x804_bit0 +1280000*x805_bit0 +1280000*x806_bit0 +921600*x807_bit0 +1280000*x808_bit0 +2560000*x809_bit0 +1280000*x810_bit0 +640000*x811_bit0 +1280000*x812_bit0 +1920000*x813_bit0 +1536000*x814_bit0 +640000*x815_bit0 +1280000*x816_bit0 +1920000*x817_bit0 +1152000*x818_bit0 +640000*x819_bit0 +1280000*x820_bit0 +640000*x821_bit0 +1280000*x822_bit0 +1280000*x823_bit0 +1920000*x824_bit0 +640000*x825_bit0 +1920000*x826_bit0 +1280000*x827_bit0 +1536000*x828_bit0 +1280000*x829_bit0 +1280000*x830_bit0 +1920000*x831_bit0 +2240000*x832_bit0 +640000*x833_bit0 +1280000*x834_bit0 +1920000*x835_bit0 +1280000*x836_bit0 +1536000*x837_bit0 +1139200*x838_bit0 +678400*x839_bit0 +1920000*x840_bit0 +1280000*x841_bit0 +1280000*x842_bit0 +2240000*x843_bit0 +1280000*x844_bit0 +2304000*x845_bit0 +1280000*x846_bit0 +1753600*x847_bit0 +1280000*x848_bit0 +640000*x849_bit0 +640000*x850_bit0 +1920000*x851_bit0 +1792000*x852_bit0 +1920000*x853_bit0 +1280000*x854_bit0 +1280000*x855_bit0 +1920000*x856_bit0 +1920000*x857_bit0 +640000*x858_bit0 +1920000*x859_bit0 +640000*x860_bit0 +1689600*x861_bit0 +1625600*x862_bit0 +768000*x863_bit0 +1536000*x864_bit0 +1536000*x865_bit0 +1536000*x866_bit0 +1536000*x867_bit0 +1536000*x868_bit0 +1536000*x869_bit0 +1536000*x870_bit0 +1779200*x871_bit0 +768000*x872_bit0 +768000*x873_bit0 +1536000*x874_bit0 +1280000*x875_bit0 +1920000*x876_bit0 +896000*x877_bit0 +768000*x878_bit0 +1536000*x879_bit0 +1280000*x880_bit0 +1920000*x881_bit0 +1920000*x882_bit0 +1920000*x883_bit0 +1280000*x884_bit0 +1408000*x885_bit0 +1280000*x886_bit0 +1280000*x887_bit0 +1280000*x888_bit0 +1280000*x889_bit0 +1280000*x890_bit0 +1625600*x891_bit0 +1779200*x892_bit0 +768000*x893_bit0 +1408000*x894_bit0 +1344000*x895_bit0 +1344000*x896_bit0 +1344000*x897_bit0 +1779200*x898_bit0 +263296*x899_bit0 +1600000*x900_bit0 +1920000*x901_bit0 +1920000*x902_bit0 +1536000*x903_bit0 +1664000*x904_bit0 +1920000*x905_bit0 +1920000*x906_bit0 +1920000*x907_bit0 +2560000*x908_bit0 +2560000*x909_bit0 +1664000*x910_bit0 +1664000*x911_bit0 +1190400*x912_bit0 +1190400*x913_bit0 +1190400*x914_bit0 +1920000*x915_bit0 +1920000*x916_bit0 +1152000*x917_bit0 +1664000*x918_bit0 +1152000*x919_bit0 +1664000*x920_bit0 +1152000*x921_bit0 +1152000*x922_bit0 +1152000*x923_bit0 +1920000*x924_bit0 +1920000*x925_bit0 +1920000*x926_bit0 +2560000*x927_bit0 +2560000*x928_bit0 +1920000*x929_bit0 +1920000*x930_bit0 +1920000*x931_bit0 +1920000*x932_bit0 +1920000*x933_bit0 +1920000*x934_bit0 +1920000*x935_bit0 +1920000*x936_bit0 +1920000*x937_bit0 +2560000*x938_bit0 +2176000*x939_bit0 +1920000*x940_bit0 +1920000*x941_bit0 +1920000*x942_bit0 +1856000*x943_bit0 +1920000*x944_bit0 +768000*x945_bit0 +499200*x946_bit0 +1267200*x947_bit0 +1267200*x948_bit0 +1267200*x949_bit0 +1267200*x950_bit0 +1267200*x951_bit0 +1267200*x952_bit0 +1267200*x953_bit0 +1267200*x954_bit0 +1267200*x955_bit0 +1267200*x956_bit0 +1267200*x957_bit0 +1267200*x958_bit0 +1267200*x959_bit0 +1267200*x960_bit0 +1267200*x961_bit0 +1273600*x962_bit0 +1273600*x963_bit0 +890880*x964_bit0 +636160*x965_bit0 +636160*x966_bit0 +636160*x967_bit0 +636160*x968_bit0 +762880*x969_bit0 +1907200*x970_bit0 +363520*x971_bit0 +1049600*x972_bit0 +716800*x973_bit0 +1267200*x974_bit0 +1267200*x975_bit0 +1267200*x976_bit0 +883200*x977_bit0 +636160*x978_bit0 +636160*x979_bit0 +1273600*x980_bit0 +1273600*x981_bit0 +636160*x982_bit0 +636160*x983_bit0 +1273600*x984_bit0 +636160*x985_bit0 +1273600*x986_bit0 +1139200*x987_bit0 +1139200*x988_bit0 +1139200*x989_bit0 +1139200*x990_bit0 +592768*x991_bit0 +947200*x992_bit0 +614400*x993_bit0 +716800*x994_bit0 +627200*x995_bit0 +640000*x996_bit0 +1529600*x997_bit0 +1920000*x998_bit0 +1920000*x999_bit0 +1280000*x1000_bit0 +640000*x1001_bit0 +1280000*x1002_bit0 +1920000*x1003_bit0 +1280000*x1004_bit0 +640000*x1005_bit0 +1280000*x1006_bit0 +921600*x1007_bit0 +1280000*x1008_bit0 +2560000*x1009_bit0 +1280000*x1010_bit0 +640000*x1011_bit0 +2112000*x1012_bit0 +1280000*x1013_bit0 +1920000*x1014_bit0 +640000*x1015_bit0 +1280000*x1016_bit0 +1920000*x1017_bit0 +640000*x1018_bit0 +1280000*x1019_bit0 +640000*x1020_bit0 +1280000*x1021_bit0 +1280000*x1022_bit0 +2112000*x1023_bit0 +1920000*x1024_bit0 +1280000*x1025_bit0 +640000*x1026_bit0 +1920000*x1027_bit0 +1536000*x1028_bit0 +1280000*x1029_bit0 +1920000*x1030_bit0 +2240000*x1031_bit0 +640000*x1032_bit0 +640000*x1033_bit0 +1280000*x1034_bit0 +1536000*x1035_bit0 +1139200*x1036_bit0 +678400*x1037_bit0 +1920000*x1038_bit0 +1920000*x1039_bit0 +1920000*x1040_bit0 +2240000*x1041_bit0 +1280000*x1042_bit0 +2304000*x1043_bit0 +1280000*x1044_bit0 +1753600*x1045_bit0 +1280000*x1046_bit0 +640000*x1047_bit0 +640000*x1048_bit0 +1920000*x1049_bit0 +1792000*x1050_bit0 +1920000*x1051_bit0 +1280000*x1052_bit0 +1920000*x1053_bit0 +1280000*x1054_bit0 +1920000*x1055_bit0 +1920000*x1056_bit0 +640000*x1057_bit0 +1920000*x1058_bit0 +1625600*x1059_bit0 +768000*x1060_bit0 +1536000*x1061_bit0 +1536000*x1062_bit0 +1536000*x1063_bit0 +1536000*x1064_bit0 +1536000*x1065_bit0 +1536000*x1066_bit0 +1536000*x1067_bit0 +1779200*x1068_bit0 +768000*x1069_bit0 +768000*x1070_bit0 +1536000*x1071_bit0 +1280000*x1072_bit0 +1920000*x1073_bit0 +896000*x1074_bit0 +768000*x1075_bit0 +1536000*x1076_bit0 +1280000*x1077_bit0 +1920000*x1078_bit0 +1920000*x1079_bit0 +1920000*x1080_bit0 +1280000*x1081_bit0 +1408000*x1082_bit0 +1280000*x1083_bit0 +1280000*x1084_bit0 +1280000*x1085_bit0 +1280000*x1086_bit0 +1280000*x1087_bit0 +1625600*x1088_bit0 +1779200*x1089_bit0 +768000*x1090_bit0 +1408000*x1091_bit0 +1344000*x1092_bit0 +1344000*x1093_bit0 +1344000*x1094_bit0 +1779200*x1095_bit0 +263296*x1096_bit0 +1600000*x1097_bit0 +1920000*x1098_bit0 +1536000*x1099_bit0 +1920000*x1100_bit0 +1190400*x1101_bit0 +1190400*x1102_bit0 +1190400*x1103_bit0 +1920000*x1104_bit0 +1152000*x1105_bit0 +1664000*x1106_bit0 +1152000*x1107_bit0 +1664000*x1108_bit0 +1152000*x1109_bit0 +1152000*x1110_bit0 +1152000*x1111_bit0 +1920000*x1112_bit0 +1920000*x1113_bit0 +1920000*x1114_bit0 +2560000*x1115_bit0 +2560000*x1116_bit0 +1920000*x1117_bit0 +1920000*x1118_bit0 +2560000*x1119_bit0 +2176000*x1120_bit0 +1920000*x1121_bit0 +1920000*x1122_bit0 +1920000*x1123_bit0 +1856000*x1124_bit0 +1920000*x1125_bit0 +768000*x1126_bit0 +499200*x1127_bit0 +1267200*x1128_bit0 +1267200*x1129_bit0 +1267200*x1130_bit0 +1267200*x1131_bit0 +1267200*x1132_bit0 +1267200*x1133_bit0 +1267200*x1134_bit0 +1267200*x1135_bit0 +1267200*x1136_bit0 +1267200*x1137_bit0 +1267200*x1138_bit0 +1267200*x1139_bit0 +1267200*x1140_bit0 +1267200*x1141_bit0 +1267200*x1142_bit0 +1273600*x1143_bit0 +1273600*x1144_bit0 +890880*x1145_bit0 +636160*x1146_bit0 +636160*x1147_bit0 +636160*x1148_bit0 +636160*x1149_bit0 +762880*x1150_bit0 +1907200*x1151_bit0 +363520*x1152_bit0 +1523200*x1153_bit0 +1049600*x1154_bit0 +716800*x1155_bit0 +244352*x1156_bit0 +1273600*x1157_bit0 +1267200*x1158_bit0 +1267200*x1159_bit0 +1267200*x1160_bit0 +883200*x1161_bit0 +636160*x1162_bit0 +636160*x1163_bit0 +1273600*x1164_bit0 +1273600*x1165_bit0 +636160*x1166_bit0 +636160*x1167_bit0 +1273600*x1168_bit0 +636160*x1169_bit0 +1273600*x1170_bit0 +1139200*x1171_bit0 +1139200*x1172_bit0 +1139200*x1173_bit0 +1139200*x1174_bit0 +1139200*x1175_bit0 +592768*x1176_bit0 +947200*x1177_bit0 +614400*x1178_bit0 +716800*x1179_bit0 +742400*x1180_bit0 +627200*x1181_bit0 +640000*x1182_bit0 +1273600*x1183_bit0 +1529600*x1184_bit0 +1273600*x1185_bit0 +1273600*x1186_bit0 +1920000*x1187_bit0 +1920000*x1188_bit0 +1280000*x1189_bit0 +640000*x1190_bit0 +1280000*x1191_bit0 +1920000*x1192_bit0 +1280000*x1193_bit0 +640000*x1194_bit0 +1280000*x1195_bit0 +921600*x1196_bit0 +1280000*x1197_bit0 +2560000*x1198_bit0 +1280000*x1199_bit0 +640000*x1200_bit0 +2112000*x1201_bit0 +1280000*x1202_bit0 +1920000*x1203_bit0 +640000*x1204_bit0 +1280000*x1205_bit0 +1920000*x1206_bit0 +640000*x1207_bit0 +1280000*x1208_bit0 +640000*x1209_bit0 +1280000*x1210_bit0 +1280000*x1211_bit0 +2112000*x1212_bit0 +1920000*x1213_bit0 +1280000*x1214_bit0 +640000*x1215_bit0 +1920000*x1216_bit0 +1536000*x1217_bit0 +1280000*x1218_bit0 +1920000*x1219_bit0 +2240000*x1220_bit0 +640000*x1221_bit0 +640000*x1222_bit0 +1280000*x1223_bit0 +1536000*x1224_bit0 +1139200*x1225_bit0 +678400*x1226_bit0 +1920000*x1227_bit0 +1920000*x1228_bit0 +1920000*x1229_bit0 +2240000*x1230_bit0 +1280000*x1231_bit0 +2304000*x1232_bit0 +1280000*x1233_bit0 +1753600*x1234_bit0 +1280000*x1235_bit0 +640000*x1236_bit0 +640000*x1237_bit0 +1920000*x1238_bit0 +1792000*x1239_bit0 +1920000*x1240_bit0 +1280000*x1241_bit0 +1920000*x1242_bit0 +1280000*x1243_bit0 +1920000*x1244_bit0 +1920000*x1245_bit0 +640000*x1246_bit0 +1920000*x1247_bit0 +1625600*x1248_bit0 +768000*x1249_bit0 +1536000*x1250_bit0 +1536000*x1251_bit0 +1536000*x1252_bit0 +1536000*x1253_bit0 +1536000*x1254_bit0 +1536000*x1255_bit0 +1536000*x1256_bit0 +1779200*x1257_bit0 +768000*x1258_bit0 +768000*x1259_bit0 +1536000*x1260_bit0 +1280000*x1261_bit0 +1920000*x1262_bit0 +896000*x1263_bit0 +768000*x1264_bit0 +1536000*x1265_bit0 +1280000*x1266_bit0 +1920000*x1267_bit0 +1920000*x1268_bit0 +1920000*x1269_bit0 +1280000*x1270_bit0 +1408000*x1271_bit0 +1280000*x1272_bit0 +1280000*x1273_bit0 +1280000*x1274_bit0 +1280000*x1275_bit0 +1280000*x1276_bit0 +1625600*x1277_bit0 +1779200*x1278_bit0 +768000*x1279_bit0 +1408000*x1280_bit0 +1344000*x1281_bit0 +1344000*x1282_bit0 +1344000*x1283_bit0 +1779200*x1284_bit0 +263296*x1285_bit0 +1600000*x1286_bit0 +1920000*x1287_bit0 +1536000*x1288_bit0 +1920000*x1289_bit0 +1190400*x1290_bit0 +1190400*x1291_bit0 +1190400*x1292_bit0 +1920000*x1293_bit0 +1152000*x1294_bit0 +1664000*x1295_bit0 +1152000*x1296_bit0 +1664000*x1297_bit0 +1152000*x1298_bit0 +1152000*x1299_bit0 +1152000*x1300_bit0 +1920000*x1301_bit0 +1920000*x1302_bit0 +1920000*x1303_bit0 +2560000*x1304_bit0 +2560000*x1305_bit0 +1920000*x1306_bit0 +1920000*x1307_bit0 +2560000*x1308_bit0 +2176000*x1309_bit0 +1920000*x1310_bit0 +1920000*x1311_bit0 +1920000*x1312_bit0 +1856000*x1313_bit0 +1920000*x1314_bit0 +768000*x1315_bit0 +499200*x1316_bit0 +1267200*x1317_bit0 +1267200*x1318_bit0 +1267200*x1319_bit0 +1267200*x1320_bit0 +1267200*x1321_bit0 +1267200*x1322_bit0 +1267200*x1323_bit0 +1267200*x1324_bit0 +1267200*x1325_bit0 +1267200*x1326_bit0 +1267200*x1327_bit0 +1267200*x1328_bit0 +1267200*x1329_bit0 +1267200*x1330_bit0 +1267200*x1331_bit0 +1273600*x1332_bit0 +1273600*x1333_bit0 +890880*x1334_bit0 +636160*x1335_bit0 +636160*x1336_bit0 +636160*x1337_bit0 +636160*x1338_bit0 +762880*x1339_bit0 +1907200*x1340_bit0 +363520*x1341_bit0 +1523200*x1342_bit0 +1049600*x1343_bit0 +716800*x1344_bit0 +244352*x1345_bit0 +1273600*x1346_bit0 +1267200*x1347_bit0 +1267200*x1348_bit0 +1267200*x1349_bit0 +883200*x1350_bit0 +636160*x1351_bit0 +636160*x1352_bit0 +1273600*x1353_bit0 +1273600*x1354_bit0 +636160*x1355_bit0 +636160*x1356_bit0 +1273600*x1357_bit0 +636160*x1358_bit0 +1273600*x1359_bit0 +1139200*x1360_bit0 +1139200*x1361_bit0 +1139200*x1362_bit0 +1139200*x1363_bit0 +1139200*x1364_bit0 +592768*x1365_bit0 +947200*x1366_bit0 +614400*x1367_bit0 +716800*x1368_bit0 +742400*x1369_bit0 +627200*x1370_bit0 +640000*x1371_bit0 +1273600*x1372_bit0 +1529600*x1373_bit0 +1273600*x1374_bit0 +1273600*x1375_bit0 +1920000*x1376_bit0 +1920000*x1377_bit0 +1280000*x1378_bit0 +640000*x1379_bit0 +1280000*x1380_bit0 +1920000*x1381_bit0 +1280000*x1382_bit0 +640000*x1383_bit0 +1280000*x1384_bit0 +921600*x1385_bit0 +1280000*x1386_bit0 +2560000*x1387_bit0 +1280000*x1388_bit0 +640000*x1389_bit0 +2112000*x1390_bit0 +1280000*x1391_bit0 +1920000*x1392_bit0 +640000*x1393_bit0 +1280000*x1394_bit0 +1920000*x1395_bit0 +640000*x1396_bit0 +1280000*x1397_bit0 +640000*x1398_bit0 +1280000*x1399_bit0 +1280000*x1400_bit0 +2112000*x1401_bit0 +1920000*x1402_bit0 +1280000*x1403_bit0 +640000*x1404_bit0 +1920000*x1405_bit0 +1536000*x1406_bit0 +1280000*x1407_bit0 +1920000*x1408_bit0 +2240000*x1409_bit0 +640000*x1410_bit0 +640000*x1411_bit0 +1280000*x1412_bit0 +1536000*x1413_bit0 +1139200*x1414_bit0 +678400*x1415_bit0 +1920000*x1416_bit0 +1920000*x1417_bit0 +1920000*x1418_bit0 +2240000*x1419_bit0 +1280000*x1420_bit0 +2304000*x1421_bit0 +1280000*x1422_bit0 +1753600*x1423_bit0 +1280000*x1424_bit0 +640000*x1425_bit0 +640000*x1426_bit0 +1920000*x1427_bit0 +1792000*x1428_bit0 +1920000*x1429_bit0 +1280000*x1430_bit0 +1920000*x1431_bit0 +1280000*x1432_bit0 +1920000*x1433_bit0 +1920000*x1434_bit0 +640000*x1435_bit0 +1920000*x1436_bit0 +1625600*x1437_bit0 +768000*x1438_bit0 +1536000*x1439_bit0 +1536000*x1440_bit0 +1536000*x1441_bit0 +1536000*x1442_bit0 +1536000*x1443_bit0 +1536000*x1444_bit0 +1536000*x1445_bit0 +1779200*x1446_bit0 +768000*x1447_bit0 +768000*x1448_bit0 +1536000*x1449_bit0 +1280000*x1450_bit0 +1920000*x1451_bit0 +896000*x1452_bit0 +768000*x1453_bit0 +1536000*x1454_bit0 +1280000*x1455_bit0 +1920000*x1456_bit0 +1920000*x1457_bit0 +1920000*x1458_bit0 +1280000*x1459_bit0 +1408000*x1460_bit0 +1280000*x1461_bit0 +1280000*x1462_bit0 +1280000*x1463_bit0 +1280000*x1464_bit0 +1280000*x1465_bit0 +1625600*x1466_bit0 +1779200*x1467_bit0 +768000*x1468_bit0 +1408000*x1469_bit0 +1344000*x1470_bit0 +1344000*x1471_bit0 +1344000*x1472_bit0 +1779200*x1473_bit0 +263296*x1474_bit0 +1600000*x1475_bit0 +1920000*x1476_bit0 +1536000*x1477_bit0 +1920000*x1478_bit0 +1190400*x1479_bit0 +1190400*x1480_bit0 +1190400*x1481_bit0 +1920000*x1482_bit0 +1152000*x1483_bit0 +1664000*x1484_bit0 +1152000*x1485_bit0 +1664000*x1486_bit0 +1152000*x1487_bit0 +1152000*x1488_bit0 +1152000*x1489_bit0 +1920000*x1490_bit0 +1920000*x1491_bit0 +1920000*x1492_bit0 +2560000*x1493_bit0 +2560000*x1494_bit0 +1920000*x1495_bit0 +1920000*x1496_bit0 +2560000*x1497_bit0 +2176000*x1498_bit0 +1920000*x1499_bit0 +1920000*x1500_bit0 +1920000*x1501_bit0 +1856000*x1502_bit0 +1920000*x1503_bit0 +768000*x1504_bit0 +499200*x1505_bit0 +1267200*x1506_bit0 +1267200*x1507_bit0 +1267200*x1508_bit0 +1267200*x1509_bit0 +1267200*x1510_bit0 +1267200*x1511_bit0 +1267200*x1512_bit0 +1267200*x1513_bit0 +1267200*x1514_bit0 +1267200*x1515_bit0 +1267200*x1516_bit0 +1267200*x1517_bit0 +1267200*x1518_bit0 +1267200*x1519_bit0 +1267200*x1520_bit0 +1273600*x1521_bit0 +1273600*x1522_bit0 +890880*x1523_bit0 +636160*x1524_bit0 +636160*x1525_bit0 +636160*x1526_bit0 +636160*x1527_bit0 +762880*x1528_bit0 +1907200*x1529_bit0 +363520*x1530_bit0 +1523200*x1531_bit0 +1049600*x1532_bit0 +716800*x1533_bit0 +244352*x1534_bit0 +1273600*x1535_bit0 +1267200*x1536_bit0 +1267200*x1537_bit0 +1267200*x1538_bit0 +883200*x1539_bit0 +636160*x1540_bit0 +636160*x1541_bit0 +1273600*x1542_bit0 +1273600*x1543_bit0 +636160*x1544_bit0 +636160*x1545_bit0 +1273600*x1546_bit0 +636160*x1547_bit0 +1273600*x1548_bit0 +1139200*x1549_bit0 +1139200*x1550_bit0 +1139200*x1551_bit0 +1139200*x1552_bit0 +1139200*x1553_bit0 +592768*x1554_bit0 +947200*x1555_bit0 +614400*x1556_bit0 +716800*x1557_bit0 +742400*x1558_bit0 +627200*x1559_bit0 +640000*x1560_bit0 +1273600*x1561_bit0 +1529600*x1562_bit0 +1273600*x1563_bit0 +1273600*x1564_bit0 +1920000*x1565_bit0 +1920000*x1566_bit0 +1280000*x1567_bit0 +1920000*x1568_bit0 +1280000*x1569_bit0 +640000*x1570_bit0 +1280000*x1571_bit0 +1280000*x1572_bit0 +921600*x1573_bit0 +1280000*x1574_bit0 +640000*x1575_bit0 +1280000*x1576_bit0 +1920000*x1577_bit0 +1920000*x1578_bit0 +1536000*x1579_bit0 +640000*x1580_bit0 +1280000*x1581_bit0 +1920000*x1582_bit0 +640000*x1583_bit0 +1280000*x1584_bit0 +1280000*x1585_bit0 +1920000*x1586_bit0 +832000*x1587_bit0 +640000*x1588_bit0 +640000*x1589_bit0 +1280000*x1590_bit0 +1536000*x1591_bit0 +1280000*x1592_bit0 +1280000*x1593_bit0 +640000*x1594_bit0 +640000*x1595_bit0 +1280000*x1596_bit0 +1920000*x1597_bit0 +640000*x1598_bit0 +640000*x1599_bit0 +1920000*x1600_bit0 +1920000*x1601_bit0 +678400*x1602_bit0 +1920000*x1603_bit0 +1280000*x1604_bit0 +1280000*x1605_bit0 +1280000*x1606_bit0 +819200*x1607_bit0 +2304000*x1608_bit0 +1280000*x1609_bit0 +1753600*x1610_bit0 +1280000*x1611_bit0 +640000*x1612_bit0 +640000*x1613_bit0 +1920000*x1614_bit0 +1792000*x1615_bit0 +1920000*x1616_bit0 +1920000*x1617_bit0 +1920000*x1618_bit0 +1920000*x1619_bit0 +1920000*x1620_bit0 +1920000*x1621_bit0 +1920000*x1622_bit0 +1920000*x1623_bit0 +1280000*x1624_bit0 +1280000*x1625_bit0 +640000*x1626_bit0 +640000*x1627_bit0 +1689600*x1628_bit0 +1625600*x1629_bit0 +768000*x1630_bit0 +1536000*x1631_bit0 +1536000*x1632_bit0 +1536000*x1633_bit0 +1536000*x1634_bit0 +1536000*x1635_bit0 +1536000*x1636_bit0 +1536000*x1637_bit0 +1779200*x1638_bit0 +768000*x1639_bit0 +768000*x1640_bit0 +1536000*x1641_bit0 +1280000*x1642_bit0 +1920000*x1643_bit0 +896000*x1644_bit0 +768000*x1645_bit0 +1536000*x1646_bit0 +1664000*x1647_bit0 +1280000*x1648_bit0 +1920000*x1649_bit0 +1920000*x1650_bit0 +1280000*x1651_bit0 +1920000*x1652_bit0 +1280000*x1653_bit0 +1280000*x1654_bit0 +1408000*x1655_bit0 +1280000*x1656_bit0 +1280000*x1657_bit0 +1280000*x1658_bit0 +1280000*x1659_bit0 +1280000*x1660_bit0 +1664000*x1661_bit0 +1625600*x1662_bit0 +1779200*x1663_bit0 +768000*x1664_bit0 +1408000*x1665_bit0 +1344000*x1666_bit0 +1344000*x1667_bit0 +1344000*x1668_bit0 +1779200*x1669_bit0 +1920000*x1670_bit0 +263296*x1671_bit0 +1600000*x1672_bit0 +1920000*x1673_bit0 +1024000*x1674_bit0 +1920000*x1675_bit0 +1920000*x1676_bit0 +1280000*x1677_bit0 +1536000*x1678_bit0 +1664000*x1679_bit0 +1920000*x1680_bit0 +1920000*x1681_bit0 +1920000*x1682_bit0 +2560000*x1683_bit0 +2560000*x1684_bit0 +1664000*x1685_bit0 +1664000*x1686_bit0 +1190400*x1687_bit0 +1190400*x1688_bit0 +1190400*x1689_bit0 +1920000*x1690_bit0 +1920000*x1691_bit0 +1152000*x1692_bit0 +1664000*x1693_bit0 +1152000*x1694_bit0 +1664000*x1695_bit0 +1152000*x1696_bit0 +1152000*x1697_bit0 +1152000*x1698_bit0 +1920000*x1699_bit0 +1920000*x1700_bit0 +1920000*x1701_bit0 +2560000*x1702_bit0 +2560000*x1703_bit0 +1920000*x1704_bit0 +1920000*x1705_bit0 +1920000*x1706_bit0 +1920000*x1707_bit0 +1920000*x1708_bit0 +1920000*x1709_bit0 +1920000*x1710_bit0 +1920000*x1711_bit0 +1920000*x1712_bit0 +1920000*x1713_bit0 +2176000*x1714_bit0 +1920000*x1715_bit0 +1920000*x1716_bit0 +1920000*x1717_bit0 +1856000*x1718_bit0 +1920000*x1719_bit0 +1920000*x1720_bit0 +768000*x1721_bit0 +499200*x1722_bit0 +1267200*x1723_bit0 +1267200*x1724_bit0 +1267200*x1725_bit0 +1267200*x1726_bit0 +1267200*x1727_bit0 +1267200*x1728_bit0 +1267200*x1729_bit0 +1267200*x1730_bit0 +1267200*x1731_bit0 +1267200*x1732_bit0 +1267200*x1733_bit0 +1267200*x1734_bit0 +1267200*x1735_bit0 +1267200*x1736_bit0 +636160*x1737_bit0 +1273600*x1738_bit0 +1273600*x1739_bit0 +890880*x1740_bit0 +636160*x1741_bit0 +636160*x1742_bit0 +636160*x1743_bit0 +636160*x1744_bit0 +636160*x1745_bit0 +636160*x1746_bit0 +636160*x1747_bit0 +762880*x1748_bit0 +372224*x1749_bit0 +363520*x1750_bit0 +1267200*x1751_bit0 +1049600*x1752_bit0 +1280000*x1753_bit0 +1267200*x1754_bit0 +1267200*x1755_bit0 +1267200*x1756_bit0 +883200*x1757_bit0 +636160*x1758_bit0 +636160*x1759_bit0 +636160*x1760_bit0 +636160*x1761_bit0 +1273600*x1762_bit0 +1273600*x1763_bit0 +636160*x1764_bit0 +636160*x1765_bit0 +636160*x1766_bit0 +1273600*x1767_bit0 +636160*x1768_bit0 +1273600*x1769_bit0 +1267200*x1770_bit0 +1267200*x1771_bit0 +1139200*x1772_bit0 +1139200*x1773_bit0 +592768*x1774_bit0 +947200*x1775_bit0 +614400*x1776_bit0 +627200*x1777_bit0 +640000*x1778_bit0 +1920000*x1779_bit0 +1920000*x1780_bit0 +1280000*x1781_bit0 +1280000*x1782_bit0 +1920000*x1783_bit0 +1280000*x1784_bit0 +1920000*x1785_bit0 +640000*x1786_bit0 +1280000*x1787_bit0 +1280000*x1788_bit0 +921600*x1789_bit0 +1280000*x1790_bit0 +2560000*x1791_bit0 +1280000*x1792_bit0 +640000*x1793_bit0 +1280000*x1794_bit0 +1920000*x1795_bit0 +1920000*x1796_bit0 +1536000*x1797_bit0 +640000*x1798_bit0 +1280000*x1799_bit0 +1920000*x1800_bit0 +1152000*x1801_bit0 +640000*x1802_bit0 +1280000*x1803_bit0 +640000*x1804_bit0 +1280000*x1805_bit0 +1280000*x1806_bit0 +1920000*x1807_bit0 +640000*x1808_bit0 +640000*x1809_bit0 +1920000*x1810_bit0 +1280000*x1811_bit0 +1536000*x1812_bit0 +1280000*x1813_bit0 +1280000*x1814_bit0 +1920000*x1815_bit0 +2240000*x1816_bit0 +640000*x1817_bit0 +640000*x1818_bit0 +1280000*x1819_bit0 +1920000*x1820_bit0 +640000*x1821_bit0 +640000*x1822_bit0 +1280000*x1823_bit0 +1536000*x1824_bit0 +1139200*x1825_bit0 +1920000*x1826_bit0 +1920000*x1827_bit0 +678400*x1828_bit0 +1920000*x1829_bit0 +1280000*x1830_bit0 +1280000*x1831_bit0 +2240000*x1832_bit0 +1280000*x1833_bit0 +2304000*x1834_bit0 +1280000*x1835_bit0 +1753600*x1836_bit0 +1280000*x1837_bit0 +640000*x1838_bit0 +640000*x1839_bit0 +1920000*x1840_bit0 +1792000*x1841_bit0 +1920000*x1842_bit0 +1920000*x1843_bit0 +1920000*x1844_bit0 +1920000*x1845_bit0 +1920000*x1846_bit0 +1920000*x1847_bit0 +1920000*x1848_bit0 +1920000*x1849_bit0 +1280000*x1850_bit0 +1280000*x1851_bit0 +1920000*x1852_bit0 +1920000*x1853_bit0 +640000*x1854_bit0 +1920000*x1855_bit0 +640000*x1856_bit0 +640000*x1857_bit0 +1689600*x1858_bit0 +1625600*x1859_bit0 +768000*x1860_bit0 +1536000*x1861_bit0 +1536000*x1862_bit0 +1536000*x1863_bit0 +1536000*x1864_bit0 +1536000*x1865_bit0 +1536000*x1866_bit0 +1536000*x1867_bit0 +1779200*x1868_bit0 +768000*x1869_bit0 +768000*x1870_bit0 +1536000*x1871_bit0 +1280000*x1872_bit0 +1920000*x1873_bit0 +896000*x1874_bit0 +768000*x1875_bit0 +1536000*x1876_bit0 +1664000*x1877_bit0 +1280000*x1878_bit0 +1920000*x1879_bit0 +1920000*x1880_bit0 +1920000*x1881_bit0 +1280000*x1882_bit0 +1408000*x1883_bit0 +1280000*x1884_bit0 +1280000*x1885_bit0 +1280000*x1886_bit0 +1280000*x1887_bit0 +1280000*x1888_bit0 +1664000*x1889_bit0 +1625600*x1890_bit0 +1779200*x1891_bit0 +768000*x1892_bit0 +1408000*x1893_bit0 +1344000*x1894_bit0 +1344000*x1895_bit0 +1344000*x1896_bit0 +1779200*x1897_bit0 +263296*x1898_bit0 +1600000*x1899_bit0 +1024000*x1900_bit0 +1920000*x1901_bit0 +1920000*x1902_bit0 +1280000*x1903_bit0 +1536000*x1904_bit0 +1664000*x1905_bit0 +1920000*x1906_bit0 +1920000*x1907_bit0 +1920000*x1908_bit0 +2560000*x1909_bit0 +2560000*x1910_bit0 +1664000*x1911_bit0 +1664000*x1912_bit0 +1190400*x1913_bit0 +1190400*x1914_bit0 +1190400*x1915_bit0 +1920000*x1916_bit0 +1920000*x1917_bit0 +1152000*x1918_bit0 +1664000*x1919_bit0 +1152000*x1920_bit0 +1664000*x1921_bit0 +1152000*x1922_bit0 +1152000*x1923_bit0 +1152000*x1924_bit0 +1920000*x1925_bit0 +1920000*x1926_bit0 +1920000*x1927_bit0 +2560000*x1928_bit0 +2560000*x1929_bit0 +1920000*x1930_bit0 +1920000*x1931_bit0 +1920000*x1932_bit0 +1920000*x1933_bit0 +1920000*x1934_bit0 +1920000*x1935_bit0 +1920000*x1936_bit0 +1920000*x1937_bit0 +1920000*x1938_bit0 +2560000*x1939_bit0 +2176000*x1940_bit0 +1920000*x1941_bit0 +1920000*x1942_bit0 +1920000*x1943_bit0 +1856000*x1944_bit0 +1920000*x1945_bit0 +768000*x1946_bit0 +499200*x1947_bit0 +1267200*x1948_bit0 +1267200*x1949_bit0 +1267200*x1950_bit0 +1267200*x1951_bit0 +1267200*x1952_bit0 +1267200*x1953_bit0 +1267200*x1954_bit0 +1267200*x1955_bit0 +1267200*x1956_bit0 +1267200*x1957_bit0 +1267200*x1958_bit0 +1267200*x1959_bit0 +1267200*x1960_bit0 +1267200*x1961_bit0 +1267200*x1962_bit0 +1273600*x1963_bit0 +1273600*x1964_bit0 +890880*x1965_bit0 +636160*x1966_bit0 +636160*x1967_bit0 +636160*x1968_bit0 +636160*x1969_bit0 +762880*x1970_bit0 +1907200*x1971_bit0 +372224*x1972_bit0 +363520*x1973_bit0 +1267200*x1974_bit0 +1049600*x1975_bit0 +716800*x1976_bit0 +1267200*x1977_bit0 +1267200*x1978_bit0 +1267200*x1979_bit0 +883200*x1980_bit0 +636160*x1981_bit0 +636160*x1982_bit0 +1273600*x1983_bit0 +1273600*x1984_bit0 +636160*x1985_bit0 +636160*x1986_bit0 +1273600*x1987_bit0 +636160*x1988_bit0 +1273600*x1989_bit0 +1267200*x1990_bit0 +1267200*x1991_bit0 +1267200*x1992_bit0 +1267200*x1993_bit0 +1139200*x1994_bit0 +1139200*x1995_bit0 +1139200*x1996_bit0 +1139200*x1997_bit0 +592768*x1998_bit0 +947200*x1999_bit0 +614400*x2000_bit0 +716800*x2001_bit0 +627200*x2002_bit0 +640000*x2003_bit0 +1529600*x2004_bit0 +1920000*x2005_bit0 +640000*x2006_bit0 +1920000*x2007_bit0 +1280000*x2008_bit0 +1920000*x2009_bit0 +1280000*x2010_bit0 +1280000*x2011_bit0 +1280000*x2012_bit0 +921600*x2013_bit0 +1280000*x2014_bit0 +1280000*x2015_bit0 +640000*x2016_bit0 +1280000*x2017_bit0 +1920000*x2018_bit0 +1536000*x2019_bit0 +640000*x2020_bit0 +1280000*x2021_bit0 +1920000*x2022_bit0 +640000*x2023_bit0 +1280000*x2024_bit0 +1280000*x2025_bit0 +1920000*x2026_bit0 +896000*x2027_bit0 +640000*x2028_bit0 +1280000*x2029_bit0 +1536000*x2030_bit0 +1280000*x2031_bit0 +1280000*x2032_bit0 +1881600*x2033_bit0 +640000*x2034_bit0 +1280000*x2035_bit0 +1920000*x2036_bit0 +678400*x2037_bit0 +1920000*x2038_bit0 +1280000*x2039_bit0 +1280000*x2040_bit0 +640000*x2041_bit0 +1280000*x2042_bit0 +2304000*x2043_bit0 +1280000*x2044_bit0 +1753600*x2045_bit0 +1920000*x2046_bit0 +1280000*x2047_bit0 +640000*x2048_bit0 +640000*x2049_bit0 +1920000*x2050_bit0 +1792000*x2051_bit0 +1920000*x2052_bit0 +1561600*x2053_bit0 +1920000*x2054_bit0 +1280000*x2055_bit0 +1280000*x2056_bit0 +1804800*x2057_bit0 +1280000*x2058_bit0 +896000*x2059_bit0 +640000*x2060_bit0 +640000*x2061_bit0 +1689600*x2062_bit0 +1625600*x2063_bit0 +768000*x2064_bit0 +1536000*x2065_bit0 +1536000*x2066_bit0 +1536000*x2067_bit0 +1536000*x2068_bit0 +1536000*x2069_bit0 +1536000*x2070_bit0 +1536000*x2071_bit0 +1779200*x2072_bit0 +768000*x2073_bit0 +768000*x2074_bit0 +1536000*x2075_bit0 +1280000*x2076_bit0 +1920000*x2077_bit0 +896000*x2078_bit0 +768000*x2079_bit0 +1536000*x2080_bit0 +1280000*x2081_bit0 +1920000*x2082_bit0 +1408000*x2083_bit0 +768000*x2084_bit0 +1280000*x2085_bit0 +1280000*x2086_bit0 +1280000*x2087_bit0 +1280000*x2088_bit0 +1280000*x2089_bit0 +1280000*x2090_bit0 +1280000*x2091_bit0 +768000*x2092_bit0 +1280000*x2093_bit0 +1280000*x2094_bit0 +1625600*x2095_bit0 +1779200*x2096_bit0 +1408000*x2097_bit0 +1280000*x2098_bit0 +1408000*x2099_bit0 +1779200*x2100_bit0 +263296*x2101_bit0 +1600000*x2102_bit0 +1689600*x2103_bit0 +1459200*x2104_bit0 +1267200*x2105_bit0 +1920000*x2106_bit0 +1894400*x2107_bit0 +1920000*x2108_bit0 +1536000*x2109_bit0 +1664000*x2110_bit0 +1920000*x2111_bit0 +1920000*x2112_bit0 +1920000*x2113_bit0 +2560000*x2114_bit0 +2560000*x2115_bit0 +1664000*x2116_bit0 +1664000*x2117_bit0 +1190400*x2118_bit0 +1190400*x2119_bit0 +1190400*x2120_bit0 +1920000*x2121_bit0 +1920000*x2122_bit0 +1152000*x2123_bit0 +1664000*x2124_bit0 +1152000*x2125_bit0 +1664000*x2126_bit0 +1152000*x2127_bit0 +1152000*x2128_bit0 +1152000*x2129_bit0 +1920000*x2130_bit0 +1920000*x2131_bit0 +1920000*x2132_bit0 +2560000*x2133_bit0 +2560000*x2134_bit0 +1920000*x2135_bit0 +1920000*x2136_bit0 +1920000*x2137_bit0 +1920000*x2138_bit0 +1920000*x2139_bit0 +1920000*x2140_bit0 +1920000*x2141_bit0 +1843200*x2142_bit0 +1920000*x2143_bit0 +1920000*x2144_bit0 +2176000*x2145_bit0 +1920000*x2146_bit0 +1920000*x2147_bit0 +1920000*x2148_bit0 +1856000*x2149_bit0 +1920000*x2150_bit0 +768000*x2151_bit0 +499200*x2152_bit0 +1267200*x2153_bit0 +1267200*x2154_bit0 +1267200*x2155_bit0 +1267200*x2156_bit0 +1267200*x2157_bit0 +1267200*x2158_bit0 +1267200*x2159_bit0 +1267200*x2160_bit0 +1267200*x2161_bit0 +1267200*x2162_bit0 +1267200*x2163_bit0 +1267200*x2164_bit0 +1267200*x2165_bit0 +1267200*x2166_bit0 +1267200*x2167_bit0 +1273600*x2168_bit0 +1273600*x2169_bit0 +1273600*x2170_bit0 +636160*x2171_bit0 +636160*x2172_bit0 +1273600*x2173_bit0 +636160*x2174_bit0 +636160*x2175_bit0 +1273600*x2176_bit0 +1273600*x2177_bit0 +762880*x2178_bit0 +363520*x2179_bit0 +1049600*x2180_bit0 +1267200*x2181_bit0 +1267200*x2182_bit0 +1267200*x2183_bit0 +883200*x2184_bit0 +636160*x2185_bit0 +1273600*x2186_bit0 +1273600*x2187_bit0 +1273600*x2188_bit0 +636160*x2189_bit0 +636160*x2190_bit0 +1273600*x2191_bit0 +1273600*x2192_bit0 +635520*x2193_bit0 +1273600*x2194_bit0 +1273600*x2195_bit0 +1139200*x2196_bit0 +1139200*x2197_bit0 +592768*x2198_bit0 +947200*x2199_bit0 +614400*x2200_bit0 +627200*x2201_bit0 +640000*x2202_bit0 +1920000*x2203_bit0 +1280000*x2204_bit0 +1280000*x2205_bit0 +1920000*x2206_bit0 +1280000*x2207_bit0 +1280000*x2208_bit0 +921600*x2209_bit0 +2560000*x2210_bit0 +1280000*x2211_bit0 +640000*x2212_bit0 +1280000*x2213_bit0 +1920000*x2214_bit0 +640000*x2215_bit0 +1920000*x2216_bit0 +640000*x2217_bit0 +1280000*x2218_bit0 +640000*x2219_bit0 +1280000*x2220_bit0 +1280000*x2221_bit0 +640000*x2222_bit0 +1920000*x2223_bit0 +1536000*x2224_bit0 +1280000*x2225_bit0 +1920000*x2226_bit0 +2240000*x2227_bit0 +640000*x2228_bit0 +1280000*x2229_bit0 +1536000*x2230_bit0 +1139200*x2231_bit0 +678400*x2232_bit0 +1920000*x2233_bit0 +2240000*x2234_bit0 +2304000*x2235_bit0 +1280000*x2236_bit0 +1280000*x2237_bit0 +640000*x2238_bit0 +640000*x2239_bit0 +1920000*x2240_bit0 +1792000*x2241_bit0 +1280000*x2242_bit0 +1280000*x2243_bit0 +1920000*x2244_bit0 +1920000*x2245_bit0 +640000*x2246_bit0 +1920000*x2247_bit0 +768000*x2248_bit0 +1536000*x2249_bit0 +1536000*x2250_bit0 +1536000*x2251_bit0 +1536000*x2252_bit0 +1536000*x2253_bit0 +1536000*x2254_bit0 +1536000*x2255_bit0 +1779200*x2256_bit0 +768000*x2257_bit0 +768000*x2258_bit0 +1536000*x2259_bit0 +1280000*x2260_bit0 +1920000*x2261_bit0 +896000*x2262_bit0 +768000*x2263_bit0 +1536000*x2264_bit0 +1920000*x2265_bit0 +1920000*x2266_bit0 +1280000*x2267_bit0 +1408000*x2268_bit0 +1280000*x2269_bit0 +1280000*x2270_bit0 +1280000*x2271_bit0 +1280000*x2272_bit0 +1779200*x2273_bit0 +768000*x2274_bit0 +1408000*x2275_bit0 +1344000*x2276_bit0 +1344000*x2277_bit0 +1344000*x2278_bit0 +1779200*x2279_bit0 +263296*x2280_bit0 +1536000*x2281_bit0 +1664000*x2282_bit0 +1152000*x2283_bit0 +1664000*x2284_bit0 +1152000*x2285_bit0 +1152000*x2286_bit0 +1152000*x2287_bit0 +1920000*x2288_bit0 +1920000*x2289_bit0 +2560000*x2290_bit0 +2176000*x2291_bit0 +1920000*x2292_bit0 +1856000*x2293_bit0 +1920000*x2294_bit0 +768000*x2295_bit0 +499200*x2296_bit0 +1267200*x2297_bit0 +1267200*x2298_bit0 +1267200*x2299_bit0 +1267200*x2300_bit0 +1267200*x2301_bit0 +1267200*x2302_bit0 +1267200*x2303_bit0 +1267200*x2304_bit0 +1267200*x2305_bit0 +1267200*x2306_bit0 +1267200*x2307_bit0 +1267200*x2308_bit0 +1267200*x2309_bit0 +1273600*x2310_bit0 +1273600*x2311_bit0 +890880*x2312_bit0 +636160*x2313_bit0 +636160*x2314_bit0 +636160*x2315_bit0 +636160*x2316_bit0 +762880*x2317_bit0 +1907200*x2318_bit0 +1049600*x2319_bit0 +716800*x2320_bit0 +1267200*x2321_bit0 +1267200*x2322_bit0 +1267200*x2323_bit0 +883200*x2324_bit0 +636160*x2325_bit0 +636160*x2326_bit0 +1273600*x2327_bit0 +1273600*x2328_bit0 +636160*x2329_bit0 +636160*x2330_bit0 +1273600*x2331_bit0 +636160*x2332_bit0 +1139200*x2333_bit0 +1139200*x2334_bit0 +1139200*x2335_bit0 +1139200*x2336_bit0 +592768*x2337_bit0 +614400*x2338_bit0 +716800*x2339_bit0 +627200*x2340_bit0 +640000*x2341_bit0 +1529600*x2342_bit0 +1920000*x2343_bit0 +1280000*x2344_bit0 +1280000*x2345_bit0 +1920000*x2346_bit0 +1280000*x2347_bit0 +1920000*x2348_bit0 +640000*x2349_bit0 +1280000*x2350_bit0 +1280000*x2351_bit0 +921600*x2352_bit0 +2560000*x2353_bit0 +1280000*x2354_bit0 +640000*x2355_bit0 +1280000*x2356_bit0 +1920000*x2357_bit0 +1920000*x2358_bit0 +1536000*x2359_bit0 +640000*x2360_bit0 +1920000*x2361_bit0 +1152000*x2362_bit0 +640000*x2363_bit0 +1280000*x2364_bit0 +640000*x2365_bit0 +1280000*x2366_bit0 +1280000*x2367_bit0 +1920000*x2368_bit0 +640000*x2369_bit0 +640000*x2370_bit0 +1920000*x2371_bit0 +2560000*x2372_bit0 +1280000*x2373_bit0 +1536000*x2374_bit0 +1280000*x2375_bit0 +1280000*x2376_bit0 +1920000*x2377_bit0 +2240000*x2378_bit0 +640000*x2379_bit0 +640000*x2380_bit0 +640000*x2381_bit0 +640000*x2382_bit0 +1280000*x2383_bit0 +1536000*x2384_bit0 +1139200*x2385_bit0 +1920000*x2386_bit0 +1920000*x2387_bit0 +678400*x2388_bit0 +1920000*x2389_bit0 +1280000*x2390_bit0 +1280000*x2391_bit0 +2240000*x2392_bit0 +2304000*x2393_bit0 +1280000*x2394_bit0 +1280000*x2395_bit0 +640000*x2396_bit0 +640000*x2397_bit0 +1920000*x2398_bit0 +1792000*x2399_bit0 +1920000*x2400_bit0 +1920000*x2401_bit0 +1920000*x2402_bit0 +1920000*x2403_bit0 +1920000*x2404_bit0 +1280000*x2405_bit0 +1280000*x2406_bit0 +1920000*x2407_bit0 +1920000*x2408_bit0 +640000*x2409_bit0 +1920000*x2410_bit0 +640000*x2411_bit0 +640000*x2412_bit0 +768000*x2413_bit0 +1536000*x2414_bit0 +1536000*x2415_bit0 +1536000*x2416_bit0 +1536000*x2417_bit0 +1536000*x2418_bit0 +1779200*x2419_bit0 +768000*x2420_bit0 +1536000*x2421_bit0 +1280000*x2422_bit0 +1920000*x2423_bit0 +896000*x2424_bit0 +1536000*x2425_bit0 +1664000*x2426_bit0 +1920000*x2427_bit0 +1920000*x2428_bit0 +1280000*x2429_bit0 +1408000*x2430_bit0 +1280000*x2431_bit0 +1280000*x2432_bit0 +1280000*x2433_bit0 +1280000*x2434_bit0 +1664000*x2435_bit0 +1779200*x2436_bit0 +768000*x2437_bit0 +1408000*x2438_bit0 +1344000*x2439_bit0 +1344000*x2440_bit0 +1344000*x2441_bit0 +1779200*x2442_bit0 +263296*x2443_bit0 +1920000*x2444_bit0 +1280000*x2445_bit0 +1664000*x2446_bit0 +1920000*x2447_bit0 +1664000*x2448_bit0 +1152000*x2449_bit0 +1664000*x2450_bit0 +1152000*x2451_bit0 +1152000*x2452_bit0 +1152000*x2453_bit0 +1920000*x2454_bit0 +1920000*x2455_bit0 +1920000*x2456_bit0 +1920000*x2457_bit0 +1920000*x2458_bit0 +2560000*x2459_bit0 +2176000*x2460_bit0 +1920000*x2461_bit0 +1856000*x2462_bit0 +1920000*x2463_bit0 +768000*x2464_bit0 +499200*x2465_bit0 +1267200*x2466_bit0 +1267200*x2467_bit0 +1267200*x2468_bit0 +1267200*x2469_bit0 +1267200*x2470_bit0 +1267200*x2471_bit0 +1267200*x2472_bit0 +1267200*x2473_bit0 +1267200*x2474_bit0 +1267200*x2475_bit0 +1267200*x2476_bit0 +1267200*x2477_bit0 +1273600*x2478_bit0 +1273600*x2479_bit0 +890880*x2480_bit0 +636160*x2481_bit0 +636160*x2482_bit0 +636160*x2483_bit0 +636160*x2484_bit0 +762880*x2485_bit0 +1907200*x2486_bit0 +1049600*x2487_bit0 +716800*x2488_bit0 +1267200*x2489_bit0 +1267200*x2490_bit0 +1267200*x2491_bit0 +883200*x2492_bit0 +636160*x2493_bit0 +636160*x2494_bit0 +1273600*x2495_bit0 +1273600*x2496_bit0 +636160*x2497_bit0 +636160*x2498_bit0 +636160*x2499_bit0 +1267200*x2500_bit0 +1267200*x2501_bit0 +1267200*x2502_bit0 +1139200*x2503_bit0 +1139200*x2504_bit0 +1139200*x2505_bit0 +592768*x2506_bit0 +614400*x2507_bit0 +716800*x2508_bit0 +742400*x2509_bit0 +627200*x2510_bit0 +640000*x2511_bit0 +1529600*x2512_bit0 +1280000*x2513_bit0 +1280000*x2514_bit0 +1280000*x2515_bit0 +1920000*x2516_bit0 +1280000*x2517_bit0 +1280000*x2518_bit0 +921600*x2519_bit0 +2560000*x2520_bit0 +1920000*x2521_bit0 +1280000*x2522_bit0 +1280000*x2523_bit0 +640000*x2524_bit0 +1024000*x2525_bit0 +1152000*x2526_bit0 +1920000*x2527_bit0 +1920000*x2528_bit0 +1536000*x2529_bit0 +640000*x2530_bit0 +1920000*x2531_bit0 +1280000*x2532_bit0 +1920000*x2533_bit0 +1152000*x2534_bit0 +640000*x2535_bit0 +1280000*x2536_bit0 +1280000*x2537_bit0 +1280000*x2538_bit0 +1920000*x2539_bit0 +1920000*x2540_bit0 +1920000*x2541_bit0 +640000*x2542_bit0 +640000*x2543_bit0 +1920000*x2544_bit0 +1280000*x2545_bit0 +1536000*x2546_bit0 +2240000*x2547_bit0 +1920000*x2548_bit0 +640000*x2549_bit0 +1280000*x2550_bit0 +1536000*x2551_bit0 +1139200*x2552_bit0 +678400*x2553_bit0 +1920000*x2554_bit0 +1280000*x2555_bit0 +2240000*x2556_bit0 +921600*x2557_bit0 +640000*x2558_bit0 +640000*x2559_bit0 +1920000*x2560_bit0 +1792000*x2561_bit0 +2240000*x2562_bit0 +2240000*x2563_bit0 +1920000*x2564_bit0 +1920000*x2565_bit0 +2240000*x2566_bit0 +640000*x2567_bit0 +1920000*x2568_bit0 +2560000*x2569_bit0 +2560000*x2570_bit0 +640000*x2571_bit0 +1036800*x2572_bit0 +1036800*x2573_bit0 +896000*x2574_bit0 +768000*x2575_bit0 +768000*x2576_bit0 +896000*x2577_bit0 +1664000*x2578_bit0 +1152000*x2579_bit0 +1664000*x2580_bit0 +1152000*x2581_bit0 +1664000*x2582_bit0 +1152000*x2583_bit0 +1152000*x2584_bit0 +1152000*x2585_bit0 +1920000*x2586_bit0 +2560000*x2587_bit0 +2176000*x2588_bit0 +1920000*x2589_bit0 +1920000*x2590_bit0 +499200*x2591_bit0 +1267200*x2592_bit0 +1267200*x2593_bit0 +1395200*x2594_bit0 +1395200*x2595_bit0 +1267200*x2596_bit0 +1267200*x2597_bit0 +1267200*x2598_bit0 +1267200*x2599_bit0 +1267200*x2600_bit0 +1267200*x2601_bit0 +1267200*x2602_bit0 +1267200*x2603_bit0 +1024000*x2604_bit0 +1024000*x2605_bit0 +1523200*x2606_bit0 +1523200*x2607_bit0 +1907200*x2608_bit0 +1267200*x2609_bit0 +1018880*x2610_bit0 +1273600*x2611_bit0 +1273600*x2612_bit0 +1273600*x2613_bit0 +1267200*x2614_bit0 +1267200*x2615_bit0 +1267200*x2616_bit0 +883200*x2617_bit0 +1024000*x2618_bit0 +896000*x2619_bit0 +896000*x2620_bit0 +896000*x2621_bit0 +1267200*x2622_bit0 +1267200*x2623_bit0 +1139200*x2624_bit0 +1139200*x2625_bit0 +1139200*x2626_bit0 +436480*x2627_bit0 +614400*x2628_bit0 +627200*x2629_bit0 +1529600*x2630_bit0 +1145600*x2631_bit0 +712960*x2632_bit0 +1273600*x2633_bit0 +1273600*x2634_bit0 +1273600*x2635_bit0 +1273600*x2636_bit0 +1273600*x2637_bit0 +1280000*x2638_bit0 +640000*x2639_bit0 +1920000*x2640_bit0 +1280000*x2641_bit0 +640000*x2642_bit0 +921600*x2643_bit0 +2560000*x2644_bit0 +1280000*x2645_bit0 +2112000*x2646_bit0 +1920000*x2647_bit0 +640000*x2648_bit0 +640000*x2649_bit0 +1280000*x2650_bit0 +640000*x2651_bit0 +1280000*x2652_bit0 +1280000*x2653_bit0 +2112000*x2654_bit0 +1920000*x2655_bit0 +640000*x2656_bit0 +1920000*x2657_bit0 +1920000*x2658_bit0 +2240000*x2659_bit0 +640000*x2660_bit0 +640000*x2661_bit0 +1280000*x2662_bit0 +1536000*x2663_bit0 +1139200*x2664_bit0 +678400*x2665_bit0 +1920000*x2666_bit0 +1920000*x2667_bit0 +1920000*x2668_bit0 +2240000*x2669_bit0 +1280000*x2670_bit0 +640000*x2671_bit0 +640000*x2672_bit0 +1920000*x2673_bit0 +1792000*x2674_bit0 +1280000*x2675_bit0 +1920000*x2676_bit0 +1920000*x2677_bit0 +1920000*x2678_bit0 +640000*x2679_bit0 +1920000*x2680_bit0 +1920000*x2681_bit0 +1920000*x2682_bit0 +1280000*x2683_bit0 +768000*x2684_bit0 +1344000*x2685_bit0 +1344000*x2686_bit0 +1664000*x2687_bit0 +1152000*x2688_bit0 +1664000*x2689_bit0 +1152000*x2690_bit0 +1152000*x2691_bit0 +2560000*x2692_bit0 +2176000*x2693_bit0 +1920000*x2694_bit0 +1920000*x2695_bit0 +499200*x2696_bit0 +1267200*x2697_bit0 +1267200*x2698_bit0 +1267200*x2699_bit0 +1267200*x2700_bit0 +1267200*x2701_bit0 +1267200*x2702_bit0 +1267200*x2703_bit0 +890880*x2704_bit0 +1907200*x2705_bit0 +1523200*x2706_bit0 +716800*x2707_bit0 +244352*x2708_bit0 +1273600*x2709_bit0 +1267200*x2710_bit0 +1267200*x2711_bit0 +1267200*x2712_bit0 +883200*x2713_bit0 +636160*x2714_bit0 +636160*x2715_bit0 +636160*x2716_bit0 +1139200*x2717_bit0 +1139200*x2718_bit0 +1139200*x2719_bit0 +614400*x2720_bit0 +716800*x2721_bit0 +742400*x2722_bit0 +1273600*x2723_bit0 +1529600*x2724_bit0 +1273600*x2725_bit0 +1273600*x2726_bit0 +1280000*x2727_bit0 +921600*x2728_bit0 +2560000*x2729_bit0 +1280000*x2730_bit0 +1920000*x2731_bit0 +640000*x2732_bit0 +640000*x2733_bit0 +1280000*x2734_bit0 +640000*x2735_bit0 +1280000*x2736_bit0 +1920000*x2737_bit0 +640000*x2738_bit0 +1920000*x2739_bit0 +2240000*x2740_bit0 +640000*x2741_bit0 +1280000*x2742_bit0 +1536000*x2743_bit0 +1139200*x2744_bit0 +678400*x2745_bit0 +1920000*x2746_bit0 +2240000*x2747_bit0 +1280000*x2748_bit0 +640000*x2749_bit0 +640000*x2750_bit0 +1920000*x2751_bit0 +1792000*x2752_bit0 +1920000*x2753_bit0 +1920000*x2754_bit0 +1920000*x2755_bit0 +1920000*x2756_bit0 +1920000*x2757_bit0 +1920000*x2758_bit0 +640000*x2759_bit0 +1920000*x2760_bit0 +1920000*x2761_bit0 +1920000*x2762_bit0 +1920000*x2763_bit0 +1664000*x2764_bit0 +1152000*x2765_bit0 +1664000*x2766_bit0 +1152000*x2767_bit0 +1152000*x2768_bit0 +2560000*x2769_bit0 +2176000*x2770_bit0 +1920000*x2771_bit0 +1920000*x2772_bit0 +499200*x2773_bit0 +1267200*x2774_bit0 +1267200*x2775_bit0 +1267200*x2776_bit0 +1267200*x2777_bit0 +1267200*x2778_bit0 +1267200*x2779_bit0 +1907200*x2780_bit0 +1523200*x2781_bit0 +716800*x2782_bit0 +1145600*x2783_bit0 +1267200*x2784_bit0 +1267200*x2785_bit0 +1267200*x2786_bit0 +883200*x2787_bit0 +1139200*x2788_bit0 +1139200*x2789_bit0 +1139200*x2790_bit0 +614400*x2791_bit0 +716800*x2792_bit0 +742400*x2793_bit0 +1273600*x2794_bit0 +1529600*x2795_bit0 +1273600*x2796_bit0 +1273600*x2797_bit0 +1280000*x2798_bit0 +1920000*x2799_bit0 +2560000*x2800_bit0 +1280000*x2801_bit0 +1152000*x2802_bit0 +640000*x2803_bit0 +1280000*x2804_bit0 +1920000*x2805_bit0 +2560000*x2806_bit0 +1920000*x2807_bit0 +2240000*x2808_bit0 +1280000*x2809_bit0 +1536000*x2810_bit0 +1139200*x2811_bit0 +2240000*x2812_bit0 +1920000*x2813_bit0 +1920000*x2814_bit0 +1920000*x2815_bit0 +2560000*x2816_bit0 +1267200*x2817_bit0 +1907200*x2818_bit0 +716800*x2819_bit0 +1267200*x2820_bit0 +1267200*x2821_bit0 +1139200*x2822_bit0 +1139200*x2823_bit0 +716800*x2824_bit0 +742400*x2825_bit0 +1529600*x2826_bit0 +1280000*x2827_bit0 +1920000*x2828_bit0 +2560000*x2829_bit0 +1280000*x2830_bit0 +640000*x2831_bit0 +1280000*x2832_bit0 +1920000*x2833_bit0 +1280000*x2834_bit0 +1920000*x2835_bit0 +1920000*x2836_bit0 +1920000*x2837_bit0 +716800*x2838_bit0 +1267200*x2839_bit0 +1267200*x2840_bit0 +1139200*x2841_bit0 +1139200*x2842_bit0 +716800*x2843_bit0 +640000*x2844_bit0 +640000*x2845_bit0 +2112000*x2846_bit0 +1280000*x2847_bit0 +2112000*x2848_bit0 +1920000*x2849_bit0 +2560000*x2850_bit0 +640000*x2851_bit0 +1920000*x2852_bit0 +1920000*x2853_bit0 +1920000*x2854_bit0 +1267200*x2855_bit0 +1523200*x2856_bit0 +244352*x2857_bit0 +1273600*x2858_bit0 +1267200*x2859_bit0 +1139200*x2860_bit0 +742400*x2861_bit0 +1273600*x2862_bit0 +1273600*x2863_bit0 +1273600*x2864_bit0 +640000*x2865_bit0 +640000*x2866_bit0 +2112000*x2867_bit0 +1280000*x2868_bit0 +2112000*x2869_bit0 +1920000*x2870_bit0 +640000*x2871_bit0 +1920000*x2872_bit0 +1920000*x2873_bit0 +1920000*x2874_bit0 +1267200*x2875_bit0 +1523200*x2876_bit0 +244352*x2877_bit0 +1273600*x2878_bit0 +1139200*x2879_bit0 +1273600*x2880_bit0 +1273600*x2881_bit0 +640000*x2882_bit0 +640000*x2883_bit0 +2112000*x2884_bit0 +1280000*x2885_bit0 +2112000*x2886_bit0 +640000*x2887_bit0 +1920000*x2888_bit0 +1920000*x2889_bit0 +1920000*x2890_bit0 +1267200*x2891_bit0 +1523200*x2892_bit0 +244352*x2893_bit0 +1273600*x2894_bit0 +1280000*x2895_bit0 +640000*x2896_bit0 +2304000*x2897_bit0 +2304000*x2898_bit0 +2304000*x2899_bit0 +1075200*x2900_bit0 +1049600*x2901_bit0 +1075200*x2902_bit0 +1075200*x2903_bit0 +1280000*x2904_bit0 +1280000*x2905_bit0 +1267200*x2906_bit0 +1267200*x2907_bit0 +1920000*x2908_bit0 +1920000*x2909_bit0 +1523200*x2910_bit0 +1139200*x2911_bit0 +742400*x2912_bit0 +1273600*x2913_bit0 +1273600*x2914_bit0 +1273600*x2915_bit0 +1920000*x2916_bit0 +1920000*x2917_bit0 +1920000*x2918_bit0 +1523200*x2919_bit0 +1139200*x2920_bit0 +1273600*x2921_bit0 +1273600*x2922_bit0 -125*x2947_bit_10 -250*x2947_bit_9 -500*x2947_bit_8 -1000*x2947_bit_7 -2000*x2947_bit_6 -4000*x2947_bit_5 -8000*x2947_bit_4 -16000*x2947_bit_3 -32000*x2947_bit_2 -64000*x2947_bit_1 -128000*x2947_bit0 -256000*x2947_bit1 -512000*x2947_bit2 -1024000*x2947_bit3 -2048000*x2947_bit4 -4096000*x2947_bit5 -8192000*x2947_bit6 -16384000*x2947_bit7 -32768000*x2947_bit8 -65536000*x2947_bit9 -131072000*x2947_bit10 -262144000*x2947_bit11 -524288000*x2947_bit12 -1048576000*x2947_bit13 -2097152000*x2947_bit14 -4194304000*x2947_bit15 -8388608000*x2947_bit16 -16777216000*x2947_bit17 -33554432000*x2947_bit18 -67108864000*x2947_bit19 = +0;
c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-mkc.opb
s UNKNOWN
c Exit Code: 0
c Total time: 2.553 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.85 0.97 0.98 2/54 8583
Raw data (stat): 8583 (runsolver) R 8582 7475 7474 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 831579523 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 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+2.61503 s]
Raw data (loadavg): 0.86 0.97 0.98 1/53 8583
Raw data (stat): 8583 (runsolver) R 8582 7475 7474 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 831579523 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 0

Child status: 0
Real time (s): 2.61469
CPU time (s): 2.5946
CPU user time (s): 2.11668
CPU system time (s): 0.477927
CPU usage (%): 99.2317
Max. virtual memory (Kb): 1028
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####