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-fiber.opb
MD5SUM	02cc3bacd8064c2ceecf74a8d0a8ab0f
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	108097879
Optimality of the best value was proved	NO
Number of terms in the objective function	1254
Biggest coefficient in the objective function	72966962
Number of bits for the biggest coefficient in the objective function	27
Sum of the numbers in the objective function	4807778524
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	4807778524
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	95.3155
Number of variables	2574
Total number of constraints	1617
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	1290
Number of constraints which are nor clauses,nor cardinality constraints	327
Minimum length of a constraint	1
Maximum length of a constraint	61
Trace number 34510

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-27 23:44:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12540 boxname=wulflinc31 idbench=965 idsolver=8 numberseed=0
MD5SUM SOLVER: 4b637b3b6117f2add1a6288e91336322  /oldhome/oroussel/solvers/vallstSAT2005PB.sh
MD5SUM BENCH:  02cc3bacd8064c2ceecf74a8d0a8ab0f  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-fiber.opb
REAL COMMAND:  vallstSAT2005PB.sh /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-fiber.opb 0
IDLAUNCH: 12540
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        918320 kB
Buffers:         20304 kB
Cached:          72960 kB
SwapCached:       1052 kB
Active:          52256 kB
Inactive:        43260 kB
HighTotal:      131008 kB
HighFree:        66388 kB
LowTotal:       903652 kB
LowFree:        851932 kB
SwapTotal:     2097892 kB
SwapFree:      2095928 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5088 kB
Slab:            15072 kB
Committed_AS:    63748 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 23:48:32 (client local time) WITH STATUS 30 IN 233.037 SECONDS
stats: 12540 0 233.037 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
1:
seed: 0
Nr of vars set: 443  (#equs: 0)
Nr of vars set: 443  (#equs: 53)
#decisions: 2873917;  #end-nodes: 1620330;
#proof improvement attempts: 0;  #restarts: 3273
Current batch, end-nodes: 856 / 914 (898)
#axs: 750, #non-axs: 751
tight: meta-meta: start: 3, end: 4;  meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14;  meta: start: 30, end (keep): 50
result: model found (1)
Model found with constant:  1465459157 (3342319366:>=*);
Model found with constant:
  (pushed:) 4294967295 (512811228:>=*)

With an increment of the last pushed constant, a proof of false was found.
result: proof of false found (0)
seed: 0
Nr of vars set: 443  (#equs: 53)
Time taken: 3 min, 52 sec
times:
0m0.016s 0m0.010s
3m28.432s 0m23.668s
v -x1_bit0 -x2_bit0  x3_bit0 -x4_bit0 -x5_bit0 -x6_bit0 -x7_bit0  x8_bit0 -x9_bit0 -x10_bit0 -x11_bit0 -x12_bit0 -x13_bit0 -x14_bit0 -x15_bit0 -x16_bit0 -x17_bit0 -x18_bit0  x19_bit0  x20_bit0 -x21_bit0  x22_bit0  x23_bit0 -x24_bit0 -x25_bit0 -x26_bit0 -x27_bit0 -x28_bit0 -x29_bit0 -x30_bit0  x31_bit0 -x32_bit0 -x33_bit0 -x34_bit0 -x35_bit0 -x36_bit0 -x37_bit0  x38_bit0 -x39_bit0 -x40_bit0  x41_bit0  x42_bit0 -x43_bit0 -x44_bit0  x45_bit0 -x46_bit0 -x47_bit0  x48_bit0  x49_bit0 -x50_bit0  x51_bit0  x52_bit0 -x53_bit0 -x54_bit0  x55_bit0  x56_bit0 -x57_bit0 -x58_bit0 -x59_bit0 -x60_bit0  x61_bit0  x62_bit0 -x63_bit0 -x64_bit0 -x65_bit0 -x66_bit0 -x67_bit0 -x68_bit0 -x69_bit0 -x70_bit0 -x71_bit0 -x72_bit0  x73_bit0  x74_bit0 -x75_bit0 -x76_bit0  x77_bit0  x78_bit0 -x79_bit0 -x80_bit0 -x81_bit0 -x82_bit0  x83_bit0  x84_bit0 -x85_bit0 -x86_bit0 -x87_bit0 -x88_bit0 -x89_bit0 -x90_bit0 -x91_bit0 -x92_bit0 -x93_bit0 -x94_bit0 -x95_bit0 -x96_bit0 -x97_bit0 -x98_bit0 -x99_bit0 -x100_bit0 -x101_bit0 -x102_bit0 -x103_bit0 -x104_bit0 -x105_bit0 -x106_bit0  x107_bit0  x108_bit0 -x109_bit0 -x110_bit0 -x111_bit0 -x112_bit0 -x113_bit0 -x114_bit0  x115_bit0 -x116_bit0 -x117_bit0 -x118_bit0 -x119_bit0 -x120_bit0 -x121_bit0 -x122_bit0 -x123_bit0  x124_bit0 -x125_bit0 -x126_bit0  x127_bit0 -x128_bit0 -x129_bit0 -x130_bit0 -x131_bit0  x132_bit0 -x133_bit0  x134_bit0  x135_bit0 -x136_bit0  x137_bit0  x138_bit0  x139_bit0  x140_bit0  x141_bit0 -x142_bit0 -x143_bit0  x144_bit0 -x145_bit0 -x146_bit0 -x147_bit0  x148_bit0  x149_bit0 -x150_bit0 -x151_bit0 -x152_bit0 -x153_bit0 -x154_bit0 -x155_bit0 -x156_bit0 -x157_bit0 -x158_bit0  x159_bit0 -x160_bit0 -x161_bit0  x162_bit0 -x163_bit0 -x164_bit0 -x165_bit0 -x166_bit0 -x167_bit0 -x168_bit0 -x169_bit0 -x170_bit0 -x171_bit0 -x172_bit0  x173_bit0 -x174_bit0 -x175_bit0  x176_bit0 -x177_bit0 -x178_bit0  x179_bit0  x180_bit0  x181_bit0  x182_bit0 -x183_bit0 -x184_bit0  x185_bit0 -x186_bit0 -x187_bit0 -x188_bit0 -x189_bit0 -x190_bit0 -x191_bit0 -x192_bit0  x193_bit0 -x194_bit0 -x195_bit0 -x196_bit0 -x197_bit0  x198_bit0  x199_bit0  x200_bit0  x201_bit0  x202_bit0 -x203_bit0 -x204_bit0  x205_bit0 -x206_bit0 -x207_bit0  x208_bit0 -x209_bit0  x210_bit0 -x211_bit0  x212_bit0  x213_bit0 -x214_bit0 -x215_bit0 -x216_bit0 -x217_bit0  x218_bit0  x219_bit0 -x220_bit0 -x221_bit0  x222_bit0 -x223_bit0 -x224_bit0 -x225_bit0  x226_bit0 -x227_bit0 -x228_bit0 -x229_bit0 -x230_bit0 -x231_bit0  x232_bit0 -x233_bit0 -x234_bit0 -x235_bit0  x236_bit0  x237_bit0 -x238_bit0 -x239_bit0  x240_bit0 -x241_bit0 -x242_bit0 -x243_bit0 -x244_bit0 -x245_bit0 -x246_bit0 -x247_bit0 -x248_bit0 -x249_bit0 -x250_bit0  x251_bit0 -x252_bit0 -x253_bit0  x254_bit0 -x255_bit0  x256_bit0 -x257_bit0  x258_bit0  x259_bit0 -x260_bit0  x261_bit0 -x262_bit0  x263_bit0 -x264_bit0 -x265_bit0 -x266_bit0 -x267_bit0 -x268_bit0  x269_bit0 -x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 -x275_bit0  x276_bit0 -x277_bit0 -x278_bit0  x279_bit0 -x280_bit0 -x281_bit0 -x282_bit0  x283_bit0 -x284_bit0  x285_bit0 -x286_bit0 -x287_bit0  x288_bit0 -x289_bit0  x290_bit0  x291_bit0 -x292_bit0  x293_bit0 -x294_bit0  x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 -x299_bit0 -x300_bit0 -x301_bit0 -x302_bit0 -x303_bit0  x304_bit0 -x305_bit0 -x306_bit0 -x307_bit0 -x308_bit0  x309_bit0 -x310_bit0 -x311_bit0 -x312_bit0 -x313_bit0 -x314_bit0  x315_bit0 -x316_bit0 -x317_bit0  x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0  x329_bit0 -x330_bit0 -x331_bit0  x332_bit0 -x333_bit0  x334_bit0 -x335_bit0 -x336_bit0  x337_bit0 -x338_bit0 -x339_bit0 -x340_bit0  x341_bit0 -x342_bit0  x343_bit0  x344_bit0 -x345_bit0 -x346_bit0 -x347_bit0 -x348_bit0  x349_bit0 -x350_bit0 -x351_bit0 -x352_bit0 -x353_bit0 -x354_bit0 -x355_bit0 -x356_bit0  x357_bit0  x358_bit0  x359_bit0  x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 -x366_bit0  x367_bit0  x368_bit0  x369_bit0  x370_bit0 -x371_bit0  x372_bit0  x373_bit0 -x374_bit0  x375_bit0  x376_bit0 -x377_bit0 -x378_bit0 -x379_bit0 -x380_bit0 -x381_bit0 -x382_bit0 -x383_bit0  x384_bit0 -x385_bit0 -x386_bit0  x387_bit0 -x388_bit0 -x389_bit0  x390_bit0 -x391_bit0 -x392_bit0  x393_bit0 -x394_bit0 -x395_bit0  x396_bit0  x397_bit0  x398_bit0 -x399_bit0 -x400_bit0 -x401_bit0 -x402_bit0 -x403_bit0 -x404_bit0 -x405_bit0  x406_bit0  x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0  x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 -x416_bit0  x417_bit0 -x418_bit0  x419_bit0 -x420_bit0 -x421_bit0 -x422_bit0 -x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x427_bit0 -x428_bit0 -x429_bit0 -x430_bit0 -x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 -x436_bit0 -x437_bit0 -x438_bit0 -x439_bit0 -x440_bit0  x441_bit0 -x442_bit0 -x443_bit0 -x444_bit0  x445_bit0  x446_bit0 -x447_bit0 -x448_bit0 -x449_bit0 -x450_bit0  x451_bit0 -x452_bit0 -x453_bit0 -x454_bit0 -x455_bit0 -x456_bit0 -x457_bit0 -x458_bit0  x459_bit0  x460_bit0 -x461_bit0 -x462_bit0 -x463_bit0 -x464_bit0  x465_bit0 -x466_bit0 -x467_bit0 -x468_bit0 -x469_bit0 -x470_bit0 -x471_bit0 -x472_bit0  x473_bit0  x474_bit0 -x475_bit0 -x476_bit0 -x477_bit0 -x478_bit0  x479_bit0  x480_bit0 -x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 -x485_bit0 -x486_bit0  x487_bit0  x488_bit0 -x489_bit0 -x490_bit0 -x491_bit0 -x492_bit0 -x493_bit0  x494_bit0  x495_bit0 -x496_bit0 -x497_bit0 -x498_bit0 -x499_bit0 -x500_bit0 -x501_bit0 -x502_bit0  x503_bit0 -x504_bit0 -x505_bit0 -x506_bit0 -x507_bit0 -x508_bit0 -x509_bit0 -x510_bit0  x511_bit0 -x512_bit0 -x513_bit0 -x514_bit0 -x515_bit0  x516_bit0 -x517_bit0 -x518_bit0 -x519_bit0  x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 -x524_bit0  x525_bit0  x526_bit0  x527_bit0  x528_bit0 -x529_bit0 -x530_bit0  x531_bit0  x532_bit0 -x533_bit0 -x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 -x540_bit0  x541_bit0 -x542_bit0 -x543_bit0 -x544_bit0 -x545_bit0 -x546_bit0 -x547_bit0 -x548_bit0 -x549_bit0 -x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 -x556_bit0  x557_bit0 -x558_bit0  x559_bit0 -x560_bit0 -x561_bit0 -x562_bit0 -x563_bit0 -x564_bit0  x565_bit0 -x566_bit0 -x567_bit0 -x568_bit0  x569_bit0 -x570_bit0 -x571_bit0  x572_bit0 -x573_bit0 -x574_bit0 -x575_bit0  x576_bit0  x577_bit0 -x578_bit0 -x579_bit0 -x580_bit0 -x581_bit0 -x582_bit0 -x583_bit0 -x584_bit0 -x585_bit0 -x586_bit0 -x587_bit0 -x588_bit0  x589_bit0  x590_bit0 -x591_bit0 -x592_bit0 -x593_bit0 -x594_bit0 -x595_bit0  x596_bit0 -x597_bit0  x598_bit0  x599_bit0 -x600_bit0  x601_bit0 -x602_bit0 -x603_bit0  x604_bit0 -x605_bit0 -x606_bit0 -x607_bit0  x608_bit0 -x609_bit0 -x610_bit0 -x611_bit0 -x612_bit0 -x613_bit0 -x614_bit0  x615_bit0 -x616_bit0 -x617_bit0 -x618_bit0 -x619_bit0 -x620_bit0 -x621_bit0  x622_bit0 -x623_bit0 -x624_bit0 -x625_bit0 -x626_bit0 -x627_bit0 -x628_bit0 -x629_bit0 -x630_bit0 -x631_bit0 -x632_bit0 -x633_bit0 -x634_bit0  x635_bit0 -x636_bit0  x637_bit0 -x638_bit0 -x639_bit0 -x640_bit0 -x641_bit0 -x642_bit0  x643_bit0 -x644_bit0 -x645_bit0 -x646_bit0 -x647_bit0  x648_bit0  x649_bit0  x650_bit0  x651_bit0 -x652_bit0 -x653_bit0  x654_bit0  x655_bit0 -x656_bit0 -x657_bit0 -x658_bit0 -x659_bit0 -x660_bit0 -x661_bit0 -x662_bit0 -x663_bit0 -x664_bit0 -x665_bit0  x666_bit0  x667_bit0 -x668_bit0  x669_bit0 -x670_bit0 -x671_bit0  x672_bit0  x673_bit0 -x674_bit0  x675_bit0 -x676_bit0 -x677_bit0  x678_bit0 -x679_bit0  x680_bit0  x681_bit0 -x682_bit0  x683_bit0 -x684_bit0 -x685_bit0 -x686_bit0 -x687_bit0 -x688_bit0 -x689_bit0  x690_bit0 -x691_bit0 -x692_bit0 -x693_bit0  x694_bit0 -x695_bit0 -x696_bit0  x697_bit0 -x698_bit0  x699_bit0  x700_bit0 -x701_bit0 -x702_bit0 -x703_bit0 -x704_bit0  x705_bit0 -x706_bit0 -x707_bit0  x708_bit0 -x709_bit0 -x710_bit0 -x711_bit0 -x712_bit0  x713_bit0 -x714_bit0  x715_bit0 -x716_bit0 -x717_bit0 -x718_bit0  x719_bit0 -x720_bit0 -x721_bit0 -x722_bit0 -x723_bit0 -x724_bit0  x725_bit0 -x726_bit0 -x727_bit0  x728_bit0 -x729_bit0 -x730_bit0 -x731_bit0 -x732_bit0  x733_bit0 -x734_bit0 -x735_bit0 -x736_bit0 -x737_bit0 -x738_bit0 -x739_bit0 -x740_bit0 -x741_bit0 -x742_bit0 -x743_bit0 -x744_bit0 -x745_bit0 -x746_bit0  x747_bit0  x748_bit0  x749_bit0  x750_bit0  x751_bit0  x752_bit0  x753_bit0  x754_bit0 -x755_bit0 -x756_bit0 -x757_bit0 -x758_bit0 -x759_bit0 -x760_bit0 -x761_bit0 -x762_bit0 -x763_bit0 -x764_bit0 -x765_bit0 -x766_bit0 -x767_bit0 -x768_bit0 -x769_bit0 -x770_bit0 -x771_bit0 -x772_bit0 -x773_bit0 -x774_bit0 -x775_bit0 -x776_bit0 -x777_bit0 -x778_bit0  x779_bit0  x780_bit0 -x781_bit0 -x782_bit0  x783_bit0 -x784_bit0 -x785_bit0  x786_bit0 -x787_bit0 -x788_bit0 -x789_bit0 -x790_bit0 -x791_bit0 -x792_bit0 -x793_bit0 -x794_bit0 -x795_bit0  x796_bit0  x797_bit0 -x798_bit0 -x799_bit0 -x800_bit0 -x801_bit0 -x802_bit0  x803_bit0 -x804_bit0 -x805_bit0  x806_bit0 -x807_bit0 -x808_bit0 -x809_bit0 -x810_bit0  x811_bit0 -x812_bit0 -x813_bit0 -x814_bit0 -x815_bit0 -x816_bit0 -x817_bit0 -x818_bit0 -x819_bit0 -x820_bit0 -x821_bit0  x822_bit0  x823_bit0 -x824_bit0 -x825_bit0 -x826_bit0 -x827_bit0  x828_bit0 -x829_bit0 -x830_bit0 -x831_bit0 -x832_bit0  x833_bit0  x834_bit0 -x835_bit0 -x836_bit0 -x837_bit0 -x838_bit0  x839_bit0 -x840_bit0 -x841_bit0  x842_bit0  x843_bit0  x844_bit0  x845_bit0  x846_bit0 -x847_bit0 -x848_bit0  x849_bit0  x850_bit0 -x851_bit0 -x852_bit0  x853_bit0  x854_bit0 -x855_bit0  x856_bit0  x857_bit0  x858_bit0  x859_bit0  x860_bit0  x861_bit0  x862_bit0  x863_bit0  x864_bit0  x865_bit0  x866_bit0  x867_bit0 -x868_bit0 -x869_bit0  x870_bit0 -x871_bit0 -x872_bit0 -x873_bit0  x874_bit0  x875_bit0  x876_bit0  x877_bit0  x878_bit0  x879_bit0 -x880_bit0  x881_bit0 -x882_bit0 -x883_bit0  x884_bit0  x885_bit0  x886_bit0  x887_bit0  x888_bit0  x889_bit0 -x890_bit0  x891_bit0  x892_bit0  x893_bit0  x894_bit0  x895_bit0 -x896_bit0  x897_bit0 -x898_bit0 -x899_bit0  x900_bit0 -x901_bit0 -x902_bit0 -x903_bit0  x904_bit0 -x905_bit0  x906_bit0  x907_bit0  x908_bit0  x909_bit0  x910_bit0  x911_bit0  x912_bit0 -x913_bit0 -x914_bit0 -x915_bit0  x916_bit0  x917_bit0 -x918_bit0 -x919_bit0 -x920_bit0  x921_bit0  x922_bit0  x923_bit0  x924_bit0  x925_bit0  x926_bit0  x927_bit0  x928_bit0  x929_bit0  x930_bit0  x931_bit0 -x932_bit0  x933_bit0  x934_bit0  x935_bit0  x936_bit0 -x937_bit0  x938_bit0  x939_bit0  x940_bit0 -x941_bit0 -x942_bit0  x943_bit0 -x944_bit0  x945_bit0  x946_bit0  x947_bit0  x948_bit0 -x949_bit0 -x950_bit0  x951_bit0  x952_bit0  x953_bit0  x954_bit0  x955_bit0 -x956_bit0  x957_bit0 -x958_bit0  x959_bit0  x960_bit0  x961_bit0  x962_bit0  x963_bit0  x964_bit0 -x965_bit0  x966_bit0  x967_bit0 -x968_bit0  x969_bit0  x970_bit0  x971_bit0  x972_bit0  x973_bit0 -x974_bit0  x975_bit0  x976_bit0  x977_bit0  x978_bit0  x979_bit0  x980_bit0  x981_bit0  x982_bit0  x983_bit0 -x984_bit0  x985_bit0  x986_bit0  x987_bit0  x988_bit0  x989_bit0  x990_bit0  x991_bit0  x992_bit0 -x993_bit0  x994_bit0  x995_bit0 -x996_bit0 -x997_bit0  x998_bit0 -x999_bit0  x1000_bit0 -x1001_bit0  x1002_bit0  x1003_bit0  x1004_bit0  x1005_bit0  x1006_bit0  x1007_bit0  x1008_bit0 -x1009_bit0  x1010_bit0  x1011_bit0  x1012_bit0 -x1013_bit0  x1014_bit0  x1015_bit0  x1016_bit0  x1017_bit0 -x1018_bit0  x1019_bit0  x1020_bit0  x1021_bit0  x1022_bit0 -x1023_bit0 -x1024_bit0 -x1025_bit0  x1026_bit0 -x1027_bit0  x1028_bit0 -x1029_bit0 -x1030_bit0 -x1031_bit0  x1032_bit0 -x1033_bit0 -x1034_bit0 -x1035_bit0  x1036_bit0  x1037_bit0 -x1038_bit0  x1039_bit0 -x1040_bit0  x1041_bit0  x1042_bit0  x1043_bit0  x1044_bit0  x1045_bit0  x1046_bit0  x1047_bit0  x1048_bit0  x1049_bit0  x1050_bit0  x1051_bit0  x1052_bit0  x1053_bit0  x1054_bit0  x1055_bit0  x1056_bit0  x1057_bit0  x1058_bit0  x1059_bit0 -x1060_bit0  x1061_bit0  x1062_bit0  x1063_bit0 -x1064_bit0 -x1065_bit0 -x1066_bit0  x1067_bit0  x1068_bit0  x1069_bit0  x1070_bit0  x1071_bit0  x1072_bit0 -x1073_bit0 -x1074_bit0  x1075_bit0  x1076_bit0  x1077_bit0 -x1078_bit0  x1079_bit0  x1080_bit0 -x1081_bit0 -x1082_bit0 -x1083_bit0  x1084_bit0  x1085_bit0  x1086_bit0  x1087_bit0  x1088_bit0  x1089_bit0  x1090_bit0  x1091_bit0  x1092_bit0 -x1093_bit0  x1094_bit0  x1095_bit0  x1096_bit0  x1097_bit0 -x1098_bit0 -x1099_bit0  x1100_bit0  x1101_bit0 -x1102_bit0  x1103_bit0  x1104_bit0 -x1105_bit0  x1106_bit0  x1107_bit0 -x1108_bit0  x1109_bit0  x1110_bit0  x1111_bit0  x1112_bit0  x1113_bit0  x1114_bit0 -x1115_bit0 -x1116_bit0  x1117_bit0 -x1118_bit0 -x1119_bit0  x1120_bit0  x1121_bit0  x1122_bit0  x1123_bit0  x1124_bit0  x1125_bit0  x1126_bit0  x1127_bit0 -x1128_bit0 -x1129_bit0  x1130_bit0  x1131_bit0  x1132_bit0  x1133_bit0  x1134_bit0  x1135_bit0  x1136_bit0  x1137_bit0  x1138_bit0  x1139_bit0  x1140_bit0  x1141_bit0  x1142_bit0  x1143_bit0 -x1144_bit0  x1145_bit0 -x1146_bit0  x1147_bit0  x1148_bit0  x1149_bit0  x1150_bit0  x1151_bit0  x1152_bit0  x1153_bit0 -x1154_bit0 -x1155_bit0  x1156_bit0  x1157_bit0  x1158_bit0 -x1159_bit0 -x1160_bit0 -x1161_bit0  x1162_bit0  x1163_bit0  x1164_bit0  x1165_bit0  x1166_bit0  x1167_bit0 -x1168_bit0  x1169_bit0 -x1170_bit0 -x1171_bit0  x1172_bit0 -x1173_bit0  x1174_bit0  x1175_bit0 -x1176_bit0  x1177_bit0  x1178_bit0  x1179_bit0  x1180_bit0  x1181_bit0 -x1182_bit0 -x1183_bit0  x1184_bit0  x1185_bit0  x1186_bit0  x1187_bit0  x1188_bit0  x1189_bit0  x1190_bit0  x1191_bit0  x1192_bit0  x1193_bit0 -x1194_bit0  x1195_bit0  x1196_bit0  x1197_bit0  x1198_bit0  x1199_bit0  x1200_bit0  x1201_bit0  x1202_bit0  x1203_bit0 -x1204_bit0  x1205_bit0 -x1206_bit0  x1207_bit0  x1208_bit0  x1209_bit0  x1210_bit0  x1211_bit0  x1212_bit0  x1213_bit0  x1214_bit0  x1215_bit0  x1216_bit0 -x1217_bit0 -x1218_bit0  x1219_bit0  x1220_bit0  x1221_bit0  x1222_bit0  x1223_bit0 -x1224_bit0  x1225_bit0  x1226_bit0  x1227_bit0  x1228_bit0 -x1229_bit0 -x1230_bit0  x1231_bit0 -x1232_bit0  x1233_bit0  x1234_bit0 -x1235_bit0 -x1236_bit0  x1237_bit0  x1238_bit0 -x1239_bit0  x1240_bit0  x1241_bit0  x1242_bit0 -x1243_bit0  x1244_bit0  x1245_bit0  x1246_bit0  x1247_bit0  x1248_bit0 -x1249_bit0  x1250_bit0  x1251_bit0 -x1252_bit0 -x1253_bit0  x1254_bit0 -x1255_bit_10 -x1255_bit_9 -x1255_bit_8 -x1255_bit_7 -x1255_bit_6 -x1255_bit_5 -x1255_bit_4 -x1255_bit_3 -x1255_bit_2 -x1255_bit_1 -x1255_bit0 -x1255_bit1 -x1255_bit2 -x1255_bit3 -x1255_bit4 -x1255_bit5 -x1255_bit6  x1255_bit7 -x1255_bit8  x1255_bit9 -x1255_bit10 -x1255_bit11 -x1255_bit12 -x1255_bit13 -x1255_bit14 -x1255_bit15 -x1255_bit16 -x1255_bit17 -x1255_bit18 -x1255_bit19 -x1264_bit_10 -x1264_bit_9 -x1264_bit_8 -x1264_bit_7 -x1264_bit_6 -x1264_bit_5 -x1264_bit_4 -x1264_bit_3 -x1264_bit_2 -x1264_bit_1 -x1264_bit0 -x1264_bit1 -x1264_bit2 -x1264_bit3 -x1264_bit4 -x1264_bit5 -x1264_bit6 -x1264_bit7 -x1264_bit8  x1264_bit9 -x1264_bit10 -x1264_bit11 -x1264_bit12 -x1264_bit13 -x1264_bit14 -x1264_bit15 -x1264_bit16 -x1264_bit17 -x1264_bit18 -x1264_bit19 -x1265_bit_10 -x1265_bit_9 -x1265_bit_8 -x1265_bit_7 -x1265_bit_6 -x1265_bit_5 -x1265_bit_4 -x1265_bit_3 -x1265_bit_2 -x1265_bit_1 -x1265_bit0 -x1265_bit1 -x1265_bit2 -x1265_bit3  x1265_bit4 -x1265_bit5 -x1265_bit6 -x1265_bit7  x1265_bit8 -x1265_bit9 -x1265_bit10 -x1265_bit11 -x1265_bit12 -x1265_bit13 -x1265_bit14 -x1265_bit15 -x1265_bit16 -x1265_bit17 -x1265_bit18 -x1265_bit19 -x1266_bit_10 -x1266_bit_9 -x1266_bit_8 -x1266_bit_7 -x1266_bit_6 -x1266_bit_5 -x1266_bit_4 -x1266_bit_3 -x1266_bit_2 -x1266_bit_1 -x1266_bit0 -x1266_bit1 -x1266_bit2 -x1266_bit3  x1266_bit4 -x1266_bit5 -x1266_bit6 -x1266_bit7 -x1266_bit8  x1266_bit9 -x1266_bit10 -x1266_bit11 -x1266_bit12 -x1266_bit13 -x1266_bit14 -x1266_bit15 -x1266_bit16 -x1266_bit17 -x1266_bit18 -x1266_bit19 -x1267_bit_10 -x1267_bit_9 -x1267_bit_8 -x1267_bit_7 -x1267_bit_6 -x1267_bit_5 -x1267_bit_4 -x1267_bit_3 -x1267_bit_2 -x1267_bit_1 -x1267_bit0 -x1267_bit1 -x1267_bit2 -x1267_bit3  x1267_bit4 -x1267_bit5 -x1267_bit6 -x1267_bit7  x1267_bit8 -x1267_bit9 -x1267_bit10 -x1267_bit11 -x1267_bit12 -x1267_bit13 -x1267_bit14 -x1267_bit15 -x1267_bit16 -x1267_bit17 -x1267_bit18 -x1267_bit19 -x1268_bit_10 -x1268_bit_9 -x1268_bit_8 -x1268_bit_7 -x1268_bit_6 -x1268_bit_5 -x1268_bit_4 -x1268_bit_3 -x1268_bit_2 -x1268_bit_1 -x1268_bit0 -x1268_bit1 -x1268_bit2 -x1268_bit3 -x1268_bit4 -x1268_bit5 -x1268_bit6 -x1268_bit7  x1268_bit8 -x1268_bit9 -x1268_bit10 -x1268_bit11 -x1268_bit12 -x1268_bit13 -x1268_bit14 -x1268_bit15 -x1268_bit16 -x1268_bit17 -x1268_bit18 -x1268_bit19 -x1269_bit_10 -x1269_bit_9 -x1269_bit_8 -x1269_bit_7 -x1269_bit_6 -x1269_bit_5 -x1269_bit_4 -x1269_bit_3 -x1269_bit_2 -x1269_bit_1 -x1269_bit0 -x1269_bit1 -x1269_bit2  x1269_bit3 -x1269_bit4 -x1269_bit5 -x1269_bit6 -x1269_bit7  x1269_bit8 -x1269_bit9 -x1269_bit10 -x1269_bit11 -x1269_bit12 -x1269_bit13 -x1269_bit14 -x1269_bit15 -x1269_bit16 -x1269_bit17 -x1269_bit18 -x1269_bit19 -x1270_bit_10 -x1270_bit_9 -x1270_bit_8 -x1270_bit_7 -x1270_bit_6 -x1270_bit_5 -x1270_bit_4 -x1270_bit_3 -x1270_bit_2 -x1270_bit_1 -x1270_bit0 -x1270_bit1 -x1270_bit2 -x1270_bit3 -x1270_bit4 -x1270_bit5 -x1270_bit6  x1270_bit7  x1270_bit8 -x1270_bit9 -x1270_bit10 -x1270_bit11 -x1270_bit12 -x1270_bit13 -x1270_bit14 -x1270_bit15 -x1270_bit16 -x1270_bit17 -x1270_bit18 -x1270_bit19 -x1271_bit_10 -x1271_bit_9 -x1271_bit_8 -x1271_bit_7 -x1271_bit_6 -x1271_bit_5 -x1271_bit_4 -x1271_bit_3 -x1271_bit_2 -x1271_bit_1 -x1271_bit0 -x1271_bit1 -x1271_bit2 -x1271_bit3 -x1271_bit4  x1271_bit5  x1271_bit6 -x1271_bit7  x1271_bit8 -x1271_bit9 -x1271_bit10 -x1271_bit11 -x1271_bit12 -x1271_bit13 -x1271_bit14 -x1271_bit15 -x1271_bit16 -x1271_bit17 -x1271_bit18 -x1271_bit19 -x1272_bit_10 -x1272_bit_9 -x1272_bit_8 -x1272_bit_7 -x1272_bit_6 -x1272_bit_5 -x1272_bit_4 -x1272_bit_3 -x1272_bit_2 -x1272_bit_1 -x1272_bit0  x1272_bit1 -x1272_bit2 -x1272_bit3 -x1272_bit4 -x1272_bit5 -x1272_bit6 -x1272_bit7 -x1272_bit8  x1272_bit9 -x1272_bit10 -x1272_bit11 -x1272_bit12 -x1272_bit13 -x1272_bit14 -x1272_bit15 -x1272_bit16 -x1272_bit17 -x1272_bit18 -x1272_bit19 -x1273_bit_10 -x1273_bit_9 -x1273_bit_8 -x1273_bit_7 -x1273_bit_6 -x1273_bit_5 -x1273_bit_4 -x1273_bit_3 -x1273_bit_2 -x1273_bit_1 -x1273_bit0 -x1273_bit1 -x1273_bit2 -x1273_bit3 -x1273_bit4 -x1273_bit5 -x1273_bit6 -x1273_bit7  x1273_bit8 -x1273_bit9 -x1273_bit10 -x1273_bit11 -x1273_bit12 -x1273_bit13 -x1273_bit14 -x1273_bit15 -x1273_bit16 -x1273_bit17 -x1273_bit18 -x1273_bit19 -x1256_bit_10 -x1256_bit_9 -x1256_bit_8 -x1256_bit_7 -x1256_bit_6 -x1256_bit_5 -x1256_bit_4 -x1256_bit_3 -x1256_bit_2 -x1256_bit_1 -x1256_bit0 -x1256_bit1  x1256_bit2 -x1256_bit3 -x1256_bit4 -x1256_bit5 -x1256_bit6  x1256_bit7  x1256_bit8 -x1256_bit9 -x1256_bit10 -x1256_bit11 -x1256_bit12 -x1256_bit13 -x1256_bit14 -x1256_bit15 -x1256_bit16 -x1256_bit17 -x1256_bit18 -x1256_bit19 -x1274_bit_10 -x1274_bit_9 -x1274_bit_8 -x1274_bit_7 -x1274_bit_6 -x1274_bit_5 -x1274_bit_4 -x1274_bit_3 -x1274_bit_2 -x1274_bit_1  x1274_bit0  x1274_bit1  x1274_bit2 -x1274_bit3 -x1274_bit4  x1274_bit5 -x1274_bit6 -x1274_bit7  x1274_bit8 -x1274_bit9 -x1274_bit10 -x1274_bit11 -x1274_bit12 -x1274_bit13 -x1274_bit14 -x1274_bit15 -x1274_bit16 -x1274_bit17 -x1274_bit18 -x1274_bit19 -x1275_bit_10 -x1275_bit_9 -x1275_bit_8 -x1275_bit_7 -x1275_bit_6 -x1275_bit_5 -x1275_bit_4 -x1275_bit_3 -x1275_bit_2 -x1275_bit_1 -x1275_bit0  x1275_bit1 -x1275_bit2 -x1275_bit3 -x1275_bit4  x1275_bit5  x1275_bit6 -x1275_bit7 -x1275_bit8  x1275_bit9 -x1275_bit10 -x1275_bit11 -x1275_bit12 -x1275_bit13 -x1275_bit14 -x1275_bit15 -x1275_bit16 -x1275_bit17 -x1275_bit18 -x1275_bit19 -x1276_bit_10 -x1276_bit_9 -x1276_bit_8 -x1276_bit_7 -x1276_bit_6 -x1276_bit_5 -x1276_bit_4 -x1276_bit_3 -x1276_bit_2 -x1276_bit_1 -x1276_bit0 -x1276_bit1 -x1276_bit2 -x1276_bit3  x1276_bit4 -x1276_bit5 -x1276_bit6  x1276_bit7 -x1276_bit8  x1276_bit9 -x1276_bit10 -x1276_bit11 -x1276_bit12 -x1276_bit13 -x1276_bit14 -x1276_bit15 -x1276_bit16 -x1276_bit17 -x1276_bit18 -x1276_bit19 -x1277_bit_10 -x1277_bit_9 -x1277_bit_8 -x1277_bit_7 -x1277_bit_6 -x1277_bit_5 -x1277_bit_4 -x1277_bit_3 -x1277_bit_2 -x1277_bit_1 -x1277_bit0  x1277_bit1  x1277_bit2 -x1277_bit3  x1277_bit4 -x1277_bit5  x1277_bit6 -x1277_bit7  x1277_bit8 -x1277_bit9 -x1277_bit10 -x1277_bit11 -x1277_bit12 -x1277_bit13 -x1277_bit14 -x1277_bit15 -x1277_bit16 -x1277_bit17 -x1277_bit18 -x1277_bit19 -x1278_bit_10 -x1278_bit_9 -x1278_bit_8 -x1278_bit_7 -x1278_bit_6 -x1278_bit_5 -x1278_bit_4 -x1278_bit_3 -x1278_bit_2 -x1278_bit_1 -x1278_bit0 -x1278_bit1 -x1278_bit2 -x1278_bit3  x1278_bit4 -x1278_bit5 -x1278_bit6 -x1278_bit7  x1278_bit8 -x1278_bit9 -x1278_bit10 -x1278_bit11 -x1278_bit12 -x1278_bit13 -x1278_bit14 -x1278_bit15 -x1278_bit16 -x1278_bit17 -x1278_bit18 -x1278_bit19 -x1279_bit_10 -x1279_bit_9 -x1279_bit_8 -x1279_bit_7 -x1279_bit_6 -x1279_bit_5 -x1279_bit_4 -x1279_bit_3 -x1279_bit_2 -x1279_bit_1 -x1279_bit0 -x1279_bit1 -x1279_bit2 -x1279_bit3 -x1279_bit4  x1279_bit5 -x1279_bit6 -x1279_bit7  x1279_bit8 -x1279_bit9 -x1279_bit10 -x1279_bit11 -x1279_bit12 -x1279_bit13 -x1279_bit14 -x1279_bit15 -x1279_bit16 -x1279_bit17 -x1279_bit18 -x1279_bit19 -x1280_bit_10 -x1280_bit_9 -x1280_bit_8 -x1280_bit_7 -x1280_bit_6 -x1280_bit_5 -x1280_bit_4 -x1280_bit_3 -x1280_bit_2 -x1280_bit_1 -x1280_bit0 -x1280_bit1 -x1280_bit2  x1280_bit3 -x1280_bit4 -x1280_bit5  x1280_bit6 -x1280_bit7 -x1280_bit8  x1280_bit9 -x1280_bit10 -x1280_bit11 -x1280_bit12 -x1280_bit13 -x1280_bit14 -x1280_bit15 -x1280_bit16 -x1280_bit17 -x1280_bit18 -x1280_bit19 -x1281_bit_10 -x1281_bit_9 -x1281_bit_8 -x1281_bit_7 -x1281_bit_6 -x1281_bit_5 -x1281_bit_4 -x1281_bit_3 -x1281_bit_2 -x1281_bit_1 -x1281_bit0 -x1281_bit1 -x1281_bit2 -x1281_bit3 -x1281_bit4 -x1281_bit5  x1281_bit6 -x1281_bit7  x1281_bit8 -x1281_bit9 -x1281_bit10 -x1281_bit11 -x1281_bit12 -x1281_bit13 -x1281_bit14 -x1281_bit15 -x1281_bit16 -x1281_bit17 -x1281_bit18 -x1281_bit19 -x1282_bit_10 -x1282_bit_9 -x1282_bit_8 -x1282_bit_7 -x1282_bit_6 -x1282_bit_5 -x1282_bit_4 -x1282_bit_3 -x1282_bit_2 -x1282_bit_1  x1282_bit0 -x1282_bit1  x1282_bit2 -x1282_bit3  x1282_bit4  x1282_bit5 -x1282_bit6 -x1282_bit7  x1282_bit8 -x1282_bit9 -x1282_bit10 -x1282_bit11 -x1282_bit12 -x1282_bit13 -x1282_bit14 -x1282_bit15 -x1282_bit16 -x1282_bit17 -x1282_bit18 -x1282_bit19 -x1283_bit_10 -x1283_bit_9 -x1283_bit_8 -x1283_bit_7 -x1283_bit_6 -x1283_bit_5 -x1283_bit_4 -x1283_bit_3 -x1283_bit_2 -x1283_bit_1 -x1283_bit0 -x1283_bit1 -x1283_bit2 -x1283_bit3  x1283_bit4 -x1283_bit5 -x1283_bit6 -x1283_bit7 -x1283_bit8 -x1283_bit9 -x1283_bit10 -x1283_bit11 -x1283_bit12 -x1283_bit13 -x1283_bit14 -x1283_bit15 -x1283_bit16 -x1283_bit17 -x1283_bit18 -x1283_bit19 -x1257_bit_10 -x1257_bit_9 -x1257_bit_8 -x1257_bit_7 -x1257_bit_6 -x1257_bit_5 -x1257_bit_4 -x1257_bit_3 -x1257_bit_2 -x1257_bit_1  x1257_bit0 -x1257_bit1 -x1257_bit2 -x1257_bit3 -x1257_bit4 -x1257_bit5 -x1257_bit6 -x1257_bit7  x1257_bit8 -x1257_bit9 -x1257_bit10 -x1257_bit11 -x1257_bit12 -x1257_bit13 -x1257_bit14 -x1257_bit15 -x1257_bit16 -x1257_bit17 -x1257_bit18 -x1257_bit19 -x1284_bit_10 -x1284_bit_9 -x1284_bit_8 -x1284_bit_7 -x1284_bit_6 -x1284_bit_5 -x1284_bit_4 -x1284_bit_3 -x1284_bit_2 -x1284_bit_1 -x1284_bit0 -x1284_bit1  x1284_bit2 -x1284_bit3 -x1284_bit4 -x1284_bit5 -x1284_bit6 -x1284_bit7  x1284_bit8 -x1284_bit9 -x1284_bit10 -x1284_bit11 -x1284_bit12 -x1284_bit13 -x1284_bit14 -x1284_bit15 -x1284_bit16 -x1284_bit17 -x1284_bit18 -x1284_bit19 -x1285_bit_10 -x1285_bit_9 -x1285_bit_8 -x1285_bit_7 -x1285_bit_6 -x1285_bit_5 -x1285_bit_4 -x1285_bit_3 -x1285_bit_2 -x1285_bit_1 -x1285_bit0 -x1285_bit1 -x1285_bit2 -x1285_bit3 -x1285_bit4  x1285_bit5 -x1285_bit6 -x1285_bit7 -x1285_bit8  x1285_bit9 -x1285_bit10 -x1285_bit11 -x1285_bit12 -x1285_bit13 -x1285_bit14 -x1285_bit15 -x1285_bit16 -x1285_bit17 -x1285_bit18 -x1285_bit19 -x1286_bit_10 -x1286_bit_9 -x1286_bit_8 -x1286_bit_7 -x1286_bit_6 -x1286_bit_5 -x1286_bit_4 -x1286_bit_3 -x1286_bit_2 -x1286_bit_1  x1286_bit0 -x1286_bit1 -x1286_bit2 -x1286_bit3 -x1286_bit4  x1286_bit5 -x1286_bit6  x1286_bit7  x1286_bit8 -x1286_bit9 -x1286_bit10 -x1286_bit11 -x1286_bit12 -x1286_bit13 -x1286_bit14 -x1286_bit15 -x1286_bit16 -x1286_bit17 -x1286_bit18 -x1286_bit19 -x1287_bit_10 -x1287_bit_9 -x1287_bit_8 -x1287_bit_7 -x1287_bit_6 -x1287_bit_5 -x1287_bit_4 -x1287_bit_3 -x1287_bit_2 -x1287_bit_1 -x1287_bit0 -x1287_bit1 -x1287_bit2 -x1287_bit3  x1287_bit4 -x1287_bit5 -x1287_bit6 -x1287_bit7 -x1287_bit8 -x1287_bit9 -x1287_bit10 -x1287_bit11 -x1287_bit12 -x1287_bit13 -x1287_bit14 -x1287_bit15 -x1287_bit16 -x1287_bit17 -x1287_bit18 -x1287_bit19 -x1288_bit_10 -x1288_bit_9 -x1288_bit_8 -x1288_bit_7 -x1288_bit_6 -x1288_bit_5 -x1288_bit_4 -x1288_bit_3 -x1288_bit_2 -x1288_bit_1 -x1288_bit0 -x1288_bit1 -x1288_bit2 -x1288_bit3 -x1288_bit4  x1288_bit5 -x1288_bit6 -x1288_bit7  x1288_bit8 -x1288_bit9 -x1288_bit10 -x1288_bit11 -x1288_bit12 -x1288_bit13 -x1288_bit14 -x1288_bit15 -x1288_bit16 -x1288_bit17 -x1288_bit18 -x1288_bit19 -x1289_bit_10 -x1289_bit_9 -x1289_bit_8 -x1289_bit_7 -x1289_bit_6 -x1289_bit_5 -x1289_bit_4 -x1289_bit_3 -x1289_bit_2 -x1289_bit_1 -x1289_bit0 -x1289_bit1 -x1289_bit2 -x1289_bit3 -x1289_bit4 -x1289_bit5  x1289_bit6  x1289_bit7 -x1289_bit8 -x1289_bit9 -x1289_bit10 -x1289_bit11 -x1289_bit12 -x1289_bit13 -x1289_bit14 -x1289_bit15 -x1289_bit16 -x1289_bit17 -x1289_bit18 -x1289_bit19 -x1290_bit_10 -x1290_bit_9 -x1290_bit_8 -x1290_bit_7 -x1290_bit_6 -x1290_bit_5 -x1290_bit_4 -x1290_bit_3 -x1290_bit_2 -x1290_bit_1 -x1290_bit0 -x1290_bit1 -x1290_bit2 -x1290_bit3  x1290_bit4  x1290_bit5 -x1290_bit6 -x1290_bit7  x1290_bit8 -x1290_bit9 -x1290_bit10 -x1290_bit11 -x1290_bit12 -x1290_bit13 -x1290_bit14 -x1290_bit15 -x1290_bit16 -x1290_bit17 -x1290_bit18 -x1290_bit19 -x1291_bit_10 -x1291_bit_9 -x1291_bit_8 -x1291_bit_7 -x1291_bit_6 -x1291_bit_5 -x1291_bit_4 -x1291_bit_3 -x1291_bit_2 -x1291_bit_1 -x1291_bit0 -x1291_bit1 -x1291_bit2 -x1291_bit3 -x1291_bit4 -x1291_bit5 -x1291_bit6 -x1291_bit7 -x1291_bit8  x1291_bit9 -x1291_bit10 -x1291_bit11 -x1291_bit12 -x1291_bit13 -x1291_bit14 -x1291_bit15 -x1291_bit16 -x1291_bit17 -x1291_bit18 -x1291_bit19 -x1292_bit_10 -x1292_bit_9 -x1292_bit_8 -x1292_bit_7 -x1292_bit_6 -x1292_bit_5 -x1292_bit_4 -x1292_bit_3 -x1292_bit_2 -x1292_bit_1  x1292_bit0 -x1292_bit1  x1292_bit2 -x1292_bit3 -x1292_bit4  x1292_bit5 -x1292_bit6 -x1292_bit7 -x1292_bit8  x1292_bit9 -x1292_bit10 -x1292_bit11 -x1292_bit12 -x1292_bit13 -x1292_bit14 -x1292_bit15 -x1292_bit16 -x1292_bit17 -x1292_bit18 -x1292_bit19 -x1293_bit_10 -x1293_bit_9 -x1293_bit_8 -x1293_bit_7 -x1293_bit_6 -x1293_bit_5 -x1293_bit_4 -x1293_bit_3 -x1293_bit_2 -x1293_bit_1 -x1293_bit0  x1293_bit1 -x1293_bit2 -x1293_bit3 -x1293_bit4 -x1293_bit5  x1293_bit6 -x1293_bit7 -x1293_bit8  x1293_bit9 -x1293_bit10 -x1293_bit11 -x1293_bit12 -x1293_bit13 -x1293_bit14 -x1293_bit15 -x1293_bit16 -x1293_bit17 -x1293_bit18 -x1293_bit19 -x1258_bit_10 -x1258_bit_9 -x1258_bit_8 -x1258_bit_7 -x1258_bit_6 -x1258_bit_5 -x1258_bit_4 -x1258_bit_3 -x1258_bit_2 -x1258_bit_1 -x1258_bit0  x1258_bit1 -x1258_bit2 -x1258_bit3  x1258_bit4 -x1258_bit5 -x1258_bit6 -x1258_bit7 -x1258_bit8  x1258_bit9 -x1258_bit10 -x1258_bit11 -x1258_bit12 -x1258_bit13 -x1258_bit14 -x1258_bit15 -x1258_bit16 -x1258_bit17 -x1258_bit18 -x1258_bit19 -x1294_bit_10 -x1294_bit_9 -x1294_bit_8 -x1294_bit_7 -x1294_bit_6 -x1294_bit_5 -x1294_bit_4 -x1294_bit_3 -x1294_bit_2 -x1294_bit_1 -x1294_bit0 -x1294_bit1 -x1294_bit2 -x1294_bit3 -x1294_bit4 -x1294_bit5  x1294_bit6 -x1294_bit7 -x1294_bit8 -x1294_bit9 -x1294_bit10 -x1294_bit11 -x1294_bit12 -x1294_bit13 -x1294_bit14 -x1294_bit15 -x1294_bit16 -x1294_bit17 -x1294_bit18 -x1294_bit19 -x1295_bit_10 -x1295_bit_9 -x1295_bit_8 -x1295_bit_7 -x1295_bit_6 -x1295_bit_5 -x1295_bit_4 -x1295_bit_3 -x1295_bit_2 -x1295_bit_1 -x1295_bit0 -x1295_bit1 -x1295_bit2 -x1295_bit3 -x1295_bit4  x1295_bit5 -x1295_bit6 -x1295_bit7 -x1295_bit8  x1295_bit9 -x1295_bit10 -x1295_bit11 -x1295_bit12 -x1295_bit13 -x1295_bit14 -x1295_bit15 -x1295_bit16 -x1295_bit17 -x1295_bit18 -x1295_bit19 -x1296_bit_10 -x1296_bit_9 -x1296_bit_8 -x1296_bit_7 -x1296_bit_6 -x1296_bit_5 -x1296_bit_4 -x1296_bit_3 -x1296_bit_2 -x1296_bit_1 -x1296_bit0 -x1296_bit1 -x1296_bit2 -x1296_bit3  x1296_bit4 -x1296_bit5  x1296_bit6 -x1296_bit7 -x1296_bit8 -x1296_bit9 -x1296_bit10 -x1296_bit11 -x1296_bit12 -x1296_bit13 -x1296_bit14 -x1296_bit15 -x1296_bit16 -x1296_bit17 -x1296_bit18 -x1296_bit19 -x1297_bit_10 -x1297_bit_9 -x1297_bit_8 -x1297_bit_7 -x1297_bit_6 -x1297_bit_5 -x1297_bit_4 -x1297_bit_3 -x1297_bit_2 -x1297_bit_1  x1297_bit0 -x1297_bit1 -x1297_bit2 -x1297_bit3  x1297_bit4 -x1297_bit5  x1297_bit6 -x1297_bit7  x1297_bit8 -x1297_bit9 -x1297_bit10 -x1297_bit11 -x1297_bit12 -x1297_bit13 -x1297_bit14 -x1297_bit15 -x1297_bit16 -x1297_bit17 -x1297_bit18 -x1297_bit19 -x1298_bit_10 -x1298_bit_9 -x1298_bit_8 -x1298_bit_7 -x1298_bit_6 -x1298_bit_5 -x1298_bit_4 -x1298_bit_3 -x1298_bit_2 -x1298_bit_1 -x1298_bit0 -x1298_bit1  x1298_bit2 -x1298_bit3 -x1298_bit4 -x1298_bit5 -x1298_bit6 -x1298_bit7  x1298_bit8 -x1298_bit9 -x1298_bit10 -x1298_bit11 -x1298_bit12 -x1298_bit13 -x1298_bit14 -x1298_bit15 -x1298_bit16 -x1298_bit17 -x1298_bit18 -x1298_bit19 -x1259_bit_10 -x1259_bit_9 -x1259_bit_8 -x1259_bit_7 -x1259_bit_6 -x1259_bit_5 -x1259_bit_4 -x1259_bit_3 -x1259_bit_2 -x1259_bit_1  x1259_bit0  x1259_bit1 -x1259_bit2 -x1259_bit3  x1259_bit4  x1259_bit5  x1259_bit6  x1259_bit7 -x1259_bit8 -x1259_bit9 -x1259_bit10 -x1259_bit11 -x1259_bit12 -x1259_bit13 -x1259_bit14 -x1259_bit15 -x1259_bit16 -x1259_bit17 -x1259_bit18 -x1259_bit19 -x1260_bit_10 -x1260_bit_9 -x1260_bit_8 -x1260_bit_7 -x1260_bit_6 -x1260_bit_5 -x1260_bit_4 -x1260_bit_3 -x1260_bit_2 -x1260_bit_1  x1260_bit0 -x1260_bit1 -x1260_bit2 -x1260_bit3 -x1260_bit4 -x1260_bit5  x1260_bit6 -x1260_bit7 -x1260_bit8  x1260_bit9 -x1260_bit10 -x1260_bit11 -x1260_bit12 -x1260_bit13 -x1260_bit14 -x1260_bit15 -x1260_bit16 -x1260_bit17 -x1260_bit18 -x1260_bit19 -x1261_bit_10 -x1261_bit_9 -x1261_bit_8 -x1261_bit_7 -x1261_bit_6 -x1261_bit_5 -x1261_bit_4 -x1261_bit_3 -x1261_bit_2 -x1261_bit_1 -x1261_bit0 -x1261_bit1  x1261_bit2 -x1261_bit3 -x1261_bit4  x1261_bit5 -x1261_bit6 -x1261_bit7  x1261_bit8 -x1261_bit9 -x1261_bit10 -x1261_bit11 -x1261_bit12 -x1261_bit13 -x1261_bit14 -x1261_bit15 -x1261_bit16 -x1261_bit17 -x1261_bit18 -x1261_bit19 -x1262_bit_10 -x1262_bit_9 -x1262_bit_8 -x1262_bit_7 -x1262_bit_6 -x1262_bit_5 -x1262_bit_4 -x1262_bit_3 -x1262_bit_2 -x1262_bit_1  x1262_bit0 -x1262_bit1  x1262_bit2 -x1262_bit3  x1262_bit4 -x1262_bit5 -x1262_bit6  x1262_bit7 -x1262_bit8  x1262_bit9 -x1262_bit10 -x1262_bit11 -x1262_bit12 -x1262_bit13 -x1262_bit14 -x1262_bit15 -x1262_bit16 -x1262_bit17 -x1262_bit18 -x1262_bit19 -x1263_bit_10 -x1263_bit_9 -x1263_bit_8 -x1263_bit_7 -x1263_bit_6 -x1263_bit_5 -x1263_bit_4 -x1263_bit_3 -x1263_bit_2 -x1263_bit_1 -x1263_bit0 -x1263_bit1 -x1263_bit2 -x1263_bit3 -x1263_bit4  x1263_bit5 -x1263_bit6  x1263_bit7 -x1263_bit8  x1263_bit9 -x1263_bit10 -x1263_bit11 -x1263_bit12 -x1263_bit13 -x1263_bit14 -x1263_bit15 -x1263_bit16 -x1263_bit17 -x1263_bit18 -x1263_bit19 
s OPTIMUM FOUND
#### 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
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.58 0.89 0.96 2/55 14235
Raw data (stat): 14235 (runsolver) R 14234 29618 29617 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 860200544 884736 94 4294967295 134512640 135332820 3221224448 3221219612 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0017 s]
Raw data (loadavg): 0.64 0.89 0.96 2/56 14240
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+20.0072 s]
Raw data (loadavg): 0.70 0.89 0.96 2/56 14240
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+30.0081 s]
Raw data (loadavg): 0.74 0.90 0.96 2/56 14240
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+40.0081 s]
Raw data (loadavg): 0.78 0.90 0.96 2/56 14240
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+50.0089 s]
Raw data (loadavg): 0.81 0.90 0.96 2/56 14240
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+60.0103 s]
Raw data (loadavg): 0.84 0.91 0.96 2/56 14240
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+70.0108 s]
Raw data (loadavg): 0.87 0.91 0.96 2/56 14242
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+80.1167 s]
Raw data (loadavg): 0.89 0.91 0.96 2/56 14242
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+90.117 s]
Raw data (loadavg): 0.90 0.91 0.96 2/56 14242
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+100.117 s]
Raw data (loadavg): 0.92 0.92 0.96 2/56 14242
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+110.139 s]
Raw data (loadavg): 0.93 0.92 0.96 2/56 14242
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+120.141 s]
Raw data (loadavg): 0.94 0.92 0.96 2/56 14242
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+130.142 s]
Raw data (loadavg): 0.95 0.92 0.96 2/56 14244
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+140.149 s]
Raw data (loadavg): 0.96 0.92 0.96 2/56 14244
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+150.155 s]
Raw data (loadavg): 0.96 0.93 0.96 2/56 14244
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+160.156 s]
Raw data (loadavg): 0.97 0.93 0.96 2/56 14244
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+170.157 s]
Raw data (loadavg): 0.97 0.93 0.96 2/56 14244
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+180.159 s]
Raw data (loadavg): 0.98 0.93 0.96 2/56 14244
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+190.159 s]
Raw data (loadavg): 0.98 0.93 0.96 2/56 14246
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+200.159 s]
Raw data (loadavg): 0.98 0.94 0.96 2/56 14246
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+210.16 s]
Raw data (loadavg): 0.98 0.94 0.96 2/56 14246
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+220.161 s]
Raw data (loadavg): 0.99 0.94 0.96 2/56 14246
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+230.162 s]
Raw data (loadavg): 0.99 0.94 0.96 2/56 14246
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+233.388 s]
Raw data (loadavg): 0.99 0.94 0.96 1/54 14256
Raw data (stat): 14235 (vallstSAT2005PB) S 14234 29618 29617 0 -1 0 321 231 0 0 0 0 0 0 20 0 1 0 860200544 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 0

Child status: 30
Real time (s): 233.388
CPU time (s): 233.037
CPU user time (s): 209.177
CPU system time (s): 23.8594
CPU usage (%): 99.8494
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	3342319366
#### END VERIFIER DATA ####