Update from HH
[Flyspeck/.git] / formal_lp / old / ineqs / tests / 156588677070_out.hl
1 needs "nobranching_lp.hl";;
2 \r
3 module Test_case = struct\r
4 let hypermap_string = "156588677070 21 6 0 1 2 3 4 5 4 0 5 6 7 3 6 5 4 3 6 4 8 3 8 4 9 3 9 4 3 3 9 3 10 3 10 3 11 3 11 3 2 3 11 2 1 3 11 1 12 3 12 1 13 3 13 1 0 3 13 0 7 3 13 7 14 3 14 7 8 3 7 6 8 3 14 8 9 4 14 9 10 12 3 10 11 12 3 12 13 14 ";;\r
5 let precision = 3;;\r
6 (***************)\r
7 (* Constraints *)\r
8 (***************)\r
9 let constraints = [\r
10 ("azim_sum", [5; 9; 14; ], [(mk_real_int64 202L); (mk_real_int64 91L); (mk_real_int64 506L); ]);\r
11 ("azim_sum_neg", [0; 3; 7; 8; 10; 11; ], [(mk_real_int64 38L); (mk_real_int64 167L); (mk_real_int64 38L); (mk_real_int64 38L); (mk_real_int64 50L); (mk_real_int64 50L); ]);\r
12 ("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 940L); (mk_real_int64 1283L); (mk_real_int64 1283L); (mk_real_int64 857L); (mk_real_int64 1283L); (mk_real_int64 1111L); (mk_real_int64 1111L); (mk_real_int64 902L); (mk_real_int64 1109L); (mk_real_int64 1111L); (mk_real_int64 1046L); (mk_real_int64 901L); (mk_real_int64 1111L); (mk_real_int64 1111L); (mk_real_int64 1111L); ]);\r
13 ("sol_sum3", [0; 5; 6; 7; ], [(mk_real_int64 38L); (mk_real_int64 50L); (mk_real_int64 6L); (mk_real_int64 6L); ]);\r
14 ("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; ], [(mk_real_int64 902L); (mk_real_int64 902L); (mk_real_int64 1109L); (mk_real_int64 1111L); (mk_real_int64 1046L); (mk_real_int64 901L); (mk_real_int64 857L); (mk_real_int64 857L); (mk_real_int64 901L); (mk_real_int64 1111L); (mk_real_int64 1111L); (mk_real_int64 1111L); (mk_real_int64 1111L); (mk_real_int64 1109L); (mk_real_int64 902L); (mk_real_int64 1109L); (mk_real_int64 901L); (mk_real_int64 1111L); ]);\r
15 ("tau_sum4_neg", [0; 1; ], [(mk_real_int64 902L); (mk_real_int64 1111L); ]);\r
16 ("tau_sum6_neg", [0; ], [(mk_real_int64 1283L); ]);\r
17 ("ln_def_neg", [0; 1; 2; 4; 5; 6; 8; 9; 10; 12; 13; 14; ], [(mk_real_int64 37L); (mk_real_int64 414L); (mk_real_int64 414L); (mk_real_int64 414L); (mk_real_int64 225L); (mk_real_int64 225L); (mk_real_int64 223L); (mk_real_int64 225L); (mk_real_int64 153L); (mk_real_int64 225L); (mk_real_int64 225L); (mk_real_int64 225L); ]);\r
18 ("ln_def", [3; 7; 11; ], [(mk_real_int64 55L); (mk_real_int64 5L); (mk_real_int64 7L); ]);\r
19 ("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 5908L); (mk_real_int64 8059L); (mk_real_int64 8059L); (mk_real_int64 5385L); (mk_real_int64 8059L); (mk_real_int64 6980L); (mk_real_int64 6980L); (mk_real_int64 5668L); (mk_real_int64 6968L); (mk_real_int64 6980L); (mk_real_int64 6572L); (mk_real_int64 5658L); (mk_real_int64 6980L); (mk_real_int64 6980L); (mk_real_int64 6980L); ]);\r
20 ("edge_sym_neg", [12; 15; 17; 18; 21; 23; 26; 27; 30; 36; 38; 39; 42; 47; 48; 50; 60; ], [(mk_real_int64 43L); (mk_real_int64 262L); (mk_real_int64 12L); (mk_real_int64 230L); (mk_real_int64 161L); (mk_real_int64 159L); (mk_real_int64 56L); (mk_real_int64 250L); (mk_real_int64 20L); (mk_real_int64 110L); (mk_real_int64 105L); (mk_real_int64 105L); (mk_real_int64 183L); (mk_real_int64 38L); (mk_real_int64 38L); (mk_real_int64 284L); (mk_real_int64 3L); ]);\r
21 ("edge_sym", [14; 33; 35; 45; 51; ], [(mk_real_int64 106L); (mk_real_int64 149L); (mk_real_int64 105L); (mk_real_int64 38L); (mk_real_int64 1L); ]);\r
22 ("y1_def_neg", [11; 12; 13; 14; 15; 17; 18; 19; 20; 21; 22; 23; 24; 25; 26; 27; 29; 31; 33; 34; 35; 36; 38; 41; 42; 44; 48; 49; 50; 51; 52; 54; 55; 62; 63; 67; ], [(mk_real_int64 65L); (mk_real_int64 6L); (mk_real_int64 125L); (mk_real_int64 191L); (mk_real_int64 101L); (mk_real_int64 104L); (mk_real_int64 222L); (mk_real_int64 21L); (mk_real_int64 303L); (mk_real_int64 103L); (mk_real_int64 60L); (mk_real_int64 142L); (mk_real_int64 163L); (mk_real_int64 87L); (mk_real_int64 331L); (mk_real_int64 8L); (mk_real_int64 12L); (mk_real_int64 107L); (mk_real_int64 158L); (mk_real_int64 73L); (mk_real_int64 97L); (mk_real_int64 124L); (mk_real_int64 151L); (mk_real_int64 103L); (mk_real_int64 247L); (mk_real_int64 247L); (mk_real_int64 54L); (mk_real_int64 65L); (mk_real_int64 1L); (mk_real_int64 113L); (mk_real_int64 112L); (mk_real_int64 257L); (mk_real_int64 1L); (mk_real_int64 57L); (mk_real_int64 77L); (mk_real_int64 175L); ]);\r
23 ("y1_def", [16; 30; 32; 53; 56; ], [(mk_real_int64 19L); (mk_real_int64 29L); (mk_real_int64 80L); (mk_real_int64 19L); (mk_real_int64 1L); ]);\r
24 ("y2_def_neg", [11; 12; 13; 16; 18; 20; 24; 26; 27; 30; 31; 32; 34; 38; 42; 44; 48; 51; 53; 54; 55; 63; 67; ], [(mk_real_int64 28L); (mk_real_int64 6L); (mk_real_int64 150L); (mk_real_int64 6L); (mk_real_int64 166L); (mk_real_int64 137L); (mk_real_int64 196L); (mk_real_int64 13L); (mk_real_int64 8L); (mk_real_int64 10L); (mk_real_int64 107L); (mk_real_int64 24L); (mk_real_int64 105L); (mk_real_int64 151L); (mk_real_int64 126L); (mk_real_int64 126L); (mk_real_int64 54L); (mk_real_int64 138L); (mk_real_int64 6L); (mk_real_int64 94L); (mk_real_int64 1L); (mk_real_int64 109L); (mk_real_int64 37L); ]);\r
25 ("y2_def", [14; 15; 17; 19; 21; 22; 23; 25; 29; 33; 35; 36; 41; 49; 50; 52; 62; ], [(mk_real_int64 116L); (mk_real_int64 61L); (mk_real_int64 63L); (mk_real_int64 33L); (mk_real_int64 62L); (mk_real_int64 57L); (mk_real_int64 86L); (mk_real_int64 53L); (mk_real_int64 7L); (mk_real_int64 96L); (mk_real_int64 59L); (mk_real_int64 75L); (mk_real_int64 62L); (mk_real_int64 99L); (mk_real_int64 1L); (mk_real_int64 68L); (mk_real_int64 35L); ]);\r
26 ("y3_def_neg", [11; 12; 13; 16; 18; 20; 24; 26; 27; 30; 31; 32; 34; 38; 42; 44; 48; 51; 53; 54; 55; 63; 67; ], [(mk_real_int64 28L); (mk_real_int64 6L); (mk_real_int64 150L); (mk_real_int64 6L); (mk_real_int64 166L); (mk_real_int64 137L); (mk_real_int64 196L); (mk_real_int64 13L); (mk_real_int64 8L); (mk_real_int64 10L); (mk_real_int64 107L); (mk_real_int64 24L); (mk_real_int64 105L); (mk_real_int64 151L); (mk_real_int64 126L); (mk_real_int64 126L); (mk_real_int64 54L); (mk_real_int64 138L); (mk_real_int64 6L); (mk_real_int64 94L); (mk_real_int64 1L); (mk_real_int64 109L); (mk_real_int64 37L); ]);\r
27 ("y3_def", [14; 15; 17; 19; 21; 22; 23; 25; 29; 33; 35; 36; 41; 49; 50; 52; 62; ], [(mk_real_int64 116L); (mk_real_int64 61L); (mk_real_int64 63L); (mk_real_int64 33L); (mk_real_int64 62L); (mk_real_int64 57L); (mk_real_int64 86L); (mk_real_int64 53L); (mk_real_int64 7L); (mk_real_int64 96L); (mk_real_int64 59L); (mk_real_int64 75L); (mk_real_int64 62L); (mk_real_int64 99L); (mk_real_int64 1L); (mk_real_int64 68L); (mk_real_int64 35L); ]);\r
28 ("y4_def_neg", [1; 3; 4; 5; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 19; 21; 23; 24; 25; 26; 28; 31; 32; 34; 38; 39; 40; 41; 42; 44; 45; 48; 49; 53; ], [(mk_real_int64 55L); (mk_real_int64 71L); (mk_real_int64 218L); (mk_real_int64 116L); (mk_real_int64 119L); (mk_real_int64 202L); (mk_real_int64 62L); (mk_real_int64 256L); (mk_real_int64 118L); (mk_real_int64 107L); (mk_real_int64 162L); (mk_real_int64 92L); (mk_real_int64 100L); (mk_real_int64 319L); (mk_real_int64 13L); (mk_real_int64 72L); (mk_real_int64 181L); (mk_real_int64 29L); (mk_real_int64 110L); (mk_real_int64 142L); (mk_real_int64 105L); (mk_real_int64 118L); (mk_real_int64 277L); (mk_real_int64 277L); (mk_real_int64 38L); (mk_real_int64 187L); (mk_real_int64 1L); (mk_real_int64 62L); (mk_real_int64 127L); (mk_real_int64 224L); (mk_real_int64 1L); (mk_real_int64 66L); (mk_real_int64 32L); (mk_real_int64 241L); ]);\r
29 ("y4_def", [2; 6; 17; 20; 22; 43; 46; ], [(mk_real_int64 12L); (mk_real_int64 29L); (mk_real_int64 16L); (mk_real_int64 49L); (mk_real_int64 124L); (mk_real_int64 30L); (mk_real_int64 1L); ]);\r
30 ("y5_def_neg", [11; 13; 16; 18; 20; 24; 30; 31; 32; 34; 38; 42; 44; 48; 51; 53; 54; 55; 61; 63; ], [(mk_real_int64 15L); (mk_real_int64 106L); (mk_real_int64 6L); (mk_real_int64 105L); (mk_real_int64 76L); (mk_real_int64 138L); (mk_real_int64 7L); (mk_real_int64 72L); (mk_real_int64 24L); (mk_real_int64 75L); (mk_real_int64 105L); (mk_real_int64 65L); (mk_real_int64 65L); (mk_real_int64 38L); (mk_real_int64 97L); (mk_real_int64 6L); (mk_real_int64 47L); (mk_real_int64 1L); (mk_real_int64 3L); (mk_real_int64 78L); ]);\r
31 ("y5_def", [12; 14; 15; 17; 19; 21; 22; 23; 25; 26; 27; 29; 33; 35; 36; 41; 49; 50; 52; 62; ], [(mk_real_int64 12L); (mk_real_int64 116L); (mk_real_int64 61L); (mk_real_int64 63L); (mk_real_int64 33L); (mk_real_int64 62L); (mk_real_int64 57L); (mk_real_int64 86L); (mk_real_int64 53L); (mk_real_int64 28L); (mk_real_int64 16L); (mk_real_int64 7L); (mk_real_int64 96L); (mk_real_int64 59L); (mk_real_int64 75L); (mk_real_int64 62L); (mk_real_int64 99L); (mk_real_int64 1L); (mk_real_int64 68L); (mk_real_int64 35L); ]);\r
32 ("y6_def_neg", [11; 13; 16; 18; 30; 32; 34; 38; 42; 48; 51; ], [(mk_real_int64 12L); (mk_real_int64 106L); (mk_real_int64 6L); (mk_real_int64 105L); (mk_real_int64 7L); (mk_real_int64 24L); (mk_real_int64 66L); (mk_real_int64 105L); (mk_real_int64 65L); (mk_real_int64 38L); (mk_real_int64 97L); ]);\r
33 ("y6_def", [10; 12; 14; 15; 17; 19; 21; 22; 23; 24; 25; 26; 27; 29; 31; 33; 35; 36; 40; 41; 43; 49; 50; 52; 53; 54; 56; 62; 63; 65; 66; ], [(mk_real_int64 3L); (mk_real_int64 12L); (mk_real_int64 116L); (mk_real_int64 61L); (mk_real_int64 63L); (mk_real_int64 206L); (mk_real_int64 62L); (mk_real_int64 167L); (mk_real_int64 86L); (mk_real_int64 105L); (mk_real_int64 115L); (mk_real_int64 28L); (mk_real_int64 16L); (mk_real_int64 7L); (mk_real_int64 226L); (mk_real_int64 96L); (mk_real_int64 59L); (mk_real_int64 75L); (mk_real_int64 319L); (mk_real_int64 65L); (mk_real_int64 248L); (mk_real_int64 99L); (mk_real_int64 1L); (mk_real_int64 230L); (mk_real_int64 436L); (mk_real_int64 187L); (mk_real_int64 230L); (mk_real_int64 328L); (mk_real_int64 176L); (mk_real_int64 346L); (mk_real_int64 38L); ]);\r
34 ("y8_def_neg", [4; ], [(mk_real_int64 3L); ]);\r
35 ("RHA", [6; 7; 9; 12; 14; 15; 26; 28; 29; 31; 33; 35; 36; 38; 52; 54; 55; 57; 62; 64; ], [(mk_real_int64 209L); (mk_real_int64 38L); (mk_real_int64 209L); (mk_real_int64 380L); (mk_real_int64 63L); (mk_real_int64 38L); (mk_real_int64 51L); (mk_real_int64 43L); (mk_real_int64 406L); (mk_real_int64 43L); (mk_real_int64 162L); (mk_real_int64 221L); (mk_real_int64 4L); (mk_real_int64 172L); (mk_real_int64 23L); (mk_real_int64 38L); (mk_real_int64 2L); (mk_real_int64 2L); (mk_real_int64 50L); (mk_real_int64 210L); ]);\r
36 ("RHB", [0; 2; 60; ], [(mk_real_int64 172L); (mk_real_int64 425L); (mk_real_int64 65L); ]);\r
37 ("tau4", [1; ], [(mk_real_int64 44L); ]);\r
38 ("tau6", [0; ], [(mk_real_int64 1283L); ]);\r
39 ("ineq106", [1; 4; 5; 7; 8; 10; 11; 12; 13; 15; 16; 19; 23; 25; 26; 31; 39; 40; 42; 44; 48; ], [(mk_real_int64 38L); (mk_real_int64 318L); (mk_real_int64 169L); (mk_real_int64 174L); (mk_real_int64 2L); (mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 65L); (mk_real_int64 237L); (mk_real_int64 145L); (mk_real_int64 331L); (mk_real_int64 20L); (mk_real_int64 264L); (mk_real_int64 161L); (mk_real_int64 207L); (mk_real_int64 172L); (mk_real_int64 2L); (mk_real_int64 2L); (mk_real_int64 186L); (mk_real_int64 169L); (mk_real_int64 96L); ]);\r
40 ("ineq107", [3; 6; 14; 20; 22; 24; 41; 43; 46; 49; ], [(mk_real_int64 38L); (mk_real_int64 38L); (mk_real_int64 50L); (mk_real_int64 60L); (mk_real_int64 161L); (mk_real_int64 50L); (mk_real_int64 38L); (mk_real_int64 38L); (mk_real_int64 1L); (mk_real_int64 50L); ]);\r
41 ("ineq108", [8; 9; 12; 32; 34; 39; 53; ], [(mk_real_int64 91L); (mk_real_int64 91L); (mk_real_int64 91L); (mk_real_int64 202L); (mk_real_int64 202L); (mk_real_int64 271L); (mk_real_int64 230L); ]);\r
42 ("ineq109", [2; 17; 20; 21; ], [(mk_real_int64 38L); (mk_real_int64 50L); (mk_real_int64 6L); (mk_real_int64 6L); ]);\r
43 ("ineq111", [1; 3; 8; 10; 14; 16; 21; 24; 28; 32; 34; 38; 41; 44; 45; 49; 53; ], [(mk_real_int64 233L); (mk_real_int64 802L); (mk_real_int64 1109L); (mk_real_int64 1111L); (mk_real_int64 1046L); (mk_real_int64 739L); (mk_real_int64 589L); (mk_real_int64 542L); (mk_real_int64 837L); (mk_real_int64 1111L); (mk_real_int64 1111L); (mk_real_int64 302L); (mk_real_int64 734L); (mk_real_int64 866L); (mk_real_int64 6L); (mk_real_int64 565L); (mk_real_int64 670L); ]);\r
44 ("ineq112", [20; ], [(mk_real_int64 199L); ]);\r
45 ("ineq113", [46; ], [(mk_real_int64 143L); ]);\r
46 ("ineq114", [2; 4; 16; 19; 23; 25; 26; 28; 38; 39; 42; 45; 47; 50; 53; ], [(mk_real_int64 669L); (mk_real_int64 100L); (mk_real_int64 161L); (mk_real_int64 659L); (mk_real_int64 268L); (mk_real_int64 353L); (mk_real_int64 6L); (mk_real_int64 274L); (mk_real_int64 809L); (mk_real_int64 375L); (mk_real_int64 36L); (mk_real_int64 812L); (mk_real_int64 148L); (mk_real_int64 336L); (mk_real_int64 441L); ]);\r
47 ("ineq119", [2; 6; ], [(mk_real_int64 84L); (mk_real_int64 278L); ]);\r
48 ("ineq120", [0; 3; 4; 5; ], [(mk_real_int64 542L); (mk_real_int64 276L); (mk_real_int64 668L); (mk_real_int64 120L); ]);\r
49 ];;\r
50 \r
51 (***************)\r
52 (* Variables   *)\r
53 (***************)\r
54 let target_variables = [\r
55 ("ln_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 3100L); (mk_real_int64 3675L); (mk_real_int64 3675L); (mk_real_int64 2625L); (mk_real_int64 3675L); (mk_real_int64 3500L); (mk_real_int64 3500L); (mk_real_int64 3100L); (mk_real_int64 3600L); (mk_real_int64 3500L); (mk_real_int64 2900L); (mk_real_int64 2850L); (mk_real_int64 3500L); (mk_real_int64 3500L); (mk_real_int64 3500L); ]);\r
56 ];;\r
57 \r
58 (*************************)\r
59 \r
60 let variable_bounds = [\r
61 ("azim_hi", [0; 2; 5; 9; 12; 28; 29; 30; 31; 48; 55; 58; 60; 64; 67; ], [(mk_real_int64 272L); (mk_real_int64 667000L); (mk_real_int64 38000L); (mk_real_int64 208L); (mk_real_int64 794L); (mk_real_int64 1000L); (mk_real_int64 534L); (mk_real_int64 107L); (mk_real_int64 1000L); (mk_real_int64 434L); (mk_real_int64 312L); (mk_real_int64 344L); (mk_real_int64 506L); (mk_real_int64 336L); (mk_real_int64 66L); ]);\r
62 ("azim_lo", [2; 6; 8; 14; 26; 33; 35; 36; 38; 49; 52; 56; 57; 59; ], [(mk_real_int64 200L); (mk_real_int64 164L); (mk_real_int64 52L); (mk_real_int64 400L); (mk_real_int64 214L); (mk_real_int64 232L); (mk_real_int64 22L); (mk_real_int64 244L); (mk_real_int64 476L); (mk_real_int64 250L); (mk_real_int64 464L); (mk_real_int64 37L); (mk_real_int64 352L); (mk_real_int64 40L); ]);\r
63 ("rhazim_hi", [2; 5; 36; 62; ], [(mk_real_int64 1000L); (mk_real_int64 343000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
64 ("rhazim_lo", [12; 28; 31; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
65 ("rho_hi", [1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 3372L); (mk_real_int64 3372L); (mk_real_int64 388L); (mk_real_int64 3372L); (mk_real_int64 1524L); (mk_real_int64 1524L); (mk_real_int64 168L); (mk_real_int64 956L); (mk_real_int64 1524L); (mk_real_int64 1064L); (mk_real_int64 3884L); (mk_real_int64 1524L); (mk_real_int64 1524L); (mk_real_int64 1524L); ]);\r
66 ("rho_lo", [0; ], [(mk_real_int64 1040L); ]);\r
67 ("tau_lo", [7; 18; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
68 ("tau_hi", [8; ], [(mk_real_int64 1000L); ]);\r
69 ("y1_lo", [13; 15; 17; 18; 19; 20; 21; 22; 23; 24; 26; 33; 36; 41; 42; 44; 48; 50; 51; 54; 55; 56; 62; ], [(mk_real_int64 360L); (mk_real_int64 400L); (mk_real_int64 400L); (mk_real_int64 205L); (mk_real_int64 385L); (mk_real_int64 180L); (mk_real_int64 200L); (mk_real_int64 385L); (mk_real_int64 200L); (mk_real_int64 280L); (mk_real_int64 620L); (mk_real_int64 400L); (mk_real_int64 200L); (mk_real_int64 200L); (mk_real_int64 450L); (mk_real_int64 450L); (mk_real_int64 360L); (mk_real_int64 200L); (mk_real_int64 120L); (mk_real_int64 280L); (mk_real_int64 80L); (mk_real_int64 500L); (mk_real_int64 600L); ]);\r
70 ("y1_hi", [11; 12; 14; 27; 30; 31; 32; 34; 35; 38; 49; 52; 63; 67; ], [(mk_real_int64 260L); (mk_real_int64 262L); (mk_real_int64 200L); (mk_real_int64 450L); (mk_real_int64 94L); (mk_real_int64 74L); (mk_real_int64 500L); (mk_real_int64 440L); (mk_real_int64 400L); (mk_real_int64 340L); (mk_real_int64 115L); (mk_real_int64 400L); (mk_real_int64 300L); (mk_real_int64 350L); ]);\r
71 ("y2_lo", [11; 13; 14; 20; 22; 25; 30; 32; 34; 35; 42; 44; 48; 50; 52; 54; 55; 56; 62; 63; ], [(mk_real_int64 108L); (mk_real_int64 136L); (mk_real_int64 248L); (mk_real_int64 372L); (mk_real_int64 216L); (mk_real_int64 220L); (mk_real_int64 26L); (mk_real_int64 472L); (mk_real_int64 160L); (mk_real_int64 396L); (mk_real_int64 452L); (mk_real_int64 452L); (mk_real_int64 360L); (mk_real_int64 272L); (mk_real_int64 296L); (mk_real_int64 364L); (mk_real_int64 80L); (mk_real_int64 152L); (mk_real_int64 56L); (mk_real_int64 300L); ]);\r
72 ("y2_hi", [12; 15; 16; 17; 18; 19; 21; 23; 24; 26; 27; 29; 31; 33; 36; 38; 41; 49; 51; 53; 67; ], [(mk_real_int64 262L); (mk_real_int64 516L); (mk_real_int64 224L); (mk_real_int64 336L); (mk_real_int64 232L); (mk_real_int64 124L); (mk_real_int64 608L); (mk_real_int64 268L); (mk_real_int64 120L); (mk_real_int64 464L); (mk_real_int64 450L); (mk_real_int64 280L); (mk_real_int64 74L); (mk_real_int64 96L); (mk_real_int64 348L); (mk_real_int64 340L); (mk_real_int64 608L); (mk_real_int64 372L); (mk_real_int64 104L); (mk_real_int64 224L); (mk_real_int64 120L); ]);\r
73 ("y3_lo", [11; 13; 14; 20; 22; 25; 30; 32; 34; 35; 42; 44; 48; 50; 52; 54; 55; 56; 62; 63; ], [(mk_real_int64 108L); (mk_real_int64 136L); (mk_real_int64 248L); (mk_real_int64 372L); (mk_real_int64 216L); (mk_real_int64 220L); (mk_real_int64 26L); (mk_real_int64 472L); (mk_real_int64 160L); (mk_real_int64 396L); (mk_real_int64 452L); (mk_real_int64 452L); (mk_real_int64 360L); (mk_real_int64 272L); (mk_real_int64 296L); (mk_real_int64 364L); (mk_real_int64 80L); (mk_real_int64 152L); (mk_real_int64 56L); (mk_real_int64 300L); ]);\r
74 ("y3_hi", [12; 15; 16; 17; 18; 19; 21; 23; 24; 26; 27; 29; 31; 33; 36; 38; 41; 49; 51; 53; 67; ], [(mk_real_int64 262L); (mk_real_int64 516L); (mk_real_int64 224L); (mk_real_int64 336L); (mk_real_int64 232L); (mk_real_int64 124L); (mk_real_int64 608L); (mk_real_int64 268L); (mk_real_int64 120L); (mk_real_int64 464L); (mk_real_int64 450L); (mk_real_int64 280L); (mk_real_int64 74L); (mk_real_int64 96L); (mk_real_int64 348L); (mk_real_int64 340L); (mk_real_int64 608L); (mk_real_int64 372L); (mk_real_int64 104L); (mk_real_int64 224L); (mk_real_int64 120L); ]);\r
75 ("y4_lo", [1; 7; 8; 9; 10; 13; 14; 16; 19; 20; 24; 25; 32; 34; 39; 40; 41; 42; 43; 44; 46; 53; ], [(mk_real_int64 155L); (mk_real_int64 190L); (mk_real_int64 330L); (mk_real_int64 335L); (mk_real_int64 695L); (mk_real_int64 345L); (mk_real_int64 100L); (mk_real_int64 110L); (mk_real_int64 700L); (mk_real_int64 676L); (mk_real_int64 100L); (mk_real_int64 285L); (mk_real_int64 245L); (mk_real_int64 245L); (mk_real_int64 5L); (mk_real_int64 370L); (mk_real_int64 376L); (mk_real_int64 410L); (mk_real_int64 626L); (mk_real_int64 15L); (mk_real_int64 227L); (mk_real_int64 300L); ]);\r
76 ("y4_hi", [2; 3; 4; 5; 6; 11; 12; 15; 17; 21; 22; 23; 26; 28; 31; 38; 45; 48; 49; ], [(mk_real_int64 312L); (mk_real_int64 124L); (mk_real_int64 170L); (mk_real_int64 235L); (mk_real_int64 374L); (mk_real_int64 180L); (mk_real_int64 140L); (mk_real_int64 675L); (mk_real_int64 200L); (mk_real_int64 319L); (mk_real_int64 453L); (mk_real_int64 160L); (mk_real_int64 205L); (mk_real_int64 375L); (mk_real_int64 180L); (mk_real_int64 250L); (mk_real_int64 250L); (mk_real_int64 240L); (mk_real_int64 25L); ]);\r
77 ("y5_lo", [11; 13; 14; 20; 22; 24; 25; 30; 32; 34; 35; 42; 44; 50; 51; 52; 56; 62; 63; 67; ], [(mk_real_int64 293L); (mk_real_int64 26L); (mk_real_int64 248L); (mk_real_int64 267L); (mk_real_int64 216L); (mk_real_int64 350L); (mk_real_int64 220L); (mk_real_int64 176L); (mk_real_int64 472L); (mk_real_int64 350L); (mk_real_int64 396L); (mk_real_int64 347L); (mk_real_int64 347L); (mk_real_int64 272L); (mk_real_int64 526L); (mk_real_int64 296L); (mk_real_int64 152L); (mk_real_int64 56L); (mk_real_int64 225L); (mk_real_int64 30L); ]);\r
78 ("y5_hi", [12; 15; 16; 17; 18; 19; 21; 23; 26; 27; 29; 31; 33; 36; 38; 41; 48; 49; 53; 54; 55; ], [(mk_real_int64 312L); (mk_real_int64 516L); (mk_real_int64 224L); (mk_real_int64 336L); (mk_real_int64 227L); (mk_real_int64 124L); (mk_real_int64 608L); (mk_real_int64 268L); (mk_real_int64 109L); (mk_real_int64 200L); (mk_real_int64 280L); (mk_real_int64 319L); (mk_real_int64 96L); (mk_real_int64 348L); (mk_real_int64 375L); (mk_real_int64 608L); (mk_real_int64 250L); (mk_real_int64 372L); (mk_real_int64 224L); (mk_real_int64 266L); (mk_real_int64 250L); ]);\r
79 ("y6_lo", [10; 11; 13; 14; 19; 20; 22; 24; 25; 30; 31; 32; 34; 35; 40; 41; 42; 43; 44; 50; 51; 52; 53; 54; 55; 56; 62; 63; 65; 66; 67; ], [(mk_real_int64 3000L); (mk_real_int64 3293L); (mk_real_int64 26L); (mk_real_int64 248L); (mk_real_int64 173000L); (mk_real_int64 76267L); (mk_real_int64 111000L); (mk_real_int64 244000L); (mk_real_int64 62220L); (mk_real_int64 176L); (mk_real_int64 297681L); (mk_real_int64 472L); (mk_real_int64 10000L); (mk_real_int64 396L); (mk_real_int64 319000L); (mk_real_int64 3000L); (mk_real_int64 347L); (mk_real_int64 248000L); (mk_real_int64 65347L); (mk_real_int64 272L); (mk_real_int64 526L); (mk_real_int64 162296L); (mk_real_int64 442000L); (mk_real_int64 233734L); (mk_real_int64 750L); (mk_real_int64 231000L); (mk_real_int64 293056L); (mk_real_int64 254225L); (mk_real_int64 346000L); (mk_real_int64 38000L); (mk_real_int64 30L); ]);\r
80 ("y6_hi", [12; 15; 16; 17; 18; 19; 21; 22; 23; 24; 26; 27; 29; 33; 34; 36; 38; 41; 48; 49; 53; 56; ], [(mk_real_int64 312L); (mk_real_int64 516L); (mk_real_int64 224L); (mk_real_int64 336L); (mk_real_int64 227L); (mk_real_int64 124L); (mk_real_int64 608L); (mk_real_int64 784L); (mk_real_int64 268L); (mk_real_int64 650L); (mk_real_int64 109L); (mk_real_int64 200L); (mk_real_int64 280L); (mk_real_int64 96L); (mk_real_int64 650L); (mk_real_int64 348L); (mk_real_int64 375L); (mk_real_int64 608L); (mk_real_int64 250L); (mk_real_int64 372L); (mk_real_int64 224L); (mk_real_int64 848L); ]);\r
81 ("y8_hi", [4; ], [(mk_real_int64 3000L); ]);\r
82 ("ye_lo", [13; 15; 16; 17; 33; 40; 45; 56; ], [(mk_real_int64 149000L); (mk_real_int64 1000L); (mk_real_int64 39000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 315000L); (mk_real_int64 1000L); ]);\r
83 ("ye_hi", [31; 50; 54; 55; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
84 ("yn_hi", [0; 2; 4; 5; 6; 7; 8; 9; 10; 12; 13; 14; ], [(mk_real_int64 188L); (mk_real_int64 536L); (mk_real_int64 536L); (mk_real_int64 900L); (mk_real_int64 900L); (mk_real_int64 1385L); (mk_real_int64 2052L); (mk_real_int64 900L); (mk_real_int64 372L); (mk_real_int64 900L); (mk_real_int64 900L); (mk_real_int64 900L); ]);\r
85 ("yn_lo", [1; 3; 11; ], [(mk_real_int64 1464L); (mk_real_int64 765L); (mk_real_int64 461L); ]);\r
86 ];;\r
87 let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
88 end;;\r
89 \r
90 concl (Test_case.result)\r