PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-fiber.opb
MD5SUM	d1d488615de0d5a5bcf2a298507e66b1
Bench Category	optimization, medium integers (OPTMEDINT)
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	72966962
Number of bits of the biggest number in a constraint	27
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	90.9232
Number of variables	2134
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	51
Trace number 34253

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-05-27 21:13:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17532 boxname=wulflinc24 idbench=1349 idsolver=8 numberseed=0
MD5SUM SOLVER: 4b637b3b6117f2add1a6288e91336322  /oldhome/oroussel/solvers/vallstSAT2005PB.sh
MD5SUM BENCH:  d1d488615de0d5a5bcf2a298507e66b1  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-fiber.opb
REAL COMMAND:  vallstSAT2005PB.sh /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-fiber.opb 0
IDLAUNCH: 17532
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        620152 kB
Buffers:         35220 kB
Cached:         357380 kB
SwapCached:        644 kB
Active:          52384 kB
Inactive:       342260 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        619900 kB
SwapTotal:     2097892 kB
SwapFree:      2096352 kB
Dirty:             232 kB
Writeback:           0 kB
Mapped:           5124 kB
Slab:            14032 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 21:27:15 (client local time) WITH STATUS 10 IN 798.741 SECONDS
stats: 17532 0 798.741 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
1:
seed: 0
Nr of vars set: 135  (#equs: 0)
Nr of vars set: 135  (#equs: 53)
#decisions: 4710964;  #end-nodes: 2599006;
#proof improvement attempts: 0;  #restarts: 4224
Current batch, end-nodes: 0 / 1135 (1135)
#axs: 750, #non-axs: 932
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: the time limit has been exceeded (2)
No model found at all.
result: the time limit has been exceeded (2)
seed: 0
Nr of vars set: 135  (#equs: 53)
Time taken: 5 min, 9 sec

2:
seed: 0
Nr of vars set: 135  (#equs: 0)
Nr of vars set: 135  (#equs: 0)
#decisions: 7070990;  #end-nodes: 4239684;
#proof improvement attempts: 0;  #restarts: 5339
Current batch, end-nodes: 776 / 1466 (1454)
#axs: 590, #non-axs: 4336
tight: meta-meta: start: 3, end: 3;  meta: start: 9, end (keep): 16
loose: meta-meta: start: 6, end: 8;  meta: start: 12, end (keep): 17
result: model found (1)
seed: 0
Nr of vars set: 2081  (#equs: 0)
Time taken: 8 min, 8 sec
times:
0m0.019s 0m0.012s
12m6.226s 1m11.727s
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_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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 
s SATISFIABLE
#### 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.85 0.94 0.91 2/54 15284
Raw data (stat): 15284 (runsolver) R 15283 4613 4612 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 859314019 884736 94 4294967295 134512640 135332820 3221224448 3221219612 135092226 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.94 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.94 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+30.0018 s]
Raw data (loadavg): 0.91 0.94 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+40.0014 s]
Raw data (loadavg): 0.92 0.94 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+50.0008 s]
Raw data (loadavg): 0.93 0.94 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+60.0008 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+70.0005 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+80.0009 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+90.0008 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+110.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+120.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+140.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+150.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+170.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+240.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+250.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15287
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 859314019 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15289
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 2128
[startup+798.985 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 15299
Raw data (stat): 15284 (vallstSAT2005PB) S 15283 4613 4612 0 -1 0 369 1296 0 0 1 1 27707 3206 19 0 1 0 859314019 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 248 485 147 0 385 0
vsize: 0

Child status: 10
Real time (s): 798.985
CPU time (s): 798.741
CPU user time (s): 726.802
CPU system time (s): 71.9391
CPU usage (%): 99.9695
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	3131133804
#### END VERIFIER DATA ####