Update from HH
[Flyspeck/.git] / formal_lp / old / ineqs / tests / 168941837467_out.hl
1 needs "nobranching_lp.hl";;
2 \r
3 module Test_case = struct\r
4 let hypermap_string = "168941837467 17 6 0 1 2 3 4 5 4 0 5 6 7 3 6 5 8 3 8 5 4 3 8 4 3 3 8 3 9 4 9 3 10 11 3 10 3 2 3 10 2 12 3 12 2 1 3 12 1 0 3 12 0 11 3 6 8 9 3 11 10 12 3 11 0 7 3 9 11 7 3 7 6 9 ";;\r
5 let precision = 3;;\r
6 (***************)\r
7 (* Constraints *)\r
8 (***************)\r
9 let constraints = [\r
10 ("azim_sum", [8; 12; ], [(mk_real_int64 91L); (mk_real_int64 74L); ]);\r
11 ("azim_sum_neg", [1; 3; 4; 5; 6; 7; 10; 11; ], [(mk_real_int64 363L); (mk_real_int64 19L); (mk_real_int64 422L); (mk_real_int64 79L); (mk_real_int64 180L); (mk_real_int64 112L); (mk_real_int64 64L); (mk_real_int64 223L); ]);\r
12 ("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 884L); (mk_real_int64 826L); (mk_real_int64 1064L); (mk_real_int64 903L); (mk_real_int64 788L); (mk_real_int64 877L); (mk_real_int64 1064L); (mk_real_int64 884L); (mk_real_int64 914L); (mk_real_int64 1064L); (mk_real_int64 914L); (mk_real_int64 850L); (mk_real_int64 1064L); ]);\r
13 ("sol_sum3", [2; 6; 7; 9; ], [(mk_real_int64 27L); (mk_real_int64 91L); (mk_real_int64 84L); (mk_real_int64 23L); ]);\r
14 ("sol_sum3_neg", [3; 8; 11; 12; ], [(mk_real_int64 465L); (mk_real_int64 191L); (mk_real_int64 66L); (mk_real_int64 57L); ]);\r
15 ("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 798L); (mk_real_int64 798L); (mk_real_int64 826L); (mk_real_int64 598L); (mk_real_int64 884L); (mk_real_int64 772L); (mk_real_int64 788L); (mk_real_int64 788L); (mk_real_int64 581L); (mk_real_int64 821L); (mk_real_int64 884L); (mk_real_int64 914L); (mk_real_int64 914L); (mk_real_int64 796L); ]);\r
16 ("tau_sum4_neg", [0; 1; ], [(mk_real_int64 850L); (mk_real_int64 1064L); ]);\r
17 ("tau_sum6_neg", [0; ], [(mk_real_int64 884L); ]);\r
18 ("ln_def_neg", [2; 6; 8; 9; 10; 12; ], [(mk_real_int64 173L); (mk_real_int64 173L); (mk_real_int64 7L); (mk_real_int64 173L); (mk_real_int64 7L); (mk_real_int64 173L); ]);\r
19 ("ln_def", [0; 1; 3; 4; 5; 7; 11; ], [(mk_real_int64 25L); (mk_real_int64 90L); (mk_real_int64 4L); (mk_real_int64 131L); (mk_real_int64 32L); (mk_real_int64 25L); (mk_real_int64 63L); ]);\r
20 ("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 5555L); (mk_real_int64 5187L); (mk_real_int64 6683L); (mk_real_int64 5674L); (mk_real_int64 4951L); (mk_real_int64 5513L); (mk_real_int64 6683L); (mk_real_int64 5555L); (mk_real_int64 5741L); (mk_real_int64 6683L); (mk_real_int64 5741L); (mk_real_int64 5341L); (mk_real_int64 6683L); ]);\r
21 ("edge_sym", [0; 2; 3; 5; 8; 18; 31; 34; 37; 39; 40; 43; ], [(mk_real_int64 49L); (mk_real_int64 72L); (mk_real_int64 72L); (mk_real_int64 49L); (mk_real_int64 19L); (mk_real_int64 238L); (mk_real_int64 88L); (mk_real_int64 49L); (mk_real_int64 263L); (mk_real_int64 43L); (mk_real_int64 43L); (mk_real_int64 2L); ]);\r
22 ("edge_sym_neg", [21; 28; 30; 49; 52; ], [(mk_real_int64 161L); (mk_real_int64 88L); (mk_real_int64 180L); (mk_real_int64 43L); (mk_real_int64 98L); ]);\r
23 ("y1_def_neg", [0; 3; 18; 26; 27; 29; 30; 35; 39; 40; 42; 43; 44; 46; 48; 51; ], [(mk_real_int64 38L); (mk_real_int64 57L); (mk_real_int64 181L); (mk_real_int64 112L); (mk_real_int64 9L); (mk_real_int64 153L); (mk_real_int64 7L); (mk_real_int64 35L); (mk_real_int64 38L); (mk_real_int64 175L); (mk_real_int64 148L); (mk_real_int64 172L); (mk_real_int64 26L); (mk_real_int64 51L); (mk_real_int64 43L); (mk_real_int64 67L); ]);\r
24 ("y1_def", [17; 19; 21; 34; 36; 38; 41; 47; 54; ], [(mk_real_int64 163L); (mk_real_int64 31L); (mk_real_int64 133L); (mk_real_int64 83L); (mk_real_int64 156L); (mk_real_int64 72L); (mk_real_int64 86L); (mk_real_int64 25L); (mk_real_int64 63L); ]);\r
25 ("y2_def", [0; 3; 21; 27; 29; 38; 40; 43; 44; 47; 51; ], [(mk_real_int64 49L); (mk_real_int64 72L); (mk_real_int64 204L); (mk_real_int64 5L); (mk_real_int64 93L); (mk_real_int64 72L); (mk_real_int64 106L); (mk_real_int64 120L); (mk_real_int64 16L); (mk_real_int64 25L); (mk_real_int64 23L); ]);\r
26 ("y2_def_neg", [17; 18; 19; 26; 30; 34; 35; 36; 39; 41; 42; 46; 48; 54; ], [(mk_real_int64 55L); (mk_real_int64 63L); (mk_real_int64 123L); (mk_real_int64 112L); (mk_real_int64 7L); (mk_real_int64 43L); (mk_real_int64 35L); (mk_real_int64 64L); (mk_real_int64 38L); (mk_real_int64 26L); (mk_real_int64 148L); (mk_real_int64 81L); (mk_real_int64 43L); (mk_real_int64 19L); ]);\r
27 ("y3_def", [0; 3; 21; 27; 29; 38; 40; 43; 44; 47; 51; ], [(mk_real_int64 49L); (mk_real_int64 72L); (mk_real_int64 204L); (mk_real_int64 5L); (mk_real_int64 93L); (mk_real_int64 72L); (mk_real_int64 106L); (mk_real_int64 120L); (mk_real_int64 16L); (mk_real_int64 25L); (mk_real_int64 23L); ]);\r
28 ("y3_def_neg", [17; 18; 19; 26; 30; 34; 35; 36; 39; 41; 42; 46; 48; 54; ], [(mk_real_int64 55L); (mk_real_int64 63L); (mk_real_int64 123L); (mk_real_int64 112L); (mk_real_int64 7L); (mk_real_int64 43L); (mk_real_int64 35L); (mk_real_int64 64L); (mk_real_int64 38L); (mk_real_int64 26L); (mk_real_int64 148L); (mk_real_int64 81L); (mk_real_int64 43L); (mk_real_int64 19L); ]);\r
29 ("y4_def", [7; 9; 20; 22; 27; 40; ], [(mk_real_int64 268L); (mk_real_int64 122L); (mk_real_int64 180L); (mk_real_int64 288L); (mk_real_int64 132L); (mk_real_int64 98L); ]);\r
30 ("y4_def_neg", [8; 11; 12; 13; 15; 16; 21; 24; 25; 26; 28; 29; 30; 32; 33; 34; 37; ], [(mk_real_int64 158L); (mk_real_int64 142L); (mk_real_int64 78L); (mk_real_int64 10L); (mk_real_int64 175L); (mk_real_int64 5L); (mk_real_int64 25L); (mk_real_int64 37L); (mk_real_int64 26L); (mk_real_int64 200L); (mk_real_int64 103L); (mk_real_int64 225L); (mk_real_int64 30L); (mk_real_int64 16L); (mk_real_int64 13L); (mk_real_int64 30L); (mk_real_int64 98L); ]);\r
31 ("y5_def", [0; 3; 27; 29; 40; 43; 44; ], [(mk_real_int64 49L); (mk_real_int64 72L); (mk_real_int64 5L); (mk_real_int64 93L); (mk_real_int64 106L); (mk_real_int64 131L); (mk_real_int64 16L); ]);\r
32 ("y5_def_neg", [17; 18; 19; 21; 26; 30; 35; 36; 38; 39; 41; 42; 46; 47; 48; 54; ], [(mk_real_int64 42L); (mk_real_int64 30L); (mk_real_int64 96L); (mk_real_int64 64L); (mk_real_int64 78L); (mk_real_int64 5L); (mk_real_int64 25L); (mk_real_int64 24L); (mk_real_int64 37L); (mk_real_int64 26L); (mk_real_int64 26L); (mk_real_int64 103L); (mk_real_int64 58L); (mk_real_int64 13L); (mk_real_int64 30L); (mk_real_int64 19L); ]);\r
33 ("y6_def", [0; 3; 16; 27; 29; 34; 40; 41; 43; 44; 48; 51; ], [(mk_real_int64 49L); (mk_real_int64 72L); (mk_real_int64 200L); (mk_real_int64 5L); (mk_real_int64 93L); (mk_real_int64 49L); (mk_real_int64 106L); (mk_real_int64 327L); (mk_real_int64 131L); (mk_real_int64 16L); (mk_real_int64 13L); (mk_real_int64 43L); ]);\r
34 ("y6_def_neg", [17; 18; 19; 21; 26; 30; 35; 36; 38; 39; 42; 46; 47; 54; ], [(mk_real_int64 42L); (mk_real_int64 30L); (mk_real_int64 96L); (mk_real_int64 64L); (mk_real_int64 5L); (mk_real_int64 5L); (mk_real_int64 25L); (mk_real_int64 24L); (mk_real_int64 37L); (mk_real_int64 26L); (mk_real_int64 103L); (mk_real_int64 58L); (mk_real_int64 13L); (mk_real_int64 2L); ]);\r
35 ("RHA", [0; 2; 3; 6; 7; 9; 10; 11; 12; 13; 14; 15; 16; 18; 19; 20; 21; 26; 27; 28; 29; 30; 31; 32; 33; 35; 37; 38; 39; 40; 41; 42; 44; 45; 47; 50; 51; 53; 54; 55; ], [(mk_real_int64 30L); (mk_real_int64 19L); (mk_real_int64 180L); (mk_real_int64 64L); (mk_real_int64 34L); (mk_real_int64 64L); (mk_real_int64 52L); (mk_real_int64 86L); (mk_real_int64 79L); (mk_real_int64 79L); (mk_real_int64 86L); (mk_real_int64 27L); (mk_real_int64 52L); (mk_real_int64 116L); (mk_real_int64 279L); (mk_real_int64 465L); (mk_real_int64 392L); (mk_real_int64 180L); (mk_real_int64 165L); (mk_real_int64 19L); (mk_real_int64 36L); (mk_real_int64 131L); (mk_real_int64 112L); (mk_real_int64 96L); (mk_real_int64 115L); (mk_real_int64 96L); (mk_real_int64 126L); (mk_real_int64 303L); (mk_real_int64 333L); (mk_real_int64 191L); (mk_real_int64 29L); (mk_real_int64 56L); (mk_real_int64 136L); (mk_real_int64 180L); (mk_real_int64 150L); (mk_real_int64 150L); (mk_real_int64 57L); (mk_real_int64 118L); (mk_real_int64 54L); (mk_real_int64 268L); ]);\r
36 ("yy10", [6; 20; ], [(mk_real_int64 49L); (mk_real_int64 57L); ]);\r
37 ("tau4", [0; 1; ], [(mk_real_int64 108L); (mk_real_int64 570L); ]);\r
38 ("tau6", [0; ], [(mk_real_int64 884L); ]);\r
39 ("ineq105", [0; 3; ], [(mk_real_int64 121L); (mk_real_int64 180L); ]);\r
40 ("ineq106", [8; 11; 13; 15; 26; 29; 30; 37; ], [(mk_real_int64 122L); (mk_real_int64 74L); (mk_real_int64 15L); (mk_real_int64 255L); (mk_real_int64 292L); (mk_real_int64 242L); (mk_real_int64 43L); (mk_real_int64 93L); ]);\r
41 ("ineq107", [7; 9; 20; 22; 27; 32; 40; ], [(mk_real_int64 335L); (mk_real_int64 236L); (mk_real_int64 194L); (mk_real_int64 337L); (mk_real_int64 171L); (mk_real_int64 46L); (mk_real_int64 126L); ]);\r
42 ("ineq108", [29; ], [(mk_real_int64 97L); ]);\r
43 ("ineq109", [7; 20; 22; 29; ], [(mk_real_int64 27L); (mk_real_int64 91L); (mk_real_int64 84L); (mk_real_int64 23L); ]);\r
44 ("ineq110", [11; 24; 33; 37; ], [(mk_real_int64 465L); (mk_real_int64 191L); (mk_real_int64 66L); (mk_real_int64 57L); ]);\r
45 ("ineq111", [8; 9; 12; 16; 21; 25; 28; 32; 34; 37; ], [(mk_real_int64 596L); (mk_real_int64 483L); (mk_real_int64 621L); (mk_real_int64 40L); (mk_real_int64 197L); (mk_real_int64 209L); (mk_real_int64 821L); (mk_real_int64 411L); (mk_real_int64 238L); (mk_real_int64 182L); ]);\r
46 ("ineq112", [5; 20; ], [(mk_real_int64 661L); (mk_real_int64 163L); ]);\r
47 ("ineq113", [0; 9; 15; 20; 32; 35; 38; 40; ], [(mk_real_int64 661L); (mk_real_int64 116L); (mk_real_int64 553L); (mk_real_int64 205L); (mk_real_int64 255L); (mk_real_int64 501L); (mk_real_int64 465L); (mk_real_int64 164L); ]);\r
48 ("ineq114", [1; 4; 8; 13; 16; 18; 19; 21; 23; 25; 30; 33; 34; 36; 39; 41; ], [(mk_real_int64 137L); (mk_real_int64 137L); (mk_real_int64 229L); (mk_real_int64 263L); (mk_real_int64 179L); (mk_real_int64 120L); (mk_real_int64 300L); (mk_real_int64 109L); (mk_real_int64 482L); (mk_real_int64 373L); (mk_real_int64 218L); (mk_real_int64 134L); (mk_real_int64 40L); (mk_real_int64 266L); (mk_real_int64 86L); (mk_real_int64 545L); ]);\r
49 ("ineq119", [2; 6; ], [(mk_real_int64 492L); (mk_real_int64 396L); ]);\r
50 ("ineq120", [0; 1; 4; ], [(mk_real_int64 205L); (mk_real_int64 45L); (mk_real_int64 97L); ]);\r
51 ];;\r
52 \r
53 (***************)\r
54 (* Variables   *)\r
55 (***************)\r
56 let target_variables = [\r
57 ("ln_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 2875L); (mk_real_int64 2275L); (mk_real_int64 3475L); (mk_real_int64 3050L); (mk_real_int64 2575L); (mk_real_int64 3225L); (mk_real_int64 3475L); (mk_real_int64 2875L); (mk_real_int64 2325L); (mk_real_int64 3475L); (mk_real_int64 2325L); (mk_real_int64 2325L); (mk_real_int64 3475L); ]);\r
58 ];;\r
59 \r
60 (*************************)\r
61 \r
62 let variable_bounds = [\r
63 ("azim_hi", [1; 4; 6; 7; 8; 15; 17; 18; 24; 29; 30; 32; 33; 34; 35; 36; 37; 39; 44; 48; 49; 52; 54; ], [(mk_real_int64 422000L); (mk_real_int64 363000L); (mk_real_int64 390L); (mk_real_int64 110L); (mk_real_int64 124L); (mk_real_int64 873L); (mk_real_int64 1000L); (mk_real_int64 354L); (mk_real_int64 612L); (mk_real_int64 773L); (mk_real_int64 54L); (mk_real_int64 120L); (mk_real_int64 800L); (mk_real_int64 1264L); (mk_real_int64 234L); (mk_real_int64 1000L); (mk_real_int64 732L); (mk_real_int64 498L); (mk_real_int64 468L); (mk_real_int64 40L); (mk_real_int64 241L); (mk_real_int64 565L); (mk_real_int64 524L); ]);\r
64 ("azim_lo", [10; 11; 14; 19; 21; 22; 27; 46; 47; 50; 53; 55; ], [(mk_real_int64 199L); (mk_real_int64 238L); (mk_real_int64 238L); (mk_real_int64 1044L); (mk_real_int64 1000L); (mk_real_int64 474L); (mk_real_int64 362L); (mk_real_int64 45L); (mk_real_int64 116L); (mk_real_int64 484L); (mk_real_int64 164L); (mk_real_int64 830L); ]);\r
65 ("rhazim_hi", [1; 4; 16; ], [(mk_real_int64 96000L); (mk_real_int64 58000L); (mk_real_int64 1000L); ]);\r
66 ("rhazim_lo", [15; 20; 29; 43; 44; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
67 ("rho_hi", [0; 1; 2; 3; 4; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 56L); (mk_real_int64 3584L); (mk_real_int64 3176L); (mk_real_int64 452L); (mk_real_int64 792L); (mk_real_int64 3176L); (mk_real_int64 56L); (mk_real_int64 2576L); (mk_real_int64 3176L); (mk_real_int64 2576L); (mk_real_int64 400L); (mk_real_int64 3176L); ]);\r
68 ("rho_lo", [5; ], [(mk_real_int64 1932L); ]);\r
69 ("tau_lo", [4; 6; 14; 15; 16; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
70 ("tau_hi", [5; 11; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
71 ("y1_lo", [0; 21; 30; 35; 36; 40; 41; ], [(mk_real_int64 115L); (mk_real_int64 700L); (mk_real_int64 200L); (mk_real_int64 460L); (mk_real_int64 184L); (mk_real_int64 200L); (mk_real_int64 500L); ]);\r
72 ("y1_hi", [3; 17; 18; 19; 26; 34; 38; 39; 42; 43; 44; 46; 47; 48; 51; ], [(mk_real_int64 300L); (mk_real_int64 423L); (mk_real_int64 520L); (mk_real_int64 60L); (mk_real_int64 220L); (mk_real_int64 259L); (mk_real_int64 580L); (mk_real_int64 380L); (mk_real_int64 220L); (mk_real_int64 532L); (mk_real_int64 200L); (mk_real_int64 20L); (mk_real_int64 80L); (mk_real_int64 160L); (mk_real_int64 100L); ]);\r
73 ("y2_lo", [0; 21; 29; 30; 34; 35; 43; 44; 51; 54; ], [(mk_real_int64 358L); (mk_real_int64 364L); (mk_real_int64 180L); (mk_real_int64 200L); (mk_real_int64 229L); (mk_real_int64 460L); (mk_real_int64 77L); (mk_real_int64 348L); (mk_real_int64 248L); (mk_real_int64 152L); ]);\r
74 ("y2_hi", [3; 17; 18; 19; 26; 27; 36; 38; 39; 40; 41; 42; 46; 47; 48; ], [(mk_real_int64 360L); (mk_real_int64 3L); (mk_real_int64 128L); (mk_real_int64 188L); (mk_real_int64 220L); (mk_real_int64 460L); (mk_real_int64 92L); (mk_real_int64 580L); (mk_real_int64 380L); (mk_real_int64 288L); (mk_real_int64 8L); (mk_real_int64 220L); (mk_real_int64 28L); (mk_real_int64 80L); (mk_real_int64 160L); ]);\r
75 ("y3_lo", [0; 21; 29; 30; 34; 35; 43; 44; 51; 54; ], [(mk_real_int64 358L); (mk_real_int64 364L); (mk_real_int64 180L); (mk_real_int64 200L); (mk_real_int64 229L); (mk_real_int64 460L); (mk_real_int64 77L); (mk_real_int64 348L); (mk_real_int64 248L); (mk_real_int64 152L); ]);\r
76 ("y3_hi", [3; 17; 18; 19; 26; 27; 36; 38; 39; 40; 41; 42; 46; 47; 48; ], [(mk_real_int64 360L); (mk_real_int64 3L); (mk_real_int64 128L); (mk_real_int64 188L); (mk_real_int64 220L); (mk_real_int64 460L); (mk_real_int64 92L); (mk_real_int64 580L); (mk_real_int64 380L); (mk_real_int64 288L); (mk_real_int64 8L); (mk_real_int64 220L); (mk_real_int64 28L); (mk_real_int64 80L); (mk_real_int64 160L); ]);\r
77 ("y4_lo", [7; 8; 13; 20; 22; 24; 25; 26; 40; ], [(mk_real_int64 297L); (mk_real_int64 70L); (mk_real_int64 275L); (mk_real_int64 554L); (mk_real_int64 283L); (mk_real_int64 436L); (mk_real_int64 125L); (mk_real_int64 20L); (mk_real_int64 602L); ]);\r
78 ("y4_hi", [9; 11; 12; 15; 21; 27; 28; 29; 30; 32; 33; 34; 37; ], [(mk_real_int64 53L); (mk_real_int64 170L); (mk_real_int64 375L); (mk_real_int64 325L); (mk_real_int64 375L); (mk_real_int64 183L); (mk_real_int64 375L); (mk_real_int64 237L); (mk_real_int64 545L); (mk_real_int64 183L); (mk_real_int64 64L); (mk_real_int64 250L); (mk_real_int64 373L); ]);\r
79 ("y5_lo", [0; 17; 18; 19; 21; 29; 34; 36; 38; 39; 43; 44; 46; 51; 54; ], [(mk_real_int64 358L); (mk_real_int64 172L); (mk_real_int64 92L); (mk_real_int64 247L); (mk_real_int64 204L); (mk_real_int64 180L); (mk_real_int64 4L); (mk_real_int64 8L); (mk_real_int64 436L); (mk_real_int64 125L); (mk_real_int64 152L); (mk_real_int64 348L); (mk_real_int64 367L); (mk_real_int64 70L); (mk_real_int64 152L); ]);\r
80 ("y5_hi", [3; 26; 27; 35; 40; 41; 42; 47; 48; ], [(mk_real_int64 360L); (mk_real_int64 375L); (mk_real_int64 460L); (mk_real_int64 375L); (mk_real_int64 288L); (mk_real_int64 8L); (mk_real_int64 375L); (mk_real_int64 64L); (mk_real_int64 250L); ]);\r
81 ("y6_lo", [0; 16; 17; 18; 19; 21; 26; 29; 34; 36; 38; 39; 41; 43; 44; 46; 48; 51; 54; ], [(mk_real_int64 358L); (mk_real_int64 200000L); (mk_real_int64 172L); (mk_real_int64 92L); (mk_real_int64 247L); (mk_real_int64 204L); (mk_real_int64 72625L); (mk_real_int64 180L); (mk_real_int64 49004L); (mk_real_int64 8L); (mk_real_int64 436L); (mk_real_int64 125L); (mk_real_int64 353000L); (mk_real_int64 152L); (mk_real_int64 348L); (mk_real_int64 367L); (mk_real_int64 43000L); (mk_real_int64 43070L); (mk_real_int64 17152L); ]);\r
82 ("y6_hi", [3; 27; 35; 40; 41; 42; 47; 48; ], [(mk_real_int64 360L); (mk_real_int64 460L); (mk_real_int64 375L); (mk_real_int64 288L); (mk_real_int64 8L); (mk_real_int64 375L); (mk_real_int64 64L); (mk_real_int64 250L); ]);\r
83 ("ye_hi", [20; 21; 46; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
84 ("ye_lo", [8; 27; 41; 42; ], [(mk_real_int64 19000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
85 ("yn_lo", [1; 2; 8; 9; 10; 11; ], [(mk_real_int64 1070L); (mk_real_int64 148L); (mk_real_int64 1532L); (mk_real_int64 148L); (mk_real_int64 532L); (mk_real_int64 149L); ]);\r
86 ("yn_hi", [0; 3; 4; 5; 6; 7; 12; ], [(mk_real_int64 925L); (mk_real_int64 308L); (mk_real_int64 1087L); (mk_real_int64 1464L); (mk_real_int64 852L); (mk_real_int64 925L); (mk_real_int64 852L); ]);\r
87 ];;\r
88 let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
89 end;;\r
90 \r
91 concl (Test_case.result)\r