Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos17.opb |
MD5SUM | 510c7f71a2644dcf876297008b35f617 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 20977859 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 2126 |
Biggest coefficient in the objective function | 27663360 |
Number of bits for the biggest coefficient in the objective function | 25 |
Sum of the numbers in the objective function | 110500348 |
Number of bits of the sum of numbers in the objective function | 27 |
Biggest number in a constraint | 1677721600000000 |
Number of bits of the biggest number in a constraint | 51 |
Biggest sum of numbers in a constraint | 40265324766820451 |
Number of bits of the biggest sum of numbers | 56 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1240.29 |
Number of variables | 3115 |
Total number of constraints | 971 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 300 |
Number of constraints which are nor clauses,nor cardinality constraints | 671 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 780 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc24 THE 2005-05-27 22:33:27 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=14607 boxname=wulflinc24 idbench=1124 idsolver=8 numberseed=0 MD5SUM SOLVER: 4b637b3b6117f2add1a6288e91336322 /oldhome/oroussel/solvers/vallstSAT2005PB.sh MD5SUM BENCH: 510c7f71a2644dcf876297008b35f617 /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-neos17.opb REAL COMMAND: vallstSAT2005PB.sh /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-neos17.opb 0 IDLAUNCH: 14607 /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: 604120 kB Buffers: 36080 kB Cached: 372160 kB SwapCached: 644 kB Active: 58260 kB Inactive: 352140 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 603868 kB SwapTotal: 2097892 kB SwapFree: 2096352 kB Dirty: 196 kB Writeback: 0 kB Mapped: 5124 kB Slab: 14488 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 22:33:30 (client local time) WITH STATUS 30 IN 2.74558 SECONDS stats: 14607 6 2.74558 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### 1: seed: 0 Nr of vars set: 39 (#equs: 0) Nr of vars set: 39 (#equs: 0) #decisions: 1070; #end-nodes: 0; #proof improvement attempts: 0; #restarts: 0 Current batch, end-nodes: 0 / 80 (80) #axs: 188, #non-axs: 0 tight: meta-meta: start: 6, end: 9; 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: 110500347 (0:>=*); Model found with constant: (pushed:) 4294967295 (110500348:>=*) 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: 39 (#equs: 0) Time taken in milliseconds: 1640 times: 0m0.018s 0m0.008s 0m1.341s 0m0.324s v -D0001_bit0 -D0002_bit0 -D0004_bit0 -D0005_bit0 -D0006_bit0 -D0007_bit0 -D0008_bit0 -D0009_bit0 -D0010_bit0 -D0011_bit0 -D0012_bit0 -D0013_bit0 -D0014_bit0 -D0016_bit0 -D0017_bit0 -D0018_bit0 -D0020_bit0 -D0021_bit0 -D0022_bit0 -D0023_bit0 -D0024_bit0 -D0025_bit0 -D0026_bit0 -D0028_bit0 -D0030_bit0 -D0031_bit0 -D0033_bit0 -D0034_bit0 -D0035_bit0 -D0037_bit0 -D0038_bit0 -D0039_bit0 -D0041_bit0 -D0042_bit0 -D0043_bit0 -D0044_bit0 -D0045_bit0 -D0047_bit0 -D0048_bit0 -D0049_bit0 -D0052_bit0 -D0053_bit0 -D0054_bit0 -D0055_bit0 -D0056_bit0 -D0057_bit0 -D0060_bit0 -D0062_bit0 -D0063_bit0 -D0064_bit0 -D0065_bit0 -D0068_bit0 -D0070_bit0 -D0071_bit0 -D0072_bit0 -D0073_bit0 -D0074_bit0 -D0075_bit0 -D0077_bit0 -D0079_bit0 -D0080_bit0 -D0081_bit0 -D0082_bit0 -D0083_bit0 -D0084_bit0 -D0085_bit0 -D0086_bit0 -D0087_bit0 -D0089_bit0 -D0090_bit0 -D0091_bit0 -D0093_bit0 -D0094_bit0 -D0095_bit0 -D0097_bit0 -D0098_bit0 -D0101_bit0 -D0102_bit0 -D0104_bit0 -D0105_bit0 -D0106_bit0 -D0107_bit0 -D0108_bit0 -D0109_bit0 -D0113_bit0 -D0115_bit0 -D0116_bit0 -D0117_bit0 -D0118_bit0 -D0119_bit0 -D0120_bit0 -D0121_bit0 -D0123_bit0 -D0124_bit0 -D0125_bit0 -D0126_bit0 -D0128_bit0 -D0129_bit0 -D0130_bit0 -D0131_bit0 -D0132_bit0 -D0133_bit0 -D0134_bit0 -D0135_bit0 -D0137_bit0 -D0138_bit0 -D0139_bit0 -D0140_bit0 -D0141_bit0 -D0142_bit0 -D0143_bit0 -D0144_bit0 -D0145_bit0 -D0148_bit0 -D0149_bit0 -D0151_bit0 -D0152_bit0 -D0153_bit0 -D0157_bit0 -D0162_bit0 -D0163_bit0 -D0164_bit0 -D0165_bit0 -D0166_bit0 -D0167_bit0 -D0168_bit0 -D0169_bit0 -D0170_bit0 -D0171_bit0 -D0172_bit0 -D0173_bit0 -D0174_bit0 -D0175_bit0 -D0176_bit0 -D0178_bit0 -D0179_bit0 -D0180_bit0 -D0182_bit0 -D0183_bit0 -D0184_bit0 -D0186_bit0 -D0187_bit0 -D0188_bit0 -D0189_bit0 -D0190_bit0 -D0192_bit0 -D0195_bit0 -D0196_bit0 -D0197_bit0 -D0198_bit0 -D0201_bit0 -D0202_bit0 -D0203_bit0 -D0204_bit0 -D0205_bit0 -D0206_bit0 -D0207_bit0 -D0208_bit0 -D0209_bit0 -D0210_bit0 -D0211_bit0 -D0212_bit0 -D0213_bit0 -D0214_bit0 -D0215_bit0 -D0216_bit0 -D0217_bit0 -D0219_bit0 -D0220_bit0 -D0221_bit0 -D0222_bit0 -D0223_bit0 -D0224_bit0 -D0225_bit0 -D0227_bit0 -D0228_bit0 -D0229_bit0 -D0230_bit0 -D0231_bit0 -D0234_bit0 -D0235_bit0 -D0236_bit0 -D0237_bit0 -D0238_bit0 -D0241_bit0 -D0242_bit0 -D0243_bit0 -D0245_bit0 -D0246_bit0 -D0247_bit0 -D0248_bit0 -D0249_bit0 -D0250_bit0 -D0251_bit0 -D0252_bit0 -D0254_bit0 -D0258_bit0 -D0259_bit0 -D0260_bit0 -D0261_bit0 -D0262_bit0 -D0263_bit0 -D0264_bit0 -D0265_bit0 -D0266_bit0 -D0267_bit0 -D0268_bit0 -D0269_bit0 -D0270_bit0 -D0271_bit0 -D0275_bit0 -D0276_bit0 -D0277_bit0 -D0278_bit0 -D0279_bit0 -D0280_bit0 -D0281_bit0 -D0282_bit0 -D0283_bit0 -D0285_bit0 -D0286_bit0 -D0287_bit0 -D0288_bit0 -D0289_bit0 -D0290_bit0 -D0291_bit0 -D0292_bit0 -D0293_bit0 -D0295_bit0 -D0296_bit0 -D0297_bit0 -D0298_bit0 -D0299_bit0 -D0300_bit0 -D0301_bit_10 -D0301_bit_9 -D0301_bit_8 -D0301_bit_7 -D0301_bit_6 -D0301_bit_5 -D0301_bit_4 -D0301_bit_3 -D0301_bit_2 -D0301_bit_1 -D0301_bit0 -D0302_bit_10 -D0302_bit_9 -D0302_bit_8 -D0302_bit_7 -D0302_bit_6 -D0302_bit_5 -D0302_bit_4 -D0302_bit_3 -D0302_bit_2 -D0302_bit_1 -D0302_bit0 -D0303_bit_10 -D0303_bit_9 -D0303_bit_8 -D0303_bit_7 -D0303_bit_6 -D0303_bit_5 -D0303_bit_4 -D0303_bit_3 -D0303_bit_2 -D0303_bit_1 -D0303_bit0 -D0304_bit_10 -D0304_bit_9 -D0304_bit_8 -D0304_bit_7 -D0304_bit_6 -D0304_bit_5 -D0304_bit_4 -D0304_bit_3 -D0304_bit_2 -D0304_bit_1 -D0304_bit0 -D0305_bit_10 -D0305_bit_9 -D0305_bit_8 -D0305_bit_7 -D0305_bit_6 -D0305_bit_5 -D0305_bit_4 -D0305_bit_3 -D0305_bit_2 -D0305_bit_1 -D0305_bit0 -D0307_bit_10 -D0307_bit_9 -D0307_bit_8 -D0307_bit_7 -D0307_bit_6 -D0307_bit_5 -D0307_bit_4 -D0307_bit_3 -D0307_bit_2 -D0307_bit_1 -D0307_bit0 -D0308_bit_10 -D0308_bit_9 -D0308_bit_8 -D0308_bit_7 -D0308_bit_6 -D0308_bit_5 -D0308_bit_4 -D0308_bit_3 -D0308_bit_2 -D0308_bit_1 -D0308_bit0 -D0309_bit_10 -D0309_bit_9 -D0309_bit_8 -D0309_bit_7 -D0309_bit_6 -D0309_bit_5 -D0309_bit_4 -D0309_bit_3 -D0309_bit_2 -D0309_bit_1 -D0309_bit0 -D0311_bit_10 -D0311_bit_9 -D0311_bit_8 -D0311_bit_7 -D0311_bit_6 -D0311_bit_5 -D0311_bit_4 -D0311_bit_3 -D0311_bit_2 -D0311_bit_1 -D0311_bit0 -D0312_bit_10 -D0312_bit_9 -D0312_bit_8 -D0312_bit_7 -D0312_bit_6 -D0312_bit_5 -D0312_bit_4 -D0312_bit_3 -D0312_bit_2 -D0312_bit_1 -D0312_bit0 -D0313_bit_10 -D0313_bit_9 -D0313_bit_8 -D0313_bit_7 -D0313_bit_6 -D0313_bit_5 -D0313_bit_4 -D0313_bit_3 -D0313_bit_2 -D0313_bit_1 -D0313_bit0 -D0314_bit_10 -D0314_bit_9 -D0314_bit_8 -D0314_bit_7 -D0314_bit_6 -D0314_bit_5 -D0314_bit_4 -D0314_bit_3 -D0314_bit_2 -D0314_bit_1 -D0314_bit0 -D0315_bit_10 -D0315_bit_9 -D0315_bit_8 -D0315_bit_7 -D0315_bit_6 -D0315_bit_5 -D0315_bit_4 -D0315_bit_3 -D0315_bit_2 -D0315_bit_1 -D0315_bit0 -D0316_bit_10 -D0316_bit_9 -D0316_bit_8 -D0316_bit_7 -D0316_bit_6 -D0316_bit_5 -D0316_bit_4 -D0316_bit_3 -D0316_bit_2 -D0316_bit_1 -D0316_bit0 -D0317_bit_10 -D0317_bit_9 -D0317_bit_8 -D0317_bit_7 -D0317_bit_6 -D0317_bit_5 -D0317_bit_4 -D0317_bit_3 -D0317_bit_2 -D0317_bit_1 -D0317_bit0 -D0318_bit_10 -D0318_bit_9 -D0318_bit_8 -D0318_bit_7 -D0318_bit_6 -D0318_bit_5 -D0318_bit_4 -D0318_bit_3 -D0318_bit_2 -D0318_bit_1 -D0318_bit0 -D0319_bit_10 -D0319_bit_9 -D0319_bit_8 -D0319_bit_7 -D0319_bit_6 -D0319_bit_5 -D0319_bit_4 -D0319_bit_3 -D0319_bit_2 -D0319_bit_1 -D0319_bit0 -D0320_bit_10 -D0320_bit_9 -D0320_bit_8 -D0320_bit_7 -D0320_bit_6 -D0320_bit_5 -D0320_bit_4 -D0320_bit_3 -D0320_bit_2 -D0320_bit_1 -D0320_bit0 -D0321_bit_10 -D0321_bit_9 -D0321_bit_8 -D0321_bit_7 -D0321_bit_6 -D0321_bit_5 -D0321_bit_4 -D0321_bit_3 -D0321_bit_2 -D0321_bit_1 -D0321_bit0 -D0322_bit_10 -D0322_bit_9 -D0322_bit_8 -D0322_bit_7 -D0322_bit_6 -D0322_bit_5 -D0322_bit_4 -D0322_bit_3 -D0322_bit_2 -D0322_bit_1 -D0322_bit0 -D0323_bit_10 -D0323_bit_9 -D0323_bit_8 -D0323_bit_7 -D0323_bit_6 -D0323_bit_5 -D0323_bit_4 -D0323_bit_3 -D0323_bit_2 -D0323_bit_1 -D0323_bit0 -D0324_bit_10 -D0324_bit_9 -D0324_bit_8 -D0324_bit_7 -D0324_bit_6 -D0324_bit_5 -D0324_bit_4 -D0324_bit_3 -D0324_bit_2 -D0324_bit_1 -D0324_bit0 -D0325_bit_10 -D0325_bit_9 -D0325_bit_8 -D0325_bit_7 -D0325_bit_6 -D0325_bit_5 -D0325_bit_4 -D0325_bit_3 -D0325_bit_2 -D0325_bit_1 -D0325_bit0 -D0327_bit_10 -D0327_bit_9 -D0327_bit_8 -D0327_bit_7 -D0327_bit_6 -D0327_bit_5 -D0327_bit_4 -D0327_bit_3 -D0327_bit_2 -D0327_bit_1 -D0327_bit0 -D0328_bit_10 -D0328_bit_9 -D0328_bit_8 -D0328_bit_7 -D0328_bit_6 -D0328_bit_5 -D0328_bit_4 -D0328_bit_3 -D0328_bit_2 -D0328_bit_1 -D0328_bit0 -D0329_bit_10 -D0329_bit_9 -D0329_bit_8 -D0329_bit_7 -D0329_bit_6 -D0329_bit_5 -D0329_bit_4 -D0329_bit_3 -D0329_bit_2 -D0329_bit_1 -D0329_bit0 -D0330_bit_10 -D0330_bit_9 -D0330_bit_8 -D0330_bit_7 -D0330_bit_6 -D0330_bit_5 -D0330_bit_4 -D0330_bit_3 -D0330_bit_2 -D0330_bit_1 -D0330_bit0 -D0331_bit_10 -D0331_bit_9 -D0331_bit_8 -D0331_bit_7 -D0331_bit_6 -D0331_bit_5 -D0331_bit_4 -D0331_bit_3 -D0331_bit_2 -D0331_bit_1 -D0331_bit0 -D0332_bit_10 -D0332_bit_9 -D0332_bit_8 -D0332_bit_7 -D0332_bit_6 -D0332_bit_5 -D0332_bit_4 -D0332_bit_3 -D0332_bit_2 -D0332_bit_1 -D0332_bit0 -D0333_bit_10 -D0333_bit_9 -D0333_bit_8 -D0333_bit_7 -D0333_bit_6 -D0333_bit_5 -D0333_bit_4 -D0333_bit_3 -D0333_bit_2 -D0333_bit_1 -D0333_bit0 -D0334_bit_10 -D0334_bit_9 -D0334_bit_8 -D0334_bit_7 -D0334_bit_6 -D0334_bit_5 -D0334_bit_4 -D0334_bit_3 -D0334_bit_2 -D0334_bit_1 -D0334_bit0 -D0335_bit_10 -D0335_bit_9 -D0335_bit_8 -D0335_bit_7 -D0335_bit_6 -D0335_bit_5 -D0335_bit_4 -D0335_bit_3 -D0335_bit_2 -D0335_bit_1 -D0335_bit0 -D0336_bit_10 -D0336_bit_9 -D0336_bit_8 -D0336_bit_7 -D0336_bit_6 -D0336_bit_5 -D0336_bit_4 -D0336_bit_3 -D0336_bit_2 -D0336_bit_1 -D0336_bit0 -D0337_bit_10 -D0337_bit_9 -D0337_bit_8 -D0337_bit_7 -D0337_bit_6 -D0337_bit_5 -D0337_bit_4 -D0337_bit_3 -D0337_bit_2 -D0337_bit_1 -D0337_bit0 -D0338_bit_10 -D0338_bit_9 -D0338_bit_8 -D0338_bit_7 -D0338_bit_6 -D0338_bit_5 -D0338_bit_4 -D0338_bit_3 -D0338_bit_2 -D0338_bit_1 -D0338_bit0 -D0340_bit_10 -D0340_bit_9 -D0340_bit_8 -D0340_bit_7 -D0340_bit_6 -D0340_bit_5 -D0340_bit_4 -D0340_bit_3 -D0340_bit_2 -D0340_bit_1 -D0340_bit0 -D0341_bit_10 -D0341_bit_9 -D0341_bit_8 -D0341_bit_7 -D0341_bit_6 -D0341_bit_5 -D0341_bit_4 -D0341_bit_3 -D0341_bit_2 -D0341_bit_1 -D0341_bit0 -D0343_bit_10 -D0343_bit_9 -D0343_bit_8 -D0343_bit_7 -D0343_bit_6 -D0343_bit_5 -D0343_bit_4 -D0343_bit_3 -D0343_bit_2 -D0343_bit_1 -D0343_bit0 -D0344_bit_10 -D0344_bit_9 -D0344_bit_8 -D0344_bit_7 -D0344_bit_6 -D0344_bit_5 -D0344_bit_4 -D0344_bit_3 -D0344_bit_2 -D0344_bit_1 -D0344_bit0 -D0345_bit_10 -D0345_bit_9 -D0345_bit_8 -D0345_bit_7 -D0345_bit_6 -D0345_bit_5 -D0345_bit_4 -D0345_bit_3 -D0345_bit_2 -D0345_bit_1 -D0345_bit0 -D0346_bit_10 -D0346_bit_9 -D0346_bit_8 -D0346_bit_7 -D0346_bit_6 -D0346_bit_5 -D0346_bit_4 -D0346_bit_3 -D0346_bit_2 -D0346_bit_1 -D0346_bit0 -D0347_bit_10 -D0347_bit_9 -D0347_bit_8 -D0347_bit_7 -D0347_bit_6 -D0347_bit_5 -D0347_bit_4 -D0347_bit_3 -D0347_bit_2 -D0347_bit_1 -D0347_bit0 -D0348_bit_10 -D0348_bit_9 -D0348_bit_8 -D0348_bit_7 -D0348_bit_6 -D0348_bit_5 -D0348_bit_4 -D0348_bit_3 -D0348_bit_2 -D0348_bit_1 -D0348_bit0 -D0349_bit_10 -D0349_bit_9 -D0349_bit_8 -D0349_bit_7 -D0349_bit_6 -D0349_bit_5 -D0349_bit_4 -D0349_bit_3 -D0349_bit_2 -D0349_bit_1 -D0349_bit0 -D0350_bit_10 -D0350_bit_9 -D0350_bit_8 -D0350_bit_7 -D0350_bit_6 -D0350_bit_5 -D0350_bit_4 -D0350_bit_3 -D0350_bit_2 -D0350_bit_1 -D0350_bit0 -D0351_bit_10 -D0351_bit_9 -D0351_bit_8 -D0351_bit_7 -D0351_bit_6 -D0351_bit_5 -D0351_bit_4 -D0351_bit_3 -D0351_bit_2 -D0351_bit_1 -D0351_bit0 -D0352_bit_10 -D0352_bit_9 -D0352_bit_8 -D0352_bit_7 -D0352_bit_6 -D0352_bit_5 -D0352_bit_4 -D0352_bit_3 -D0352_bit_2 -D0352_bit_1 -D0352_bit0 -D0353_bit_10 -D0353_bit_9 -D0353_bit_8 -D0353_bit_7 -D0353_bit_6 -D0353_bit_5 -D0353_bit_4 -D0353_bit_3 -D0353_bit_2 -D0353_bit_1 -D0353_bit0 -D0354_bit_10 -D0354_bit_9 -D0354_bit_8 -D0354_bit_7 -D0354_bit_6 -D0354_bit_5 -D0354_bit_4 -D0354_bit_3 -D0354_bit_2 -D0354_bit_1 -D0354_bit0 -D0355_bit_10 -D0355_bit_9 -D0355_bit_8 -D0355_bit_7 -D0355_bit_6 -D0355_bit_5 -D0355_bit_4 -D0355_bit_3 -D0355_bit_2 -D0355_bit_1 -D0355_bit0 -D0356_bit_10 -D0356_bit_9 -D0356_bit_8 -D0356_bit_7 -D0356_bit_6 -D0356_bit_5 -D0356_bit_4 -D0356_bit_3 -D0356_bit_2 -D0356_bit_1 -D0356_bit0 -D0357_bit_10 -D0357_bit_9 -D0357_bit_8 -D0357_bit_7 -D0357_bit_6 -D0357_bit_5 -D0357_bit_4 -D0357_bit_3 -D0357_bit_2 -D0357_bit_1 -D0357_bit0 -D0358_bit_10 -D0358_bit_9 -D0358_bit_8 -D0358_bit_7 -D0358_bit_6 -D0358_bit_5 -D0358_bit_4 -D0358_bit_3 -D0358_bit_2 -D0358_bit_1 -D0358_bit0 -D0359_bit_10 -D0359_bit_9 -D0359_bit_8 -D0359_bit_7 -D0359_bit_6 -D0359_bit_5 -D0359_bit_4 -D0359_bit_3 -D0359_bit_2 -D0359_bit_1 -D0359_bit0 -D0360_bit_10 -D0360_bit_9 -D0360_bit_8 -D0360_bit_7 -D0360_bit_6 -D0360_bit_5 -D0360_bit_4 -D0360_bit_3 -D0360_bit_2 -D0360_bit_1 -D0360_bit0 -D0361_bit_10 -D0361_bit_9 -D0361_bit_8 -D0361_bit_7 -D0361_bit_6 -D0361_bit_5 -D0361_bit_4 -D0361_bit_3 -D0361_bit_2 -D0361_bit_1 -D0361_bit0 -D0362_bit_10 -D0362_bit_9 -D0362_bit_8 -D0362_bit_7 -D0362_bit_6 -D0362_bit_5 -D0362_bit_4 -D0362_bit_3 -D0362_bit_2 -D0362_bit_1 -D0362_bit0 -D0363_bit_10 -D0363_bit_9 -D0363_bit_8 -D0363_bit_7 -D0363_bit_6 -D0363_bit_5 -D0363_bit_4 -D0363_bit_3 -D0363_bit_2 -D0363_bit_1 -D0363_bit0 -D0364_bit_10 -D0364_bit_9 -D0364_bit_8 -D0364_bit_7 -D0364_bit_6 -D0364_bit_5 -D0364_bit_4 -D0364_bit_3 -D0364_bit_2 -D0364_bit_1 -D0364_bit0 -D0365_bit_10 -D0365_bit_9 -D0365_bit_8 -D0365_bit_7 -D0365_bit_6 -D0365_bit_5 -D0365_bit_4 -D0365_bit_3 -D0365_bit_2 -D0365_bit_1 -D0365_bit0 -D0366_bit_10 -D0366_bit_9 -D0366_bit_8 -D0366_bit_7 -D0366_bit_6 -D0366_bit_5 -D0366_bit_4 -D0366_bit_3 -D0366_bit_2 -D0366_bit_1 -D0366_bit0 -D0367_bit_10 -D0367_bit_9 -D0367_bit_8 -D0367_bit_7 -D0367_bit_6 -D0367_bit_5 -D0367_bit_4 -D0367_bit_3 -D0367_bit_2 -D0367_bit_1 -D0367_bit0 -D0368_bit_10 -D0368_bit_9 -D0368_bit_8 -D0368_bit_7 -D0368_bit_6 -D0368_bit_5 -D0368_bit_4 -D0368_bit_3 -D0368_bit_2 -D0368_bit_1 -D0368_bit0 -D0369_bit_10 -D0369_bit_9 -D0369_bit_8 -D0369_bit_7 -D0369_bit_6 -D0369_bit_5 -D0369_bit_4 -D0369_bit_3 -D0369_bit_2 -D0369_bit_1 -D0369_bit0 -D0371_bit_10 -D0371_bit_9 -D0371_bit_8 -D0371_bit_7 -D0371_bit_6 -D0371_bit_5 -D0371_bit_4 -D0371_bit_3 -D0371_bit_2 -D0371_bit_1 -D0371_bit0 -D0372_bit_10 -D0372_bit_9 -D0372_bit_8 -D0372_bit_7 -D0372_bit_6 -D0372_bit_5 -D0372_bit_4 -D0372_bit_3 -D0372_bit_2 -D0372_bit_1 -D0372_bit0 -D0373_bit_10 -D0373_bit_9 -D0373_bit_8 -D0373_bit_7 -D0373_bit_6 -D0373_bit_5 -D0373_bit_4 -D0373_bit_3 -D0373_bit_2 -D0373_bit_1 -D0373_bit0 -D0375_bit_10 -D0375_bit_9 -D0375_bit_8 -D0375_bit_7 -D0375_bit_6 -D0375_bit_5 -D0375_bit_4 -D0375_bit_3 -D0375_bit_2 -D0375_bit_1 -D0375_bit0 -D0376_bit_10 -D0376_bit_9 -D0376_bit_8 -D0376_bit_7 -D0376_bit_6 -D0376_bit_5 -D0376_bit_4 -D0376_bit_3 -D0376_bit_2 -D0376_bit_1 -D0376_bit0 -D0377_bit_10 -D0377_bit_9 -D0377_bit_8 -D0377_bit_7 -D0377_bit_6 -D0377_bit_5 -D0377_bit_4 -D0377_bit_3 -D0377_bit_2 -D0377_bit_1 -D0377_bit0 -D0378_bit_10 -D0378_bit_9 -D0378_bit_8 -D0378_bit_7 -D0378_bit_6 -D0378_bit_5 -D0378_bit_4 -D0378_bit_3 -D0378_bit_2 -D0378_bit_1 -D0378_bit0 -D0379_bit_10 -D0379_bit_9 -D0379_bit_8 -D0379_bit_7 -D0379_bit_6 -D0379_bit_5 -D0379_bit_4 -D0379_bit_3 -D0379_bit_2 -D0379_bit_1 -D0379_bit0 -D0382_bit_10 -D0382_bit_9 -D0382_bit_8 -D0382_bit_7 -D0382_bit_6 -D0382_bit_5 -D0382_bit_4 -D0382_bit_3 -D0382_bit_2 -D0382_bit_1 -D0382_bit0 -D0383_bit_10 -D0383_bit_9 -D0383_bit_8 -D0383_bit_7 -D0383_bit_6 -D0383_bit_5 -D0383_bit_4 -D0383_bit_3 -D0383_bit_2 -D0383_bit_1 -D0383_bit0 -D0384_bit_10 -D0384_bit_9 -D0384_bit_8 -D0384_bit_7 -D0384_bit_6 -D0384_bit_5 -D0384_bit_4 -D0384_bit_3 -D0384_bit_2 -D0384_bit_1 -D0384_bit0 -D0385_bit_10 -D0385_bit_9 -D0385_bit_8 -D0385_bit_7 -D0385_bit_6 -D0385_bit_5 -D0385_bit_4 -D0385_bit_3 -D0385_bit_2 -D0385_bit_1 -D0385_bit0 -D0386_bit_10 -D0386_bit_9 -D0386_bit_8 -D0386_bit_7 -D0386_bit_6 -D0386_bit_5 -D0386_bit_4 -D0386_bit_3 -D0386_bit_2 -D0386_bit_1 -D0386_bit0 -D0387_bit_10 -D0387_bit_9 -D0387_bit_8 -D0387_bit_7 -D0387_bit_6 -D0387_bit_5 -D0387_bit_4 -D0387_bit_3 -D0387_bit_2 -D0387_bit_1 -D0387_bit0 -D0388_bit_10 -D0388_bit_9 -D0388_bit_8 -D0388_bit_7 -D0388_bit_6 -D0388_bit_5 -D0388_bit_4 -D0388_bit_3 -D0388_bit_2 -D0388_bit_1 -D0388_bit0 -D0389_bit_10 -D0389_bit_9 -D0389_bit_8 -D0389_bit_7 -D0389_bit_6 -D0389_bit_5 -D0389_bit_4 -D0389_bit_3 -D0389_bit_2 -D0389_bit_1 -D0389_bit0 -D0390_bit_10 -D0390_bit_9 -D0390_bit_8 -D0390_bit_7 -D0390_bit_6 -D0390_bit_5 -D0390_bit_4 -D0390_bit_3 -D0390_bit_2 -D0390_bit_1 -D0390_bit0 -D0391_bit_10 -D0391_bit_9 -D0391_bit_8 -D0391_bit_7 -D0391_bit_6 -D0391_bit_5 -D0391_bit_4 -D0391_bit_3 -D0391_bit_2 -D0391_bit_1 -D0391_bit0 -D0392_bit_10 -D0392_bit_9 -D0392_bit_8 -D0392_bit_7 -D0392_bit_6 -D0392_bit_5 -D0392_bit_4 -D0392_bit_3 -D0392_bit_2 -D0392_bit_1 -D0392_bit0 -D0394_bit_10 -D0394_bit_9 -D0394_bit_8 -D0394_bit_7 -D0394_bit_6 -D0394_bit_5 -D0394_bit_4 -D0394_bit_3 -D0394_bit_2 -D0394_bit_1 -D0394_bit0 -D0395_bit_10 -D0395_bit_9 -D0395_bit_8 -D0395_bit_7 -D0395_bit_6 -D0395_bit_5 -D0395_bit_4 -D0395_bit_3 -D0395_bit_2 -D0395_bit_1 -D0395_bit0 -D0396_bit_10 -D0396_bit_9 -D0396_bit_8 -D0396_bit_7 -D0396_bit_6 -D0396_bit_5 -D0396_bit_4 -D0396_bit_3 -D0396_bit_2 -D0396_bit_1 -D0396_bit0 -D0397_bit_10 -D0397_bit_9 -D0397_bit_8 -D0397_bit_7 -D0397_bit_6 -D0397_bit_5 -D0397_bit_4 -D0397_bit_3 -D0397_bit_2 -D0397_bit_1 -D0397_bit0 -D0398_bit_10 -D0398_bit_9 -D0398_bit_8 -D0398_bit_7 -D0398_bit_6 -D0398_bit_5 -D0398_bit_4 -D0398_bit_3 -D0398_bit_2 -D0398_bit_1 -D0398_bit0 -D0399_bit_10 -D0399_bit_9 -D0399_bit_8 -D0399_bit_7 -D0399_bit_6 -D0399_bit_5 -D0399_bit_4 -D0399_bit_3 -D0399_bit_2 -D0399_bit_1 -D0399_bit0 -D0400_bit_10 -D0400_bit_9 -D0400_bit_8 -D0400_bit_7 -D0400_bit_6 -D0400_bit_5 -D0400_bit_4 -D0400_bit_3 -D0400_bit_2 -D0400_bit_1 -D0400_bit0 -D0401_bit_10 -D0401_bit_9 -D0401_bit_8 -D0401_bit_7 -D0401_bit_6 -D0401_bit_5 -D0401_bit_4 -D0401_bit_3 -D0401_bit_2 -D0401_bit_1 -D0401_bit0 -D0403_bit_10 -D0403_bit_9 -D0403_bit_8 -D0403_bit_7 -D0403_bit_6 -D0403_bit_5 -D0403_bit_4 -D0403_bit_3 -D0403_bit_2 -D0403_bit_1 -D0403_bit0 -D0404_bit_10 -D0404_bit_9 -D0404_bit_8 -D0404_bit_7 -D0404_bit_6 -D0404_bit_5 -D0404_bit_4 -D0404_bit_3 -D0404_bit_2 -D0404_bit_1 -D0404_bit0 -D0405_bit_10 -D0405_bit_9 -D0405_bit_8 -D0405_bit_7 -D0405_bit_6 -D0405_bit_5 -D0405_bit_4 -D0405_bit_3 -D0405_bit_2 -D0405_bit_1 -D0405_bit0 -D0406_bit_10 -D0406_bit_9 -D0406_bit_8 -D0406_bit_7 -D0406_bit_6 -D0406_bit_5 -D0406_bit_4 -D0406_bit_3 -D0406_bit_2 -D0406_bit_1 -D0406_bit0 -D0407_bit_10 -D0407_bit_9 -D0407_bit_8 -D0407_bit_7 -D0407_bit_6 -D0407_bit_5 -D0407_bit_4 -D0407_bit_3 -D0407_bit_2 -D0407_bit_1 -D0407_bit0 -D0408_bit_10 -D0408_bit_9 -D0408_bit_8 -D0408_bit_7 -D0408_bit_6 -D0408_bit_5 -D0408_bit_4 -D0408_bit_3 -D0408_bit_2 -D0408_bit_1 -D0408_bit0 -D0409_bit_10 -D0409_bit_9 -D0409_bit_8 -D0409_bit_7 -D0409_bit_6 -D0409_bit_5 -D0409_bit_4 -D0409_bit_3 -D0409_bit_2 -D0409_bit_1 -D0409_bit0 -D0410_bit_10 -D0410_bit_9 -D0410_bit_8 -D0410_bit_7 -D0410_bit_6 -D0410_bit_5 -D0410_bit_4 -D0410_bit_3 -D0410_bit_2 -D0410_bit_1 -D0410_bit0 -D0411_bit_10 -D0411_bit_9 -D0411_bit_8 -D0411_bit_7 -D0411_bit_6 -D0411_bit_5 -D0411_bit_4 -D0411_bit_3 -D0411_bit_2 -D0411_bit_1 -D0411_bit0 -D0412_bit_10 -D0412_bit_9 -D0412_bit_8 -D0412_bit_7 -D0412_bit_6 -D0412_bit_5 -D0412_bit_4 -D0412_bit_3 -D0412_bit_2 -D0412_bit_1 -D0412_bit0 -D0413_bit_10 -D0413_bit_9 -D0413_bit_8 -D0413_bit_7 -D0413_bit_6 -D0413_bit_5 -D0413_bit_4 -D0413_bit_3 -D0413_bit_2 -D0413_bit_1 -D0413_bit0 -D0414_bit_10 -D0414_bit_9 -D0414_bit_8 -D0414_bit_7 -D0414_bit_6 -D0414_bit_5 -D0414_bit_4 -D0414_bit_3 -D0414_bit_2 -D0414_bit_1 -D0414_bit0 -D0415_bit_10 -D0415_bit_9 -D0415_bit_8 -D0415_bit_7 -D0415_bit_6 -D0415_bit_5 -D0415_bit_4 -D0415_bit_3 -D0415_bit_2 -D0415_bit_1 -D0415_bit0 -D0416_bit_10 -D0416_bit_9 -D0416_bit_8 -D0416_bit_7 -D0416_bit_6 -D0416_bit_5 -D0416_bit_4 -D0416_bit_3 -D0416_bit_2 -D0416_bit_1 -D0416_bit0 -D0417_bit_10 -D0417_bit_9 -D0417_bit_8 -D0417_bit_7 -D0417_bit_6 -D0417_bit_5 -D0417_bit_4 -D0417_bit_3 -D0417_bit_2 -D0417_bit_1 -D0417_bit0 -D0418_bit_10 -D0418_bit_9 -D0418_bit_8 -D0418_bit_7 -D0418_bit_6 -D0418_bit_5 -D0418_bit_4 -D0418_bit_3 -D0418_bit_2 -D0418_bit_1 -D0418_bit0 -D0419_bit_10 -D0419_bit_9 -D0419_bit_8 -D0419_bit_7 -D0419_bit_6 -D0419_bit_5 -D0419_bit_4 -D0419_bit_3 -D0419_bit_2 -D0419_bit_1 -D0419_bit0 -D0420_bit_10 -D0420_bit_9 -D0420_bit_8 -D0420_bit_7 -D0420_bit_6 -D0420_bit_5 -D0420_bit_4 -D0420_bit_3 -D0420_bit_2 -D0420_bit_1 -D0420_bit0 -D0421_bit_10 -D0421_bit_9 -D0421_bit_8 -D0421_bit_7 -D0421_bit_6 -D0421_bit_5 -D0421_bit_4 -D0421_bit_3 -D0421_bit_2 -D0421_bit_1 -D0421_bit0 -D0422_bit_10 -D0422_bit_9 -D0422_bit_8 -D0422_bit_7 -D0422_bit_6 -D0422_bit_5 -D0422_bit_4 -D0422_bit_3 -D0422_bit_2 -D0422_bit_1 -D0422_bit0 -D0423_bit_10 -D0423_bit_9 -D0423_bit_8 -D0423_bit_7 -D0423_bit_6 -D0423_bit_5 -D0423_bit_4 -D0423_bit_3 -D0423_bit_2 -D0423_bit_1 -D0423_bit0 -D0424_bit_10 -D0424_bit_9 -D0424_bit_8 -D0424_bit_7 -D0424_bit_6 -D0424_bit_5 -D0424_bit_4 -D0424_bit_3 -D0424_bit_2 -D0424_bit_1 -D0424_bit0 -D0426_bit_10 -D0426_bit_9 -D0426_bit_8 -D0426_bit_7 -D0426_bit_6 -D0426_bit_5 -D0426_bit_4 -D0426_bit_3 -D0426_bit_2 -D0426_bit_1 -D0426_bit0 -D0427_bit_10 -D0427_bit_9 -D0427_bit_8 -D0427_bit_7 -D0427_bit_6 -D0427_bit_5 -D0427_bit_4 -D0427_bit_3 -D0427_bit_2 -D0427_bit_1 -D0427_bit0 -D0428_bit_10 -D0428_bit_9 -D0428_bit_8 -D0428_bit_7 -D0428_bit_6 -D0428_bit_5 -D0428_bit_4 -D0428_bit_3 -D0428_bit_2 -D0428_bit_1 -D0428_bit0 -D0429_bit_10 -D0429_bit_9 -D0429_bit_8 -D0429_bit_7 -D0429_bit_6 -D0429_bit_5 -D0429_bit_4 -D0429_bit_3 -D0429_bit_2 -D0429_bit_1 -D0429_bit0 -D0430_bit_10 -D0430_bit_9 -D0430_bit_8 -D0430_bit_7 -D0430_bit_6 -D0430_bit_5 -D0430_bit_4 -D0430_bit_3 -D0430_bit_2 -D0430_bit_1 -D0430_bit0 -D0431_bit_10 -D0431_bit_9 -D0431_bit_8 -D0431_bit_7 -D0431_bit_6 -D0431_bit_5 -D0431_bit_4 -D0431_bit_3 -D0431_bit_2 -D0431_bit_1 -D0431_bit0 -D0432_bit_10 -D0432_bit_9 -D0432_bit_8 -D0432_bit_7 -D0432_bit_6 -D0432_bit_5 -D0432_bit_4 -D0432_bit_3 -D0432_bit_2 -D0432_bit_1 -D0432_bit0 -D0433_bit_10 -D0433_bit_9 -D0433_bit_8 -D0433_bit_7 -D0433_bit_6 -D0433_bit_5 -D0433_bit_4 -D0433_bit_3 -D0433_bit_2 -D0433_bit_1 -D0433_bit0 -D0434_bit_10 -D0434_bit_9 -D0434_bit_8 -D0434_bit_7 -D0434_bit_6 -D0434_bit_5 -D0434_bit_4 -D0434_bit_3 -D0434_bit_2 -D0434_bit_1 -D0434_bit0 -D0435_bit_10 -D0435_bit_9 -D0435_bit_8 -D0435_bit_7 -D0435_bit_6 -D0435_bit_5 -D0435_bit_4 -D0435_bit_3 -D0435_bit_2 -D0435_bit_1 -D0435_bit0 -D0436_bit_10 -D0436_bit_9 -D0436_bit_8 -D0436_bit_7 -D0436_bit_6 -D0436_bit_5 -D0436_bit_4 -D0436_bit_3 -D0436_bit_2 -D0436_bit_1 -D0436_bit0 -D0437_bit_10 -D0437_bit_9 -D0437_bit_8 -D0437_bit_7 -D0437_bit_6 -D0437_bit_5 -D0437_bit_4 -D0437_bit_3 -D0437_bit_2 -D0437_bit_1 -D0437_bit0 -D0438_bit_10 -D0438_bit_9 -D0438_bit_8 -D0438_bit_7 -D0438_bit_6 -D0438_bit_5 -D0438_bit_4 -D0438_bit_3 -D0438_bit_2 -D0438_bit_1 -D0438_bit0 -D0439_bit_10 -D0439_bit_9 -D0439_bit_8 -D0439_bit_7 -D0439_bit_6 -D0439_bit_5 -D0439_bit_4 -D0439_bit_3 -D0439_bit_2 -D0439_bit_1 -D0439_bit0 -D0440_bit_10 -D0440_bit_9 -D0440_bit_8 -D0440_bit_7 -D0440_bit_6 -D0440_bit_5 -D0440_bit_4 -D0440_bit_3 -D0440_bit_2 -D0440_bit_1 -D0440_bit0 -D0441_bit_10 -D0441_bit_9 -D0441_bit_8 -D0441_bit_7 -D0441_bit_6 -D0441_bit_5 -D0441_bit_4 -D0441_bit_3 -D0441_bit_2 -D0441_bit_1 -D0441_bit0 -D0442_bit_10 -D0442_bit_9 -D0442_bit_8 -D0442_bit_7 -D0442_bit_6 -D0442_bit_5 -D0442_bit_4 -D0442_bit_3 -D0442_bit_2 -D0442_bit_1 -D0442_bit0 -D0443_bit_10 -D0443_bit_9 -D0443_bit_8 -D0443_bit_7 -D0443_bit_6 -D0443_bit_5 -D0443_bit_4 -D0443_bit_3 -D0443_bit_2 -D0443_bit_1 -D0443_bit0 -D0444_bit_10 -D0444_bit_9 -D0444_bit_8 -D0444_bit_7 -D0444_bit_6 -D0444_bit_5 -D0444_bit_4 -D0444_bit_3 -D0444_bit_2 -D0444_bit_1 -D0444_bit0 -D0446_bit_10 -D0446_bit_9 -D0446_bit_8 -D0446_bit_7 -D0446_bit_6 -D0446_bit_5 -D0446_bit_4 -D0446_bit_3 -D0446_bit_2 -D0446_bit_1 -D0446_bit0 -D0447_bit_10 -D0447_bit_9 -D0447_bit_8 -D0447_bit_7 -D0447_bit_6 -D0447_bit_5 -D0447_bit_4 -D0447_bit_3 -D0447_bit_2 -D0447_bit_1 -D0447_bit0 -D0448_bit_10 -D0448_bit_9 -D0448_bit_8 -D0448_bit_7 -D0448_bit_6 -D0448_bit_5 -D0448_bit_4 -D0448_bit_3 -D0448_bit_2 -D0448_bit_1 -D0448_bit0 -D0449_bit_10 -D0449_bit_9 -D0449_bit_8 -D0449_bit_7 -D0449_bit_6 -D0449_bit_5 -D0449_bit_4 -D0449_bit_3 -D0449_bit_2 -D0449_bit_1 -D0449_bit0 -D0450_bit_10 -D0450_bit_9 -D0450_bit_8 -D0450_bit_7 -D0450_bit_6 -D0450_bit_5 -D0450_bit_4 -D0450_bit_3 -D0450_bit_2 -D0450_bit_1 -D0450_bit0 -D0451_bit_10 -D0451_bit_9 -D0451_bit_8 -D0451_bit_7 -D0451_bit_6 -D0451_bit_5 -D0451_bit_4 -D0451_bit_3 -D0451_bit_2 -D0451_bit_1 -D0451_bit0 -D0452_bit_10 -D0452_bit_9 -D0452_bit_8 -D0452_bit_7 -D0452_bit_6 -D0452_bit_5 -D0452_bit_4 -D0452_bit_3 -D0452_bit_2 -D0452_bit_1 -D0452_bit0 -D0453_bit_10 -D0453_bit_9 -D0453_bit_8 -D0453_bit_7 -D0453_bit_6 -D0453_bit_5 -D0453_bit_4 -D0453_bit_3 -D0453_bit_2 -D0453_bit_1 -D0453_bit0 -D0454_bit_10 -D0454_bit_9 -D0454_bit_8 -D0454_bit_7 -D0454_bit_6 -D0454_bit_5 -D0454_bit_4 -D0454_bit_3 -D0454_bit_2 -D0454_bit_1 -D0454_bit0 -D0455_bit_10 -D0455_bit_9 -D0455_bit_8 -D0455_bit_7 -D0455_bit_6 -D0455_bit_5 -D0455_bit_4 -D0455_bit_3 -D0455_bit_2 -D0455_bit_1 -D0455_bit0 -D0456_bit_10 -D0456_bit_9 -D0456_bit_8 -D0456_bit_7 -D0456_bit_6 -D0456_bit_5 -D0456_bit_4 -D0456_bit_3 -D0456_bit_2 -D0456_bit_1 -D0456_bit0 -D0457_bit_10 -D0457_bit_9 -D0457_bit_8 -D0457_bit_7 -D0457_bit_6 -D0457_bit_5 -D0457_bit_4 -D0457_bit_3 -D0457_bit_2 -D0457_bit_1 -D0457_bit0 -D0458_bit_10 -D0458_bit_9 -D0458_bit_8 -D0458_bit_7 -D0458_bit_6 -D0458_bit_5 -D0458_bit_4 -D0458_bit_3 -D0458_bit_2 -D0458_bit_1 -D0458_bit0 -D0459_bit_10 -D0459_bit_9 -D0459_bit_8 -D0459_bit_7 -D0459_bit_6 -D0459_bit_5 -D0459_bit_4 -D0459_bit_3 -D0459_bit_2 -D0459_bit_1 -D0459_bit0 -D0460_bit_10 -D0460_bit_9 -D0460_bit_8 -D0460_bit_7 -D0460_bit_6 -D0460_bit_5 -D0460_bit_4 -D0460_bit_3 -D0460_bit_2 -D0460_bit_1 -D0460_bit0 -D0461_bit_10 -D0461_bit_9 -D0461_bit_8 -D0461_bit_7 -D0461_bit_6 -D0461_bit_5 -D0461_bit_4 -D0461_bit_3 -D0461_bit_2 -D0461_bit_1 -D0461_bit0 -D0462_bit_10 -D0462_bit_9 -D0462_bit_8 -D0462_bit_7 -D0462_bit_6 -D0462_bit_5 -D0462_bit_4 -D0462_bit_3 -D0462_bit_2 -D0462_bit_1 -D0462_bit0 -D0463_bit_10 -D0463_bit_9 -D0463_bit_8 -D0463_bit_7 -D0463_bit_6 -D0463_bit_5 -D0463_bit_4 -D0463_bit_3 -D0463_bit_2 -D0463_bit_1 -D0463_bit0 -D0464_bit_10 -D0464_bit_9 -D0464_bit_8 -D0464_bit_7 -D0464_bit_6 -D0464_bit_5 -D0464_bit_4 -D0464_bit_3 -D0464_bit_2 -D0464_bit_1 -D0464_bit0 -D0465_bit_10 -D0465_bit_9 -D0465_bit_8 -D0465_bit_7 -D0465_bit_6 -D0465_bit_5 -D0465_bit_4 -D0465_bit_3 -D0465_bit_2 -D0465_bit_1 -D0465_bit0 -D0466_bit_10 -D0466_bit_9 -D0466_bit_8 -D0466_bit_7 -D0466_bit_6 -D0466_bit_5 -D0466_bit_4 -D0466_bit_3 -D0466_bit_2 -D0466_bit_1 -D0466_bit0 -D0467_bit_10 -D0467_bit_9 -D0467_bit_8 -D0467_bit_7 -D0467_bit_6 -D0467_bit_5 -D0467_bit_4 -D0467_bit_3 -D0467_bit_2 -D0467_bit_1 -D0467_bit0 -D0468_bit_10 -D0468_bit_9 -D0468_bit_8 -D0468_bit_7 -D0468_bit_6 -D0468_bit_5 -D0468_bit_4 -D0468_bit_3 -D0468_bit_2 -D0468_bit_1 -D0468_bit0 -D0469_bit_10 -D0469_bit_9 -D0469_bit_8 -D0469_bit_7 -D0469_bit_6 -D0469_bit_5 -D0469_bit_4 -D0469_bit_3 -D0469_bit_2 -D0469_bit_1 -D0469_bit0 -D0470_bit_10 -D0470_bit_9 -D0470_bit_8 -D0470_bit_7 -D0470_bit_6 -D0470_bit_5 -D0470_bit_4 -D0470_bit_3 -D0470_bit_2 -D0470_bit_1 -D0470_bit0 -D0471_bit_10 -D0471_bit_9 -D0471_bit_8 -D0471_bit_7 -D0471_bit_6 -D0471_bit_5 -D0471_bit_4 -D0471_bit_3 -D0471_bit_2 -D0471_bit_1 -D0471_bit0 -D0472_bit_10 -D0472_bit_9 -D0472_bit_8 -D0472_bit_7 -D0472_bit_6 -D0472_bit_5 -D0472_bit_4 -D0472_bit_3 -D0472_bit_2 -D0472_bit_1 -D0472_bit0 -D0473_bit_10 -D0473_bit_9 -D0473_bit_8 -D0473_bit_7 -D0473_bit_6 -D0473_bit_5 -D0473_bit_4 -D0473_bit_3 -D0473_bit_2 -D0473_bit_1 -D0473_bit0 -D0474_bit_10 -D0474_bit_9 -D0474_bit_8 -D0474_bit_7 -D0474_bit_6 -D0474_bit_5 -D0474_bit_4 -D0474_bit_3 -D0474_bit_2 -D0474_bit_1 -D0474_bit0 -D0475_bit_10 -D0475_bit_9 -D0475_bit_8 -D0475_bit_7 -D0475_bit_6 -D0475_bit_5 -D0475_bit_4 -D0475_bit_3 -D0475_bit_2 -D0475_bit_1 -D0475_bit0 -D0476_bit_10 -D0476_bit_9 -D0476_bit_8 -D0476_bit_7 -D0476_bit_6 -D0476_bit_5 -D0476_bit_4 -D0476_bit_3 -D0476_bit_2 -D0476_bit_1 -D0476_bit0 -D0477_bit_10 -D0477_bit_9 -D0477_bit_8 -D0477_bit_7 -D0477_bit_6 -D0477_bit_5 -D0477_bit_4 -D0477_bit_3 -D0477_bit_2 -D0477_bit_1 -D0477_bit0 -D0478_bit_10 -D0478_bit_9 -D0478_bit_8 -D0478_bit_7 -D0478_bit_6 -D0478_bit_5 -D0478_bit_4 -D0478_bit_3 -D0478_bit_2 -D0478_bit_1 -D0478_bit0 -D0479_bit_10 -D0479_bit_9 -D0479_bit_8 -D0479_bit_7 -D0479_bit_6 -D0479_bit_5 -D0479_bit_4 -D0479_bit_3 -D0479_bit_2 -D0479_bit_1 -D0479_bit0 -D0480_bit_10 -D0480_bit_9 -D0480_bit_8 -D0480_bit_7 -D0480_bit_6 -D0480_bit_5 -D0480_bit_4 -D0480_bit_3 -D0480_bit_2 -D0480_bit_1 -D0480_bit0 -D0481_bit_10 -D0481_bit_9 -D0481_bit_8 -D0481_bit_7 -D0481_bit_6 -D0481_bit_5 -D0481_bit_4 -D0481_bit_3 -D0481_bit_2 -D0481_bit_1 -D0481_bit0 -D0482_bit_10 -D0482_bit_9 -D0482_bit_8 -D0482_bit_7 -D0482_bit_6 -D0482_bit_5 -D0482_bit_4 -D0482_bit_3 -D0482_bit_2 -D0482_bit_1 -D0482_bit0 -D0483_bit_10 -D0483_bit_9 -D0483_bit_8 -D0483_bit_7 -D0483_bit_6 -D0483_bit_5 -D0483_bit_4 -D0483_bit_3 -D0483_bit_2 -D0483_bit_1 -D0483_bit0 -D0484_bit_10 -D0484_bit_9 -D0484_bit_8 -D0484_bit_7 -D0484_bit_6 -D0484_bit_5 -D0484_bit_4 -D0484_bit_3 -D0484_bit_2 -D0484_bit_1 -D0484_bit0 -D0485_bit_10 -D0485_bit_9 -D0485_bit_8 -D0485_bit_7 -D0485_bit_6 -D0485_bit_5 -D0485_bit_4 -D0485_bit_3 -D0485_bit_2 -D0485_bit_1 -D0485_bit0 D0003_bit0 D0015_bit0 D0019_bit0 D0027_bit0 D0029_bit0 D0032_bit0 D0036_bit0 D0040_bit0 D0046_bit0 D0050_bit0 D0051_bit0 D0058_bit0 D0059_bit0 D0061_bit0 D0066_bit0 D0067_bit0 D0069_bit0 D0076_bit0 D0078_bit0 D0088_bit0 D0092_bit0 D0096_bit0 D0099_bit0 D0100_bit0 D0103_bit0 D0110_bit0 D0111_bit0 D0112_bit0 D0114_bit0 D0122_bit0 D0127_bit0 D0136_bit0 D0146_bit0 D0147_bit0 D0150_bit0 D0154_bit0 D0155_bit0 D0156_bit0 D0158_bit0 D0159_bit0 D0160_bit0 D0161_bit0 D0177_bit0 D0181_bit0 D0185_bit0 D0191_bit0 D0193_bit0 D0194_bit0 D0199_bit0 D0200_bit0 D0218_bit0 D0226_bit0 D0232_bit0 D0233_bit0 D0239_bit0 D0240_bit0 D0244_bit0 D0253_bit0 D0255_bit0 D0256_bit0 D0257_bit0 D0272_bit0 D0273_bit0 D0274_bit0 D0284_bit0 D0294_bit0 -D0306_bit_10 -D0306_bit_9 -D0306_bit_8 -D0306_bit_7 -D0306_bit_6 -D0306_bit_5 -D0306_bit_4 -D0306_bit_3 -D0306_bit_2 D0306_bit_1 -D0306_bit0 D0310_bit_10 D0310_bit_9 D0310_bit_8 D0310_bit_7 D0310_bit_6 D0310_bit_5 D0310_bit_4 D0310_bit_3 D0310_bit_2 D0310_bit_1 -D0310_bit0 D0326_bit_10 D0326_bit_9 D0326_bit_8 D0326_bit_7 -D0326_bit_6 D0326_bit_5 D0326_bit_4 D0326_bit_3 -D0326_bit_2 -D0326_bit_1 -D0326_bit0 -D0339_bit_10 D0339_bit_9 -D0339_bit_8 D0339_bit_7 -D0339_bit_6 D0339_bit_5 D0339_bit_4 D0339_bit_3 -D0339_bit_2 -D0339_bit_1 -D0339_bit0 -D0342_bit_10 -D0342_bit_9 -D0342_bit_8 D0342_bit_7 -D0342_bit_6 -D0342_bit_5 -D0342_bit_4 D0342_bit_3 -D0342_bit_2 -D0342_bit_1 -D0342_bit0 D0370_bit_10 D0370_bit_9 D0370_bit_8 D0370_bit_7 D0370_bit_6 D0370_bit_5 D0370_bit_4 -D0370_bit_3 D0370_bit_2 D0370_bit_1 -D0370_bit0 D0374_bit_10 D0374_bit_9 -D0374_bit_8 D0374_bit_7 -D0374_bit_6 -D0374_bit_5 -D0374_bit_4 -D0374_bit_3 -D0374_bit_2 -D0374_bit_1 -D0374_bit0 -D0380_bit_10 D0380_bit_9 -D0380_bit_8 -D0380_bit_7 -D0380_bit_6 -D0380_bit_5 D0380_bit_4 D0380_bit_3 D0380_bit_2 D0380_bit_1 -D0380_bit0 D0381_bit_10 -D0381_bit_9 D0381_bit_8 D0381_bit_7 -D0381_bit_6 D0381_bit_5 -D0381_bit_4 -D0381_bit_3 -D0381_bit_2 -D0381_bit_1 -D0381_bit0 D0393_bit_10 D0393_bit_9 D0393_bit_8 D0393_bit_7 D0393_bit_6 D0393_bit_5 -D0393_bit_4 -D0393_bit_3 D0393_bit_2 D0393_bit_1 -D0393_bit0 D0402_bit_10 -D0402_bit_9 D0402_bit_8 -D0402_bit_7 -D0402_bit_6 -D0402_bit_5 D0402_bit_4 D0402_bit_3 D0402_bit_2 -D0402_bit_1 -D0402_bit0 D0425_bit_10 D0425_bit_9 D0425_bit_8 -D0425_bit_7 D0425_bit_6 D0425_bit_5 D0425_bit_4 D0425_bit_3 D0425_bit_2 D0425_bit_1 -D0425_bit0 D0445_bit_10 D0445_bit_9 -D0445_bit_8 -D0445_bit_7 -D0445_bit_6 D0445_bit_5 D0445_bit_4 D0445_bit_3 D0445_bit_2 D0445_bit_1 -D0445_bit0 A01_bit_10 A01_bit_9 A01_bit_8 A01_bit_7 A01_bit_6 A01_bit_5 A01_bit_4 A01_bit_3 A01_bit_2 A01_bit_1 A01_bit0 A01_bit1 A01_bit2 A01_bit3 A01_bit4 A01_bit5 A01_bit6 A01_bit7 A01_bit8 A01_bit9 A01_bit10 A01_bit11 A01_bit12 A01_bit13 A01_bit14 A01_bit15 A01_bit16 A01_bit17 A01_bit18 A01_bit19 A02_bit_10 A02_bit_9 A02_bit_8 A02_bit_7 A02_bit_6 A02_bit_5 A02_bit_4 A02_bit_3 A02_bit_2 A02_bit_1 A02_bit0 A02_bit1 A02_bit2 A02_bit3 A02_bit4 A02_bit5 A02_bit6 A02_bit7 A02_bit8 A02_bit9 A02_bit10 A02_bit11 A02_bit12 A02_bit13 A02_bit14 A02_bit15 A02_bit16 A02_bit17 A02_bit18 A02_bit19 A03_bit_10 A03_bit_9 A03_bit_8 A03_bit_7 A03_bit_6 A03_bit_5 A03_bit_4 A03_bit_3 A03_bit_2 A03_bit_1 A03_bit0 A03_bit1 A03_bit2 A03_bit3 A03_bit4 A03_bit5 A03_bit6 A03_bit7 A03_bit8 A03_bit9 A03_bit10 A03_bit11 A03_bit12 A03_bit13 A03_bit14 A03_bit15 A03_bit16 A03_bit17 A03_bit18 A03_bit19 A04_bit_10 A04_bit_9 A04_bit_8 A04_bit_7 A04_bit_6 A04_bit_5 A04_bit_4 A04_bit_3 A04_bit_2 A04_bit_1 A04_bit0 A04_bit1 A04_bit2 A04_bit3 A04_bit4 A04_bit5 A04_bit6 A04_bit7 A04_bit8 A04_bit9 A04_bit10 A04_bit11 A04_bit12 A04_bit13 A04_bit14 A04_bit15 A04_bit16 A04_bit17 A04_bit18 A04_bit19 A05_bit_10 A05_bit_9 A05_bit_8 A05_bit_7 A05_bit_6 A05_bit_5 A05_bit_4 A05_bit_3 A05_bit_2 A05_bit_1 A05_bit0 -A05_bit1 A05_bit2 A05_bit3 A05_bit4 A05_bit5 A05_bit6 A05_bit7 A05_bit8 A05_bit9 A05_bit10 A05_bit11 A05_bit12 A05_bit13 A05_bit14 A05_bit15 A05_bit16 A05_bit17 A05_bit18 A05_bit19 A06_bit_10 A06_bit_9 A06_bit_8 A06_bit_7 A06_bit_6 A06_bit_5 A06_bit_4 A06_bit_3 A06_bit_2 A06_bit_1 A06_bit0 A06_bit1 A06_bit2 A06_bit3 A06_bit4 A06_bit5 A06_bit6 A06_bit7 A06_bit8 A06_bit9 A06_bit10 A06_bit11 A06_bit12 A06_bit13 A06_bit14 A06_bit15 A06_bit16 A06_bit17 A06_bit18 A06_bit19 A07_bit_10 A07_bit_9 A07_bit_8 A07_bit_7 A07_bit_6 A07_bit_5 A07_bit_4 A07_bit_3 A07_bit_2 A07_bit_1 A07_bit0 A07_bit1 A07_bit2 A07_bit3 A07_bit4 A07_bit5 A07_bit6 A07_bit7 A07_bit8 A07_bit9 A07_bit10 A07_bit11 A07_bit12 A07_bit13 A07_bit14 A07_bit15 A07_bit16 A07_bit17 A07_bit18 A07_bit19 A08_bit_10 A08_bit_9 A08_bit_8 A08_bit_7 A08_bit_6 A08_bit_5 A08_bit_4 A08_bit_3 A08_bit_2 A08_bit_1 A08_bit0 A08_bit1 A08_bit2 A08_bit3 A08_bit4 A08_bit5 A08_bit6 A08_bit7 A08_bit8 A08_bit9 A08_bit10 A08_bit11 A08_bit12 A08_bit13 A08_bit14 A08_bit15 A08_bit16 A08_bit17 A08_bit18 A08_bit19 A09_bit_10 A09_bit_9 A09_bit_8 A09_bit_7 A09_bit_6 A09_bit_5 A09_bit_4 A09_bit_3 A09_bit_2 A09_bit_1 A09_bit0 A09_bit1 A09_bit2 A09_bit3 A09_bit4 A09_bit5 A09_bit6 A09_bit7 A09_bit8 A09_bit9 A09_bit10 A09_bit11 A09_bit12 A09_bit13 A09_bit14 A09_bit15 A09_bit16 A09_bit17 A09_bit18 A09_bit19 A10_bit_10 A10_bit_9 A10_bit_8 A10_bit_7 A10_bit_6 A10_bit_5 A10_bit_4 A10_bit_3 A10_bit_2 A10_bit_1 A10_bit0 A10_bit1 A10_bit2 A10_bit3 A10_bit4 A10_bit5 A10_bit6 A10_bit7 A10_bit8 A10_bit9 A10_bit10 A10_bit11 A10_bit12 A10_bit13 A10_bit14 A10_bit15 A10_bit16 A10_bit17 A10_bit18 A10_bit19 A11_bit_10 A11_bit_9 A11_bit_8 A11_bit_7 A11_bit_6 A11_bit_5 A11_bit_4 A11_bit_3 A11_bit_2 A11_bit_1 A11_bit0 A11_bit1 A11_bit2 A11_bit3 A11_bit4 A11_bit5 A11_bit6 A11_bit7 A11_bit8 A11_bit9 A11_bit10 A11_bit11 A11_bit12 A11_bit13 A11_bit14 A11_bit15 A11_bit16 A11_bit17 A11_bit18 A11_bit19 A12_bit_10 A12_bit_9 A12_bit_8 A12_bit_7 A12_bit_6 A12_bit_5 A12_bit_4 A12_bit_3 A12_bit_2 A12_bit_1 A12_bit0 A12_bit1 A12_bit2 A12_bit3 A12_bit4 A12_bit5 A12_bit6 A12_bit7 A12_bit8 A12_bit9 A12_bit10 A12_bit11 A12_bit12 A12_bit13 A12_bit14 A12_bit15 A12_bit16 A12_bit17 A12_bit18 A12_bit19 A13_bit_10 A13_bit_9 A13_bit_8 A13_bit_7 A13_bit_6 A13_bit_5 A13_bit_4 A13_bit_3 A13_bit_2 A13_bit_1 A13_bit0 A13_bit1 A13_bit2 A13_bit3 A13_bit4 A13_bit5 A13_bit6 A13_bit7 A13_bit8 A13_bit9 A13_bit10 A13_bit11 A13_bit12 A13_bit13 A13_bit14 A13_bit15 A13_bit16 A13_bit17 A13_bit18 A13_bit19 A14_bit_10 A14_bit_9 A14_bit_8 A14_bit_7 A14_bit_6 A14_bit_5 A14_bit_4 A14_bit_3 A14_bit_2 A14_bit_1 A14_bit0 A14_bit1 A14_bit2 A14_bit3 A14_bit4 A14_bit5 A14_bit6 A14_bit7 A14_bit8 A14_bit9 A14_bit10 A14_bit11 A14_bit12 A14_bit13 A14_bit14 A14_bit15 A14_bit16 A14_bit17 A14_bit18 A14_bit19 A15_bit_10 A15_bit_9 A15_bit_8 A15_bit_7 A15_bit_6 A15_bit_5 A15_bit_4 A15_bit_3 A15_bit_2 A15_bit_1 A15_bit0 A15_bit1 A15_bit2 A15_bit3 A15_bit4 A15_bit5 A15_bit6 A15_bit7 A15_bit8 A15_bit9 A15_bit10 A15_bit11 A15_bit12 A15_bit13 A15_bit14 A15_bit15 A15_bit16 A15_bit17 A15_bit18 A15_bit19 A16_bit_10 A16_bit_9 A16_bit_8 A16_bit_7 A16_bit_6 A16_bit_5 A16_bit_4 A16_bit_3 A16_bit_2 A16_bit_1 A16_bit0 A16_bit1 A16_bit2 A16_bit3 A16_bit4 A16_bit5 A16_bit6 A16_bit7 A16_bit8 A16_bit9 A16_bit10 A16_bit11 A16_bit12 A16_bit13 A16_bit14 A16_bit15 A16_bit16 A16_bit17 A16_bit18 A16_bit19 A17_bit_10 A17_bit_9 A17_bit_8 A17_bit_7 A17_bit_6 A17_bit_5 A17_bit_4 A17_bit_3 A17_bit_2 A17_bit_1 A17_bit0 A17_bit1 A17_bit2 A17_bit3 A17_bit4 A17_bit5 A17_bit6 A17_bit7 A17_bit8 A17_bit9 A17_bit10 A17_bit11 A17_bit12 A17_bit13 A17_bit14 A17_bit15 A17_bit16 A17_bit17 A17_bit18 A17_bit19 A18_bit_10 A18_bit_9 A18_bit_8 A18_bit_7 A18_bit_6 A18_bit_5 A18_bit_4 A18_bit_3 A18_bit_2 A18_bit_1 A18_bit0 A18_bit1 A18_bit2 A18_bit3 A18_bit4 A18_bit5 A18_bit6 A18_bit7 A18_bit8 A18_bit9 A18_bit10 A18_bit11 A18_bit12 A18_bit13 A18_bit14 A18_bit15 A18_bit16 A18_bit17 A18_bit18 A18_bit19 A19_bit_10 A19_bit_9 A19_bit_8 A19_bit_7 A19_bit_6 A19_bit_5 A19_bit_4 A19_bit_3 A19_bit_2 A19_bit_1 A19_bit0 A19_bit1 A19_bit2 A19_bit3 A19_bit4 A19_bit5 A19_bit6 A19_bit7 A19_bit8 A19_bit9 A19_bit10 A19_bit11 A19_bit12 A19_bit13 A19_bit14 A19_bit15 A19_bit16 A19_bit17 A19_bit18 A19_bit19 A20_bit_10 A20_bit_9 A20_bit_8 A20_bit_7 A20_bit_6 A20_bit_5 A20_bit_4 A20_bit_3 A20_bit_2 A20_bit_1 A20_bit0 A20_bit1 A20_bit2 A20_bit3 A20_bit4 A20_bit5 A20_bit6 A20_bit7 A20_bit8 A20_bit9 A20_bit10 A20_bit11 A20_bit12 A20_bit13 A20_bit14 A20_bit15 A20_bit16 A20_bit17 A20_bit18 A20_bit19 A21_bit_10 A21_bit_9 A21_bit_8 A21_bit_7 A21_bit_6 A21_bit_5 A21_bit_4 A21_bit_3 A21_bit_2 A21_bit_1 A21_bit0 A21_bit1 A21_bit2 A21_bit3 A21_bit4 A21_bit5 A21_bit6 A21_bit7 A21_bit8 A21_bit9 A21_bit10 A21_bit11 A21_bit12 A21_bit13 A21_bit14 A21_bit15 A21_bit16 A21_bit17 A21_bit18 A21_bit19 A22_bit_10 A22_bit_9 A22_bit_8 A22_bit_7 A22_bit_6 A22_bit_5 A22_bit_4 A22_bit_3 A22_bit_2 A22_bit_1 A22_bit0 A22_bit1 A22_bit2 A22_bit3 A22_bit4 A22_bit5 A22_bit6 A22_bit7 A22_bit8 A22_bit9 A22_bit10 A22_bit11 A22_bit12 A22_bit13 A22_bit14 A22_bit15 A22_bit16 A22_bit17 A22_bit18 A22_bit19 A23_bit_10 A23_bit_9 A23_bit_8 A23_bit_7 A23_bit_6 A23_bit_5 A23_bit_4 A23_bit_3 A23_bit_2 A23_bit_1 A23_bit0 A23_bit1 A23_bit2 A23_bit3 A23_bit4 A23_bit5 A23_bit6 A23_bit7 A23_bit8 A23_bit9 A23_bit10 A23_bit11 A23_bit12 A23_bit13 A23_bit14 A23_bit15 A23_bit16 A23_bit17 A23_bit18 A23_bit19 A24_bit_10 A24_bit_9 A24_bit_8 A24_bit_7 A24_bit_6 A24_bit_5 A24_bit_4 A24_bit_3 A24_bit_2 A24_bit_1 A24_bit0 -A24_bit1 A24_bit2 A24_bit3 A24_bit4 A24_bit5 A24_bit6 A24_bit7 A24_bit8 A24_bit9 A24_bit10 A24_bit11 A24_bit12 A24_bit13 A24_bit14 A24_bit15 A24_bit16 A24_bit17 A24_bit18 A24_bit19 A25_bit_10 A25_bit_9 A25_bit_8 A25_bit_7 A25_bit_6 A25_bit_5 A25_bit_4 A25_bit_3 A25_bit_2 A25_bit_1 A25_bit0 -A25_bit1 -A25_bit2 -A25_bit3 -A25_bit4 -A25_bit5 -A25_bit6 -A25_bit7 -A25_bit8 -A25_bit9 -A25_bit10 -A25_bit11 -A25_bit12 -A25_bit13 -A25_bit14 -A25_bit15 -A25_bit16 -A25_bit17 -A25_bit18 -A25_bit19 B25_bit_10 B25_bit_9 B25_bit_8 B25_bit_7 B25_bit_6 B25_bit_5 B25_bit_4 B25_bit_3 B25_bit_2 B25_bit_1 B25_bit0 -B25_bit1 -B25_bit2 -B25_bit3 -B25_bit4 -B25_bit5 -B25_bit6 -B25_bit7 -B25_bit8 -B25_bit9 -B25_bit10 -B25_bit11 -B25_bit12 -B25_bit13 -B25_bit14 -B25_bit15 -B25_bit16 -B25_bit17 -B25_bit18 -B25_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.78 0.95 0.91 2/54 15759 Raw data (stat): 15759 (runsolver) R 15758 4613 4612 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 859791208 884736 94 4294967295 134512640 135332820 3221224448 3221219612 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+3.08181 s] Raw data (loadavg): 0.80 0.95 0.91 1/53 15772 Raw data (stat): 15759 (runsolver) R 15758 4613 4612 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 859791208 884736 94 4294967295 134512640 135332820 3221224448 3221219612 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 0 Child status: 30 Real time (s): 3.08157 CPU time (s): 2.74558 CPU user time (s): 2.19967 CPU system time (s): 0.545917 CPU usage (%): 89.0968 Max. virtual memory (Kb): 864 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: FAILED ERROR: unsatisfied constraint on line 1025 #### END VERIFIER DATA ####