Update from HH

[Flyspeck/.git] / formal_lp / old / ineqs / tests2 / 63626063287_out.hl

needs "nobranching_lp.hl";;
\r
module Test_case = struct\r
let hypermap_string = "63626063287 22 4 0 1 2 3 3 0 3 4 3 4 3 5 3 5 3 2 3 5 2 6 3 6 2 7 3 7 2 1 3 7 1 8 3 8 1 9 3 9 1 0 4 9 0 4 10 3 10 4 11 3 11 4 5 4 11 5 6 12 3 12 6 13 3 13 6 7 4 13 7 8 14 3 14 8 10 3 8 9 10 3 14 10 11 3 14 11 12 3 12 13 14 ";;\r
let precision = 3;;\r
(***************)\r
(* Constraints *)\r
(***************)\r
let constraints = [\r
("azim_sum", [1; 2; 4; 5; 7; 8; 10; 11; ], [(mk_real_int64 339L); (mk_real_int64 181L); (mk_real_int64 181L); (mk_real_int64 5L); (mk_real_int64 331L); (mk_real_int64 5L); (mk_real_int64 339L); (mk_real_int64 331L); ]);\r
("azim_sum_neg", [12; 13; ], [(mk_real_int64 187L); (mk_real_int64 187L); ]);\r
("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 927L); (mk_real_int64 1080L); (mk_real_int64 1080L); (mk_real_int64 927L); (mk_real_int64 1080L); (mk_real_int64 1080L); (mk_real_int64 1080L); (mk_real_int64 1080L); (mk_real_int64 1080L); (mk_real_int64 927L); (mk_real_int64 1080L); (mk_real_int64 1080L); (mk_real_int64 991L); (mk_real_int64 991L); (mk_real_int64 1080L); ]);\r
("sol_sum3_neg", [5; 6; 9; 10; ], [(mk_real_int64 181L); (mk_real_int64 5L); (mk_real_int64 181L); (mk_real_int64 5L); ]);\r
("sol_sum3", [11; 17; ], [(mk_real_int64 187L); (mk_real_int64 187L); ]);\r
("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; ], [(mk_real_int64 927L); (mk_real_int64 927L); (mk_real_int64 927L); (mk_real_int64 1080L); (mk_real_int64 1080L); (mk_real_int64 1080L); (mk_real_int64 1080L); (mk_real_int64 927L); (mk_real_int64 927L); (mk_real_int64 1080L); (mk_real_int64 1080L); (mk_real_int64 991L); (mk_real_int64 991L); (mk_real_int64 1080L); (mk_real_int64 927L); (mk_real_int64 1080L); (mk_real_int64 991L); (mk_real_int64 991L); ]);\r
("tau_sum4_neg", [0; 1; 2; 3; ], [(mk_real_int64 927L); (mk_real_int64 927L); (mk_real_int64 1080L); (mk_real_int64 1080L); ]);\r
("ln_def_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 23L); (mk_real_int64 191L); (mk_real_int64 191L); (mk_real_int64 23L); (mk_real_int64 191L); (mk_real_int64 191L); (mk_real_int64 191L); (mk_real_int64 191L); (mk_real_int64 191L); (mk_real_int64 23L); (mk_real_int64 191L); (mk_real_int64 191L); (mk_real_int64 93L); (mk_real_int64 93L); (mk_real_int64 191L); ]);\r
("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 5827L); (mk_real_int64 6785L); (mk_real_int64 6785L); (mk_real_int64 5827L); (mk_real_int64 6785L); (mk_real_int64 6785L); (mk_real_int64 6785L); (mk_real_int64 6785L); (mk_real_int64 6785L); (mk_real_int64 5827L); (mk_real_int64 6785L); (mk_real_int64 6785L); (mk_real_int64 6230L); (mk_real_int64 6230L); (mk_real_int64 6785L); ]);\r
("edge_sym", [0; 1; 5; 9; 12; 17; 33; 46; 53; ], [(mk_real_int64 49L); (mk_real_int64 216L); (mk_real_int64 136L); (mk_real_int64 29L); (mk_real_int64 39L); (mk_real_int64 59L); (mk_real_int64 216L); (mk_real_int64 36L); (mk_real_int64 2L); ]);\r
("edge_sym_neg", [6; 8; 14; 15; 18; 21; 23; 24; 26; 27; 36; 37; 40; 47; 56; 57; 63; 66; ], [(mk_real_int64 49L); (mk_real_int64 106L); (mk_real_int64 44L); (mk_real_int64 2L); (mk_real_int64 266L); (mk_real_int64 224L); (mk_real_int64 295L); (mk_real_int64 2L); (mk_real_int64 136L); (mk_real_int64 39L); (mk_real_int64 47L); (mk_real_int64 59L); (mk_real_int64 2L); (mk_real_int64 54L); (mk_real_int64 39L); (mk_real_int64 44L); (mk_real_int64 266L); (mk_real_int64 36L); ]);\r
("y1_def_neg", [1; 5; 7; 8; 9; 10; 13; 14; 15; 16; 17; 18; 19; 20; 22; 23; 24; 25; 26; 30; 33; 35; 36; 38; 39; 40; 42; 45; 46; 47; 49; 53; 56; 57; 58; 62; 63; 64; 69; ], [(mk_real_int64 39L); (mk_real_int64 71L); (mk_real_int64 78L); (mk_real_int64 108L); (mk_real_int64 93L); (mk_real_int64 116L); (mk_real_int64 1L); (mk_real_int64 38L); (mk_real_int64 144L); (mk_real_int64 106L); (mk_real_int64 73L); (mk_real_int64 13L); (mk_real_int64 35L); (mk_real_int64 163L); (mk_real_int64 77L); (mk_real_int64 41L); (mk_real_int64 192L); (mk_real_int64 93L); (mk_real_int64 186L); (mk_real_int64 71L); (mk_real_int64 39L); (mk_real_int64 37L); (mk_real_int64 194L); (mk_real_int64 77L); (mk_real_int64 41L); (mk_real_int64 192L); (mk_real_int64 2L); (mk_real_int64 28L); (mk_real_int64 31L); (mk_real_int64 114L); (mk_real_int64 111L); (mk_real_int64 2L); (mk_real_int64 145L); (mk_real_int64 38L); (mk_real_int64 116L); (mk_real_int64 179L); (mk_real_int64 13L); (mk_real_int64 53L); (mk_real_int64 173L); ]);\r
("y1_def", [37; 48; 66; ], [(mk_real_int64 34L); (mk_real_int64 94L); (mk_real_int64 36L); ]);\r
("y2_def", [1; 7; 9; 10; 13; 14; 17; 18; 19; 22; 23; 25; 33; 35; 37; 38; 39; 42; 46; 53; 57; 58; 62; 63; 64; ], [(mk_real_int64 49L); (mk_real_int64 47L); (mk_real_int64 57L); (mk_real_int64 31L); (mk_real_int64 2L); (mk_real_int64 59L); (mk_real_int64 113L); (mk_real_int64 20L); (mk_real_int64 55L); (mk_real_int64 119L); (mk_real_int64 64L); (mk_real_int64 57L); (mk_real_int64 49L); (mk_real_int64 57L); (mk_real_int64 123L); (mk_real_int64 119L); (mk_real_int64 64L); (mk_real_int64 2L); (mk_real_int64 19L); (mk_real_int64 2L); (mk_real_int64 59L); (mk_real_int64 31L); (mk_real_int64 6L); (mk_real_int64 20L); (mk_real_int64 32L); ]);\r
("y2_def_neg", [5; 8; 15; 16; 20; 24; 26; 30; 36; 40; 45; 47; 48; 49; 56; 66; 69; ], [(mk_real_int64 71L); (mk_real_int64 108L); (mk_real_int64 144L); (mk_real_int64 106L); (mk_real_int64 68L); (mk_real_int64 192L); (mk_real_int64 61L); (mk_real_int64 71L); (mk_real_int64 194L); (mk_real_int64 192L); (mk_real_int64 28L); (mk_real_int64 114L); (mk_real_int64 28L); (mk_real_int64 26L); (mk_real_int64 142L); (mk_real_int64 86L); (mk_real_int64 124L); ]);\r
("y3_def", [1; 7; 9; 10; 13; 14; 17; 18; 19; 22; 23; 25; 33; 35; 37; 38; 39; 42; 46; 53; 57; 58; 62; 63; 64; ], [(mk_real_int64 49L); (mk_real_int64 47L); (mk_real_int64 57L); (mk_real_int64 31L); (mk_real_int64 2L); (mk_real_int64 59L); (mk_real_int64 113L); (mk_real_int64 20L); (mk_real_int64 55L); (mk_real_int64 119L); (mk_real_int64 64L); (mk_real_int64 57L); (mk_real_int64 49L); (mk_real_int64 57L); (mk_real_int64 123L); (mk_real_int64 119L); (mk_real_int64 64L); (mk_real_int64 2L); (mk_real_int64 19L); (mk_real_int64 2L); (mk_real_int64 59L); (mk_real_int64 31L); (mk_real_int64 6L); (mk_real_int64 20L); (mk_real_int64 32L); ]);\r
("y3_def_neg", [5; 8; 15; 16; 20; 24; 26; 30; 36; 40; 45; 47; 48; 49; 56; 66; 69; ], [(mk_real_int64 71L); (mk_real_int64 108L); (mk_real_int64 144L); (mk_real_int64 106L); (mk_real_int64 68L); (mk_real_int64 192L); (mk_real_int64 61L); (mk_real_int64 71L); (mk_real_int64 194L); (mk_real_int64 192L); (mk_real_int64 28L); (mk_real_int64 114L); (mk_real_int64 28L); (mk_real_int64 26L); (mk_real_int64 142L); (mk_real_int64 86L); (mk_real_int64 124L); ]);\r
("y4_def_neg", [1; 3; 4; 5; 6; 9; 10; 11; 12; 13; 14; 15; 16; 18; 19; 20; 21; 22; 26; 27; 28; 29; 30; 31; 32; 34; 35; 37; 40; 41; 42; 46; 47; 48; 53; ], [(mk_real_int64 49L); (mk_real_int64 89L); (mk_real_int64 75L); (mk_real_int64 108L); (mk_real_int64 121L); (mk_real_int64 4L); (mk_real_int64 111L); (mk_real_int64 100L); (mk_real_int64 74L); (mk_real_int64 212L); (mk_real_int64 37L); (mk_real_int64 103L); (mk_real_int64 279L); (mk_real_int64 223L); (mk_real_int64 120L); (mk_real_int64 136L); (mk_real_int64 108L); (mk_real_int64 164L); (mk_real_int64 49L); (mk_real_int64 108L); (mk_real_int64 135L); (mk_real_int64 138L); (mk_real_int64 223L); (mk_real_int64 120L); (mk_real_int64 136L); (mk_real_int64 35L); (mk_real_int64 79L); (mk_real_int64 101L); (mk_real_int64 103L); (mk_real_int64 111L); (mk_real_int64 121L); (mk_real_int64 286L); (mk_real_int64 37L); (mk_real_int64 61L); (mk_real_int64 54L); ]);\r
("y4_def", [33; 36; 50; ], [(mk_real_int64 61L); (mk_real_int64 145L); (mk_real_int64 105L); ]);\r
("y5_def", [1; 7; 9; 10; 13; 14; 17; 18; 19; 22; 23; 25; 33; 35; 37; 38; 39; 42; 45; 46; 53; 57; 58; 62; 63; 64; ], [(mk_real_int64 49L); (mk_real_int64 47L); (mk_real_int64 57L); (mk_real_int64 39L); (mk_real_int64 2L); (mk_real_int64 59L); (mk_real_int64 113L); (mk_real_int64 20L); (mk_real_int64 55L); (mk_real_int64 119L); (mk_real_int64 64L); (mk_real_int64 57L); (mk_real_int64 49L); (mk_real_int64 57L); (mk_real_int64 19L); (mk_real_int64 119L); (mk_real_int64 64L); (mk_real_int64 2L); (mk_real_int64 61L); (mk_real_int64 19L); (mk_real_int64 2L); (mk_real_int64 59L); (mk_real_int64 39L); (mk_real_int64 39L); (mk_real_int64 20L); (mk_real_int64 32L); ]);\r
("y5_def_neg", [5; 8; 15; 16; 20; 24; 26; 30; 36; 40; 47; 48; 49; 56; 66; ], [(mk_real_int64 49L); (mk_real_int64 75L); (mk_real_int64 100L); (mk_real_int64 74L); (mk_real_int64 113L); (mk_real_int64 136L); (mk_real_int64 28L); (mk_real_int64 49L); (mk_real_int64 135L); (mk_real_int64 136L); (mk_real_int64 79L); (mk_real_int64 28L); (mk_real_int64 8L); (mk_real_int64 98L); (mk_real_int64 69L); ]);\r
("y6_def", [1; 4; 7; 9; 10; 11; 13; 14; 17; 18; 19; 22; 23; 25; 27; 28; 33; 35; 37; 38; 39; 42; 45; 46; 49; 50; 53; 55; 57; 58; 59; 61; 62; 63; 64; 65; 67; 69; ], [(mk_real_int64 49L); (mk_real_int64 49L); (mk_real_int64 47L); (mk_real_int64 57L); (mk_real_int64 106L); (mk_real_int64 121L); (mk_real_int64 2L); (mk_real_int64 59L); (mk_real_int64 113L); (mk_real_int64 20L); (mk_real_int64 55L); (mk_real_int64 296L); (mk_real_int64 64L); (mk_real_int64 323L); (mk_real_int64 68L); (mk_real_int64 185L); (mk_real_int64 49L); (mk_real_int64 57L); (mk_real_int64 19L); (mk_real_int64 119L); (mk_real_int64 330L); (mk_real_int64 2L); (mk_real_int64 61L); (mk_real_int64 19L); (mk_real_int64 122L); (mk_real_int64 129L); (mk_real_int64 2L); (mk_real_int64 207L); (mk_real_int64 59L); (mk_real_int64 39L); (mk_real_int64 121L); (mk_real_int64 42L); (mk_real_int64 39L); (mk_real_int64 20L); (mk_real_int64 162L); (mk_real_int64 129L); (mk_real_int64 107L); (mk_real_int64 36L); ]);\r
("y6_def_neg", [5; 8; 15; 16; 20; 26; 36; 47; 48; 56; 66; ], [(mk_real_int64 49L); (mk_real_int64 75L); (mk_real_int64 100L); (mk_real_int64 31L); (mk_real_int64 113L); (mk_real_int64 28L); (mk_real_int64 135L); (mk_real_int64 79L); (mk_real_int64 28L); (mk_real_int64 98L); (mk_real_int64 69L); ]);\r
("RHA", [1; 2; 6; 7; 12; 26; 29; 33; 34; 46; 50; 60; 65; 69; ], [(mk_real_int64 152L); (mk_real_int64 152L); (mk_real_int64 152L); (mk_real_int64 23L); (mk_real_int64 152L); (mk_real_int64 23L); (mk_real_int64 152L); (mk_real_int64 152L); (mk_real_int64 152L); (mk_real_int64 37L); (mk_real_int64 88L); (mk_real_int64 152L); (mk_real_int64 88L); (mk_real_int64 37L); ]);\r
("RHB", [44; 51; ], [(mk_real_int64 88L); (mk_real_int64 88L); ]);\r
("ineq105", [1; 6; 9; 14; ], [(mk_real_int64 123L); (mk_real_int64 123L); (mk_real_int64 5L); (mk_real_int64 5L); ]);\r
("ineq106", [3; 5; 6; 21; 22; 34; 37; 42; 48; 53; ], [(mk_real_int64 129L); (mk_real_int64 152L); (mk_real_int64 152L); (mk_real_int64 152L); (mk_real_int64 129L); (mk_real_int64 51L); (mk_real_int64 88L); (mk_real_int64 152L); (mk_real_int64 88L); (mk_real_int64 51L); ]);\r
("ineq107", [36; 50; ], [(mk_real_int64 187L); (mk_real_int64 187L); ]);\r
("ineq108", [5; 9; 10; 13; 14; 15; 16; 18; 19; 21; 27; 29; 30; 31; 40; 41; 46; 47; ], [(mk_real_int64 5L); (mk_real_int64 5L); (mk_real_int64 162L); (mk_real_int64 310L); (mk_real_int64 54L); (mk_real_int64 150L); (mk_real_int64 158L); (mk_real_int64 326L); (mk_real_int64 176L); (mk_real_int64 5L); (mk_real_int64 158L); (mk_real_int64 150L); (mk_real_int64 326L); (mk_real_int64 176L); (mk_real_int64 5L); (mk_real_int64 162L); (mk_real_int64 310L); (mk_real_int64 54L); ]);\r
("ineq109", [33; 53; ], [(mk_real_int64 187L); (mk_real_int64 187L); ]);\r
("ineq110", [16; 20; 29; 32; ], [(mk_real_int64 181L); (mk_real_int64 5L); (mk_real_int64 181L); (mk_real_int64 5L); ]);\r
("ineq111", [1; 4; 6; 11; 12; 16; 20; 22; 26; 28; 32; 35; 37; 40; 42; 46; 50; 53; ], [(mk_real_int64 394L); (mk_real_int64 601L); (mk_real_int64 134L); (mk_real_int64 798L); (mk_real_int64 591L); (mk_real_int64 1080L); (mk_real_int64 1080L); (mk_real_int64 601L); (mk_real_int64 394L); (mk_real_int64 1080L); (mk_real_int64 1080L); (mk_real_int64 633L); (mk_real_int64 321L); (mk_real_int64 798L); (mk_real_int64 134L); (mk_real_int64 591L); (mk_real_int64 321L); (mk_real_int64 633L); ]);\r
("ineq114", [2; 3; 6; 8; 10; 13; 14; 22; 25; 34; 38; 41; 42; 44; 46; 47; 49; 53; ], [(mk_real_int64 533L); (mk_real_int64 326L); (mk_real_int64 8L); (mk_real_int64 785L); (mk_real_int64 282L); (mk_real_int64 47L); (mk_real_int64 443L); (mk_real_int64 326L); (mk_real_int64 533L); (mk_real_int64 359L); (mk_real_int64 670L); (mk_real_int64 282L); (mk_real_int64 8L); (mk_real_int64 785L); (mk_real_int64 47L); (mk_real_int64 443L); (mk_real_int64 670L); (mk_real_int64 359L); ]);\r
("ineq119", [11; 12; ], [(mk_real_int64 643L); (mk_real_int64 643L); ]);\r
("ineq120", [1; 2; 6; 7; 8; 13; ], [(mk_real_int64 279L); (mk_real_int64 649L); (mk_real_int64 279L); (mk_real_int64 649L); (mk_real_int64 437L); (mk_real_int64 437L); ]);\r
];;\r
\r
(***************)\r
(* Variables   *)\r
(***************)\r
let target_variables = [\r
("ln_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 3275L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3275L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3275L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 2750L); (mk_real_int64 2750L); (mk_real_int64 3625L); ]);\r
];;\r
\r
(*************************)\r
\r
let variable_bounds = [\r
("azim_hi", [1; 2; 6; 7; 10; 12; 17; 18; 26; 29; 33; 34; 41; 46; 50; 52; 58; 60; 62; 63; 65; 69; ], [(mk_real_int64 1482L); (mk_real_int64 942L); (mk_real_int64 658L); (mk_real_int64 76L); (mk_real_int64 8L); (mk_real_int64 410L); (mk_real_int64 422L); (mk_real_int64 318L); (mk_real_int64 76L); (mk_real_int64 658L); (mk_real_int64 1482L); (mk_real_int64 942L); (mk_real_int64 246L); (mk_real_int64 734L); (mk_real_int64 420L); (mk_real_int64 246L); (mk_real_int64 8L); (mk_real_int64 410L); (mk_real_int64 422L); (mk_real_int64 318L); (mk_real_int64 420L); (mk_real_int64 734L); ]);\r
("azim_lo", [14; 44; 51; 57; ], [(mk_real_int64 468L); (mk_real_int64 791L); (mk_real_int64 791L); (mk_real_int64 468L); ]);\r
("rhazim_lo", [1; 2; 6; 7; 9; 10; 12; 25; 26; 29; 33; 34; 46; 49; 50; 58; 60; 64; 65; 69; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("rhazim_hi", [44; 51; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("rho_lo", [0; 3; 9; 12; 13; ], [(mk_real_int64 1732L); (mk_real_int64 1732L); (mk_real_int64 1732L); (mk_real_int64 2556L); (mk_real_int64 2556L); ]);\r
("rho_hi", [1; 2; 4; 5; 6; 7; 8; 10; 11; 14; ], [(mk_real_int64 1720L); (mk_real_int64 1720L); (mk_real_int64 1720L); (mk_real_int64 1720L); (mk_real_int64 1720L); (mk_real_int64 1720L); (mk_real_int64 1720L); (mk_real_int64 1720L); (mk_real_int64 1720L); (mk_real_int64 1720L); ]);\r
("tau_hi", [0; 5; 10; 14; 19; 21; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("y1_hi", [1; 5; 7; 9; 10; 15; 17; 18; 20; 22; 25; 26; 30; 33; 38; 42; 46; 47; 49; 53; 56; 58; 63; 64; 69; ], [(mk_real_int64 255L); (mk_real_int64 80L); (mk_real_int64 600L); (mk_real_int64 625L); (mk_real_int64 680L); (mk_real_int64 360L); (mk_real_int64 150L); (mk_real_int64 310L); (mk_real_int64 250L); (mk_real_int64 390L); (mk_real_int64 625L); (mk_real_int64 420L); (mk_real_int64 80L); (mk_real_int64 255L); (mk_real_int64 390L); (mk_real_int64 425L); (mk_real_int64 400L); (mk_real_int64 60L); (mk_real_int64 420L); (mk_real_int64 425L); (mk_real_int64 185L); (mk_real_int64 680L); (mk_real_int64 310L); (mk_real_int64 200L); (mk_real_int64 223L); ]);\r
("y1_lo", [8; 13; 14; 16; 19; 23; 24; 35; 36; 37; 39; 40; 45; 48; 57; 62; 66; ], [(mk_real_int64 180L); (mk_real_int64 175L); (mk_real_int64 70L); (mk_real_int64 380L); (mk_real_int64 250L); (mk_real_int64 360L); (mk_real_int64 500L); (mk_real_int64 130L); (mk_real_int64 400L); (mk_real_int64 470L); (mk_real_int64 360L); (mk_real_int64 500L); (mk_real_int64 237L); (mk_real_int64 500L); (mk_real_int64 70L); (mk_real_int64 230L); (mk_real_int64 280L); ]);\r
("y2_hi", [1; 5; 9; 10; 15; 23; 25; 30; 33; 35; 37; 39; 42; 47; 49; 53; 56; 58; 62; 64; 69; ], [(mk_real_int64 446L); (mk_real_int64 80L); (mk_real_int64 148L); (mk_real_int64 208L); (mk_real_int64 360L); (mk_real_int64 64L); (mk_real_int64 148L); (mk_real_int64 80L); (mk_real_int64 446L); (mk_real_int64 512L); (mk_real_int64 380L); (mk_real_int64 64L); (mk_real_int64 10L); (mk_real_int64 60L); (mk_real_int64 252L); (mk_real_int64 10L); (mk_real_int64 180L); (mk_real_int64 208L); (mk_real_int64 460L); (mk_real_int64 32L); (mk_real_int64 387L); ]);\r
("y2_lo", [7; 8; 13; 14; 16; 17; 18; 19; 20; 22; 24; 26; 36; 38; 40; 45; 46; 48; 57; 63; 66; ], [(mk_real_int64 44L); (mk_real_int64 180L); (mk_real_int64 180L); (mk_real_int64 32L); (mk_real_int64 380L); (mk_real_int64 160L); (mk_real_int64 344L); (mk_real_int64 400L); (mk_real_int64 108L); (mk_real_int64 336L); (mk_real_int64 500L); (mk_real_int64 224L); (mk_real_int64 400L); (mk_real_int64 336L); (mk_real_int64 500L); (mk_real_int64 237L); (mk_real_int64 436L); (mk_real_int64 424L); (mk_real_int64 32L); (mk_real_int64 344L); (mk_real_int64 204L); ]);\r
("y3_hi", [1; 5; 9; 10; 15; 23; 25; 30; 33; 35; 37; 39; 42; 47; 49; 53; 56; 58; 62; 64; 69; ], [(mk_real_int64 446L); (mk_real_int64 80L); (mk_real_int64 148L); (mk_real_int64 208L); (mk_real_int64 360L); (mk_real_int64 64L); (mk_real_int64 148L); (mk_real_int64 80L); (mk_real_int64 446L); (mk_real_int64 512L); (mk_real_int64 380L); (mk_real_int64 64L); (mk_real_int64 10L); (mk_real_int64 60L); (mk_real_int64 252L); (mk_real_int64 10L); (mk_real_int64 180L); (mk_real_int64 208L); (mk_real_int64 460L); (mk_real_int64 32L); (mk_real_int64 387L); ]);\r
("y3_lo", [7; 8; 13; 14; 16; 17; 18; 19; 20; 22; 24; 26; 36; 38; 40; 45; 46; 48; 57; 63; 66; ], [(mk_real_int64 44L); (mk_real_int64 180L); (mk_real_int64 180L); (mk_real_int64 32L); (mk_real_int64 380L); (mk_real_int64 160L); (mk_real_int64 344L); (mk_real_int64 400L); (mk_real_int64 108L); (mk_real_int64 336L); (mk_real_int64 500L); (mk_real_int64 224L); (mk_real_int64 400L); (mk_real_int64 336L); (mk_real_int64 500L); (mk_real_int64 237L); (mk_real_int64 436L); (mk_real_int64 424L); (mk_real_int64 32L); (mk_real_int64 344L); (mk_real_int64 204L); ]);\r
("y4_lo", [1; 4; 13; 18; 19; 26; 27; 29; 30; 31; 33; 35; 36; 40; 46; 50; ], [(mk_real_int64 250L); (mk_real_int64 125L); (mk_real_int64 350L); (mk_real_int64 310L); (mk_real_int64 560L); (mk_real_int64 250L); (mk_real_int64 230L); (mk_real_int64 226L); (mk_real_int64 310L); (mk_real_int64 560L); (mk_real_int64 412L); (mk_real_int64 125L); (mk_real_int64 449L); (mk_real_int64 175L); (mk_real_int64 225L); (mk_real_int64 574L); ]);\r
("y4_hi", [3; 5; 6; 9; 10; 11; 12; 14; 15; 16; 20; 21; 22; 32; 34; 37; 41; 42; 47; 48; 53; ], [(mk_real_int64 635L); (mk_real_int64 455L); (mk_real_int64 130L); (mk_real_int64 575L); (mk_real_int64 30L); (mk_real_int64 250L); (mk_real_int64 125L); (mk_real_int64 10L); (mk_real_int64 250L); (mk_real_int64 294L); (mk_real_int64 20L); (mk_real_int64 455L); (mk_real_int64 510L); (mk_real_int64 20L); (mk_real_int64 65L); (mk_real_int64 595L); (mk_real_int64 30L); (mk_real_int64 130L); (mk_real_int64 10L); (mk_real_int64 720L); (mk_real_int64 528L); ]);\r
("y5_lo", [5; 7; 8; 10; 13; 14; 17; 18; 19; 22; 26; 30; 38; 45; 46; 47; 48; 49; 57; 58; 62; 63; ], [(mk_real_int64 250L); (mk_real_int64 44L); (mk_real_int64 125L); (mk_real_int64 422L); (mk_real_int64 180L); (mk_real_int64 32L); (mk_real_int64 160L); (mk_real_int64 344L); (mk_real_int64 400L); (mk_real_int64 336L); (mk_real_int64 169L); (mk_real_int64 250L); (mk_real_int64 336L); (mk_real_int64 412L); (mk_real_int64 436L); (mk_real_int64 125L); (mk_real_int64 424L); (mk_real_int64 93L); (mk_real_int64 32L); (mk_real_int64 422L); (mk_real_int64 35L); (mk_real_int64 344L); ]);\r
("y5_hi", [1; 9; 15; 16; 20; 23; 24; 25; 33; 35; 37; 39; 40; 42; 53; 56; 64; 66; 69; ], [(mk_real_int64 446L); (mk_real_int64 148L); (mk_real_int64 250L); (mk_real_int64 125L); (mk_real_int64 36L); (mk_real_int64 64L); (mk_real_int64 20L); (mk_real_int64 148L); (mk_real_int64 446L); (mk_real_int64 512L); (mk_real_int64 124L); (mk_real_int64 64L); (mk_real_int64 20L); (mk_real_int64 10L); (mk_real_int64 10L); (mk_real_int64 70L); (mk_real_int64 32L); (mk_real_int64 451L); (mk_real_int64 27L); ]);\r
("y6_lo", [4; 5; 7; 8; 10; 11; 13; 14; 16; 17; 18; 19; 22; 24; 25; 26; 27; 28; 30; 38; 39; 40; 45; 46; 47; 48; 49; 50; 55; 57; 58; 59; 61; 62; 63; 64; 65; 67; 69; ], [(mk_real_int64 49000L); (mk_real_int64 250L); (mk_real_int64 44L); (mk_real_int64 125L); (mk_real_int64 68000L); (mk_real_int64 121000L); (mk_real_int64 180L); (mk_real_int64 32L); (mk_real_int64 42875L); (mk_real_int64 160L); (mk_real_int64 344L); (mk_real_int64 400L); (mk_real_int64 177336L); (mk_real_int64 136000L); (mk_real_int64 266000L); (mk_real_int64 169L); (mk_real_int64 68000L); (mk_real_int64 185000L); (mk_real_int64 49250L); (mk_real_int64 336L); (mk_real_int64 266000L); (mk_real_int64 136000L); (mk_real_int64 412L); (mk_real_int64 436L); (mk_real_int64 125L); (mk_real_int64 424L); (mk_real_int64 130093L); (mk_real_int64 129000L); (mk_real_int64 207000L); (mk_real_int64 32L); (mk_real_int64 422L); (mk_real_int64 121000L); (mk_real_int64 42000L); (mk_real_int64 35L); (mk_real_int64 344L); (mk_real_int64 130000L); (mk_real_int64 129000L); (mk_real_int64 107000L); (mk_real_int64 36000L); ]);\r
("y6_hi", [1; 9; 10; 15; 20; 23; 24; 25; 33; 35; 37; 39; 40; 42; 53; 56; 64; 66; 69; ], [(mk_real_int64 446L); (mk_real_int64 148L); (mk_real_int64 578L); (mk_real_int64 250L); (mk_real_int64 36L); (mk_real_int64 64L); (mk_real_int64 20L); (mk_real_int64 148L); (mk_real_int64 446L); (mk_real_int64 512L); (mk_real_int64 124L); (mk_real_int64 64L); (mk_real_int64 20L); (mk_real_int64 10L); (mk_real_int64 10L); (mk_real_int64 70L); (mk_real_int64 32L); (mk_real_int64 451L); (mk_real_int64 27L); ]);\r
("ye_lo", [1; 5; 8; 14; 15; 33; 36; 46; 65; 66; 67; ], [(mk_real_int64 167000L); (mk_real_int64 185000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 207000L); (mk_real_int64 167000L); (mk_real_int64 177000L); (mk_real_int64 36000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("ye_hi", [16; 19; 24; 40; 45; 46; 47; 49; 64; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("yn_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 14; ], [(mk_real_int64 252L); (mk_real_int64 484L); (mk_real_int64 1484L); (mk_real_int64 252L); (mk_real_int64 484L); (mk_real_int64 484L); (mk_real_int64 1484L); (mk_real_int64 1484L); (mk_real_int64 484L); (mk_real_int64 252L); (mk_real_int64 484L); (mk_real_int64 484L); (mk_real_int64 484L); ]);\r
("yn_lo", [12; 13; ], [(mk_real_int64 68L); (mk_real_int64 68L); ]);\r
];;\r
let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
end;;\r
\r
concl (Test_case.result)\r