Update from HH

[Flyspeck/.git] / formal_lp / old / ineqs / tests / 241242841715_out.hl

needs "nobranching_lp.hl";;
\r
module Test_case = struct\r
let hypermap_string = "241242841715 21 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 3 9 3 10 3 10 3 2 3 10 2 11 3 11 2 12 3 12 2 1 3 12 1 0 3 12 0 13 3 13 0 7 3 13 7 14 4 14 7 6 9 3 6 8 9 3 14 9 10 3 14 10 11 3 11 12 13 3 13 14 11 ";;\r
let precision = 3;;\r
(***************)\r
(* Constraints *)\r
(***************)\r
let constraints = [\r
("azim_sum_neg", [1; 4; 8; 10; 11; 12; 14; ], [(mk_real_int64 207L); (mk_real_int64 356L); (mk_real_int64 102L); (mk_real_int64 90L); (mk_real_int64 210L); (mk_real_int64 77L); (mk_real_int64 67L); ]);\r
("azim_sum", [6; 7; 9; 13; ], [(mk_real_int64 120L); (mk_real_int64 22L); (mk_real_int64 43L); (mk_real_int64 380L); ]);\r
("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 1131L); (mk_real_int64 825L); (mk_real_int64 1131L); (mk_real_int64 1131L); (mk_real_int64 861L); (mk_real_int64 1131L); (mk_real_int64 1029L); (mk_real_int64 1112L); (mk_real_int64 1042L); (mk_real_int64 1131L); (mk_real_int64 1109L); (mk_real_int64 903L); (mk_real_int64 1121L); (mk_real_int64 1131L); (mk_real_int64 1019L); ]);\r
("sol_sum3", [2; 3; 8; 9; 16; ], [(mk_real_int64 83L); (mk_real_int64 31L); (mk_real_int64 139L); (mk_real_int64 139L); (mk_real_int64 160L); ]);\r
("sol_sum3_neg", [14; 17; ], [(mk_real_int64 46L); (mk_real_int64 55L); ]);\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 1042L); (mk_real_int64 825L); (mk_real_int64 825L); (mk_real_int64 1042L); (mk_real_int64 1081L); (mk_real_int64 1109L); (mk_real_int64 1019L); (mk_real_int64 709L); (mk_real_int64 832L); (mk_real_int64 832L); (mk_real_int64 903L); (mk_real_int64 1044L); (mk_real_int64 1044L); (mk_real_int64 940L); (mk_real_int64 1089L); (mk_real_int64 1019L); (mk_real_int64 903L); (mk_real_int64 975L); ]);\r
("tau_sum4_neg", [0; 1; ], [(mk_real_int64 1131L); (mk_real_int64 1131L); ]);\r
("tau_sum6_neg", [0; ], [(mk_real_int64 1131L); ]);\r
("ln_def_neg", [0; 2; 3; 5; 6; 7; 8; 9; 10; 12; 13; 14; ], [(mk_real_int64 247L); (mk_real_int64 247L); (mk_real_int64 247L); (mk_real_int64 247L); (mk_real_int64 134L); (mk_real_int64 226L); (mk_real_int64 149L); (mk_real_int64 247L); (mk_real_int64 223L); (mk_real_int64 236L); (mk_real_int64 247L); (mk_real_int64 124L); ]);\r
("ln_def", [1; 4; 11; ], [(mk_real_int64 91L); (mk_real_int64 51L); (mk_real_int64 5L); ]);\r
("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 7105L); (mk_real_int64 5181L); (mk_real_int64 7105L); (mk_real_int64 7105L); (mk_real_int64 5408L); (mk_real_int64 7105L); (mk_real_int64 6463L); (mk_real_int64 6988L); (mk_real_int64 6549L); (mk_real_int64 7105L); (mk_real_int64 6967L); (mk_real_int64 5672L); (mk_real_int64 7041L); (mk_real_int64 7105L); (mk_real_int64 6403L); ]);\r
("edge_sym_neg", [11; 12; 15; 21; 23; 24; 29; 32; 42; 45; 48; 58; 61; ], [(mk_real_int64 191L); (mk_real_int64 95L); (mk_real_int64 321L); (mk_real_int64 60L); (mk_real_int64 198L); (mk_real_int64 100L); (mk_real_int64 97L); (mk_real_int64 173L); (mk_real_int64 169L); (mk_real_int64 153L); (mk_real_int64 107L); (mk_real_int64 41L); (mk_real_int64 21L); ]);\r
("edge_sym", [18; 20; 27; 30; 33; 39; 41; 64; ], [(mk_real_int64 148L); (mk_real_int64 6L); (mk_real_int64 35L); (mk_real_int64 138L); (mk_real_int64 81L); (mk_real_int64 173L); (mk_real_int64 169L); (mk_real_int64 101L); ]);\r
("y1_def_neg", [10; 12; 14; 15; 16; 18; 19; 20; 21; 22; 23; 25; 27; 29; 31; 32; 34; 41; 42; 43; 44; 45; 47; 53; 55; 57; 59; 61; 64; 65; 66; ], [(mk_real_int64 47L); (mk_real_int64 111L); (mk_real_int64 184L); (mk_real_int64 12L); (mk_real_int64 43L); (mk_real_int64 13L); (mk_real_int64 96L); (mk_real_int64 5L); (mk_real_int64 53L); (mk_real_int64 40L); (mk_real_int64 180L); (mk_real_int64 148L); (mk_real_int64 13L); (mk_real_int64 250L); (mk_real_int64 146L); (mk_real_int64 7L); (mk_real_int64 24L); (mk_real_int64 82L); (mk_real_int64 221L); (mk_real_int64 188L); (mk_real_int64 52L); (mk_real_int64 24L); (mk_real_int64 78L); (mk_real_int64 109L); (mk_real_int64 102L); (mk_real_int64 31L); (mk_real_int64 67L); (mk_real_int64 41L); (mk_real_int64 83L); (mk_real_int64 184L); (mk_real_int64 170L); ]);\r
("y1_def", [17; 24; 30; 33; 36; 38; 40; 56; 63; 67; ], [(mk_real_int64 62L); (mk_real_int64 31L); (mk_real_int64 33L); (mk_real_int64 8L); (mk_real_int64 73L); (mk_real_int64 49L); (mk_real_int64 105L); (mk_real_int64 18L); (mk_real_int64 1L); (mk_real_int64 60L); ]);\r
("y2_def_neg", [12; 15; 17; 18; 19; 20; 23; 24; 25; 29; 30; 32; 33; 34; 36; 38; 40; 42; 43; 47; 55; 61; 63; 64; 65; ], [(mk_real_int64 178L); (mk_real_int64 147L); (mk_real_int64 19L); (mk_real_int64 13L); (mk_real_int64 143L); (mk_real_int64 5L); (mk_real_int64 180L); (mk_real_int64 9L); (mk_real_int64 207L); (mk_real_int64 143L); (mk_real_int64 10L); (mk_real_int64 7L); (mk_real_int64 3L); (mk_real_int64 24L); (mk_real_int64 50L); (mk_real_int64 73L); (mk_real_int64 32L); (mk_real_int64 85L); (mk_real_int64 188L); (mk_real_int64 16L); (mk_real_int64 102L); (mk_real_int64 84L); (mk_real_int64 32L); (mk_real_int64 6L); (mk_real_int64 171L); ]);\r
("y2_def", [10; 14; 16; 21; 22; 27; 31; 41; 44; 45; 53; 56; 57; 59; 66; 67; ], [(mk_real_int64 33L); (mk_real_int64 111L); (mk_real_int64 26L); (mk_real_int64 32L); (mk_real_int64 34L); (mk_real_int64 8L); (mk_real_int64 88L); (mk_real_int64 50L); (mk_real_int64 32L); (mk_real_int64 37L); (mk_real_int64 71L); (mk_real_int64 18L); (mk_real_int64 7L); (mk_real_int64 41L); (mk_real_int64 175L); (mk_real_int64 9L); ]);\r
("y3_def_neg", [12; 15; 17; 18; 19; 20; 23; 24; 25; 29; 30; 32; 33; 34; 36; 38; 40; 42; 43; 47; 55; 61; 63; 64; 65; ], [(mk_real_int64 178L); (mk_real_int64 147L); (mk_real_int64 19L); (mk_real_int64 13L); (mk_real_int64 143L); (mk_real_int64 5L); (mk_real_int64 180L); (mk_real_int64 9L); (mk_real_int64 207L); (mk_real_int64 143L); (mk_real_int64 10L); (mk_real_int64 7L); (mk_real_int64 3L); (mk_real_int64 24L); (mk_real_int64 50L); (mk_real_int64 73L); (mk_real_int64 32L); (mk_real_int64 85L); (mk_real_int64 188L); (mk_real_int64 16L); (mk_real_int64 102L); (mk_real_int64 84L); (mk_real_int64 32L); (mk_real_int64 6L); (mk_real_int64 171L); ]);\r
("y3_def", [10; 14; 16; 21; 22; 27; 31; 41; 44; 45; 53; 56; 57; 59; 66; 67; ], [(mk_real_int64 33L); (mk_real_int64 111L); (mk_real_int64 26L); (mk_real_int64 32L); (mk_real_int64 34L); (mk_real_int64 8L); (mk_real_int64 88L); (mk_real_int64 50L); (mk_real_int64 32L); (mk_real_int64 37L); (mk_real_int64 71L); (mk_real_int64 18L); (mk_real_int64 7L); (mk_real_int64 41L); (mk_real_int64 175L); (mk_real_int64 9L); ]);\r
("y4_def_neg", [0; 2; 4; 6; 9; 11; 12; 13; 15; 17; 19; 21; 22; 24; 31; 32; 33; 34; 35; 37; 39; 41; 42; 43; 45; 50; 51; 52; ], [(mk_real_int64 63L); (mk_real_int64 33L); (mk_real_int64 210L); (mk_real_int64 49L); (mk_real_int64 36L); (mk_real_int64 61L); (mk_real_int64 64L); (mk_real_int64 125L); (mk_real_int64 65L); (mk_real_int64 15L); (mk_real_int64 204L); (mk_real_int64 166L); (mk_real_int64 5L); (mk_real_int64 16L); (mk_real_int64 93L); (mk_real_int64 191L); (mk_real_int64 130L); (mk_real_int64 60L); (mk_real_int64 70L); (mk_real_int64 107L); (mk_real_int64 133L); (mk_real_int64 71L); (mk_real_int64 9L); (mk_real_int64 32L); (mk_real_int64 77L); (mk_real_int64 125L); (mk_real_int64 131L); (mk_real_int64 329L); ]);\r
("y4_def", [5; 7; 8; 10; 14; 20; 23; 26; 28; 30; 49; 53; ], [(mk_real_int64 80L); (mk_real_int64 95L); (mk_real_int64 27L); (mk_real_int64 10L); (mk_real_int64 48L); (mk_real_int64 52L); (mk_real_int64 13L); (mk_real_int64 190L); (mk_real_int64 173L); (mk_real_int64 162L); (mk_real_int64 91L); (mk_real_int64 49L); ]);\r
("y5_def_neg", [12; 15; 17; 19; 23; 24; 25; 29; 30; 32; 33; 34; 40; 42; 43; 55; 56; 61; 65; 67; ], [(mk_real_int64 128L); (mk_real_int64 111L); (mk_real_int64 19L); (mk_real_int64 103L); (mk_real_int64 125L); (mk_real_int64 9L); (mk_real_int64 148L); (mk_real_int64 87L); (mk_real_int64 10L); (mk_real_int64 5L); (mk_real_int64 3L); (mk_real_int64 16L); (mk_real_int64 32L); (mk_real_int64 43L); (mk_real_int64 130L); (mk_real_int64 71L); (mk_real_int64 9L); (mk_real_int64 62L); (mk_real_int64 117L); (mk_real_int64 23L); ]);\r
("y5_def", [10; 14; 16; 18; 20; 21; 22; 27; 31; 36; 41; 44; 45; 53; 57; 59; 63; 64; 66; ], [(mk_real_int64 33L); (mk_real_int64 111L); (mk_real_int64 26L); (mk_real_int64 27L); (mk_real_int64 10L); (mk_real_int64 32L); (mk_real_int64 34L); (mk_real_int64 8L); (mk_real_int64 88L); (mk_real_int64 16L); (mk_real_int64 50L); (mk_real_int64 32L); (mk_real_int64 37L); (mk_real_int64 71L); (mk_real_int64 9L); (mk_real_int64 41L); (mk_real_int64 44L); (mk_real_int64 10L); (mk_real_int64 175L); ]);\r
("y6_def_neg", [12; 15; 19; 23; 24; 29; 30; 32; 33; 34; 40; 42; 43; 55; 56; 61; 65; ], [(mk_real_int64 128L); (mk_real_int64 111L); (mk_real_int64 98L); (mk_real_int64 125L); (mk_real_int64 9L); (mk_real_int64 87L); (mk_real_int64 10L); (mk_real_int64 5L); (mk_real_int64 3L); (mk_real_int64 16L); (mk_real_int64 32L); (mk_real_int64 43L); (mk_real_int64 130L); (mk_real_int64 71L); (mk_real_int64 9L); (mk_real_int64 62L); (mk_real_int64 117L); ]);\r
("y6_def", [10; 14; 16; 17; 18; 20; 21; 22; 25; 26; 27; 31; 36; 41; 44; 45; 46; 53; 54; 57; 59; 63; 64; 66; 67; ], [(mk_real_int64 33L); (mk_real_int64 111L); (mk_real_int64 313L); (mk_real_int64 22L); (mk_real_int64 27L); (mk_real_int64 10L); (mk_real_int64 32L); (mk_real_int64 72L); (mk_real_int64 214L); (mk_real_int64 57L); (mk_real_int64 8L); (mk_real_int64 88L); (mk_real_int64 16L); (mk_real_int64 50L); (mk_real_int64 93L); (mk_real_int64 37L); (mk_real_int64 153L); (mk_real_int64 165L); (mk_real_int64 264L); (mk_real_int64 109L); (mk_real_int64 41L); (mk_real_int64 158L); (mk_real_int64 10L); (mk_real_int64 175L); (mk_real_int64 345L); ]);\r
("RHA", [11; 13; 16; 18; 20; 23; 24; 26; 28; 31; 32; 33; 34; 35; 36; 37; 38; 39; 41; 42; 43; 46; 48; 54; 55; 56; 57; 58; 60; 62; 64; 65; 67; ], [(mk_real_int64 89L); (mk_real_int64 218L); (mk_real_int64 146L); (mk_real_int64 306L); (mk_real_int64 89L); (mk_real_int64 50L); (mk_real_int64 28L); (mk_real_int64 22L); (mk_real_int64 90L); (mk_real_int64 67L); (mk_real_int64 421L); (mk_real_int64 193L); (mk_real_int64 71L); (mk_real_int64 299L); (mk_real_int64 29L); (mk_real_int64 71L); (mk_real_int64 29L); (mk_real_int64 299L); (mk_real_int64 92L); (mk_real_int64 77L); (mk_real_int64 77L); (mk_real_int64 77L); (mk_real_int64 87L); (mk_real_int64 102L); (mk_real_int64 191L); (mk_real_int64 42L); (mk_real_int64 3L); (mk_real_int64 20L); (mk_real_int64 90L); (mk_real_int64 116L); (mk_real_int64 218L); (mk_real_int64 132L); (mk_real_int64 44L); ]);\r
("RHB", [8; 9; 45; 47; 50; 51; ], [(mk_real_int64 19L); (mk_real_int64 102L); (mk_real_int64 15L); (mk_real_int64 15L); (mk_real_int64 102L); (mk_real_int64 19L); ]);\r
("tau4", [0; 1; ], [(mk_real_int64 1131L); (mk_real_int64 572L); ]);\r
("tau6", [0; ], [(mk_real_int64 1131L); ]);\r
("ineq106", [0; 4; 6; 11; 12; 17; 19; 21; 31; 32; 34; 39; 43; 45; 51; 52; ], [(mk_real_int64 70L); (mk_real_int64 306L); (mk_real_int64 72L); (mk_real_int64 89L); (mk_real_int64 50L); (mk_real_int64 22L); (mk_real_int64 112L); (mk_real_int64 243L); (mk_real_int64 136L); (mk_real_int64 141L); (mk_real_int64 87L); (mk_real_int64 172L); (mk_real_int64 39L); (mk_real_int64 112L); (mk_real_int64 14L); (mk_real_int64 156L); ]);\r
("ineq107", [2; 5; 7; 9; 14; 15; 20; 23; 26; 28; 30; 47; 49; 53; ], [(mk_real_int64 102L); (mk_real_int64 207L); (mk_real_int64 123L); (mk_real_int64 72L); (mk_real_int64 61L); (mk_real_int64 90L); (mk_real_int64 67L); (mk_real_int64 17L); (mk_real_int64 188L); (mk_real_int64 188L); (mk_real_int64 210L); (mk_real_int64 67L); (mk_real_int64 50L); (mk_real_int64 78L); ]);\r
("ineq108", [0; 12; 35; 37; 39; 50; 52; ], [(mk_real_int64 22L); (mk_real_int64 43L); (mk_real_int64 102L); (mk_real_int64 102L); (mk_real_int64 22L); (mk_real_int64 129L); (mk_real_int64 325L); ]);\r
("ineq109", [8; 10; 26; 28; 49; ], [(mk_real_int64 83L); (mk_real_int64 31L); (mk_real_int64 139L); (mk_real_int64 139L); (mk_real_int64 160L); ]);\r
("ineq110", [42; 53; ], [(mk_real_int64 46L); (mk_real_int64 55L); ]);\r
("ineq111", [2; 5; 9; 13; 15; 19; 22; 24; 28; 32; 33; 37; 41; 43; 47; 50; 51; ], [(mk_real_int64 901L); (mk_real_int64 640L); (mk_real_int64 733L); (mk_real_int64 1000L); (mk_real_int64 1074L); (mk_real_int64 1019L); (mk_real_int64 36L); (mk_real_int64 132L); (mk_real_int64 132L); (mk_real_int64 756L); (mk_real_int64 1044L); (mk_real_int64 298L); (mk_real_int64 566L); (mk_real_int64 41L); (mk_real_int64 412L); (mk_real_int64 294L); (mk_real_int64 975L); ]);\r
("ineq113", [44; ], [(mk_real_int64 449L); ]);\r
("ineq114", [1; 3; 6; 8; 10; 11; 13; 16; 22; 25; 29; 31; 38; 41; 42; 45; 48; 50; ], [(mk_real_int64 142L); (mk_real_int64 184L); (mk_real_int64 202L); (mk_real_int64 622L); (mk_real_int64 191L); (mk_real_int64 118L); (mk_real_int64 80L); (mk_real_int64 35L); (mk_real_int64 673L); (mk_real_int64 700L); (mk_real_int64 700L); (mk_real_int64 146L); (mk_real_int64 746L); (mk_real_int64 374L); (mk_real_int64 600L); (mk_real_int64 607L); (mk_real_int64 335L); (mk_real_int64 274L); ]);\r
("ineq120", [4; 7; ], [(mk_real_int64 502L); (mk_real_int64 57L); ]);\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 3625L); (mk_real_int64 2325L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 2600L); (mk_real_int64 3625L); (mk_real_int64 2975L); (mk_real_int64 3100L); (mk_real_int64 2925L); (mk_real_int64 3625L); (mk_real_int64 3775L); (mk_real_int64 2400L); (mk_real_int64 3825L); (mk_real_int64 3625L); (mk_real_int64 3475L); ]);\r
];;\r
\r
(*************************)\r
\r
let variable_bounds = [\r
("azim_hi", [1; 4; 8; 17; 18; 23; 24; 32; 35; 39; 49; 51; 52; 55; 62; ], [(mk_real_int64 356000L); (mk_real_int64 207000L); (mk_real_int64 344L); (mk_real_int64 1000L); (mk_real_int64 372L); (mk_real_int64 80L); (mk_real_int64 1000L); (mk_real_int64 298L); (mk_real_int64 200L); (mk_real_int64 200L); (mk_real_int64 516L); (mk_real_int64 344L); (mk_real_int64 206L); (mk_real_int64 124L); (mk_real_int64 710L); ]);\r
("azim_lo", [9; 11; 13; 16; 19; 20; 21; 26; 41; 45; 47; 48; 50; 56; 58; 59; 64; ], [(mk_real_int64 48L); (mk_real_int64 108L); (mk_real_int64 816L); (mk_real_int64 548L); (mk_real_int64 1000L); (mk_real_int64 434L); (mk_real_int64 132L); (mk_real_int64 90L); (mk_real_int64 604L); (mk_real_int64 360L); (mk_real_int64 360L); (mk_real_int64 4L); (mk_real_int64 48L); (mk_real_int64 400L); (mk_real_int64 291L); (mk_real_int64 18L); (mk_real_int64 476L); ]);\r
("rhazim_hi", [1; 4; 13; 16; ], [(mk_real_int64 270000L); (mk_real_int64 306000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("rhazim_lo", [32; 33; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("rho_hi", [0; 1; 2; 3; 4; 5; 6; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 2204L); (mk_real_int64 3300L); (mk_real_int64 2204L); (mk_real_int64 2204L); (mk_real_int64 2524L); (mk_real_int64 2204L); (mk_real_int64 3236L); (mk_real_int64 2204L); (mk_real_int64 1956L); (mk_real_int64 2452L); (mk_real_int64 3364L); (mk_real_int64 2204L); (mk_real_int64 396L); ]);\r
("rho_lo", [7; 8; ], [(mk_real_int64 192L); (mk_real_int64 1072L); ]);\r
("tau_lo", [3; 4; 6; 12; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("tau_hi", [2; 17; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("y1_hi", [14; 15; 18; 19; 20; 30; 31; 32; 33; 34; 36; 38; 41; 42; 43; 45; 47; 53; 55; 57; 61; 65; 66; ], [(mk_real_int64 400L); (mk_real_int64 300L); (mk_real_int64 467L); (mk_real_int64 60L); (mk_real_int64 319L); (mk_real_int64 500L); (mk_real_int64 200L); (mk_real_int64 520L); (mk_real_int64 500L); (mk_real_int64 240L); (mk_real_int64 11L); (mk_real_int64 251L); (mk_real_int64 400L); (mk_real_int64 320L); (mk_real_int64 80L); (mk_real_int64 30L); (mk_real_int64 390L); (mk_real_int64 630L); (mk_real_int64 120L); (mk_real_int64 220L); (mk_real_int64 340L); (mk_real_int64 100L); (mk_real_int64 25L); ]);\r
("y1_lo", [10; 12; 16; 17; 21; 22; 24; 25; 27; 29; 44; 56; 59; 63; 64; 67; ], [(mk_real_int64 170L); (mk_real_int64 180L); (mk_real_int64 200L); (mk_real_int64 500L); (mk_real_int64 400L); (mk_real_int64 105L); (mk_real_int64 500L); (mk_real_int64 320L); (mk_real_int64 200L); (mk_real_int64 620L); (mk_real_int64 200L); (mk_real_int64 520L); (mk_real_int64 200L); (mk_real_int64 160L); (mk_real_int64 235L); (mk_real_int64 100L); ]);\r
("y2_lo", [22; 24; 30; 38; 41; 44; 47; 53; 56; 57; 59; 61; ], [(mk_real_int64 148L); (mk_real_int64 272L); (mk_real_int64 184L); (mk_real_int64 325L); (mk_real_int64 496L); (mk_real_int64 332L); (mk_real_int64 512L); (mk_real_int64 384L); (mk_real_int64 520L); (mk_real_int64 184L); (mk_real_int64 232L); (mk_real_int64 344L); ]);\r
("y2_hi", [10; 12; 14; 15; 16; 17; 18; 19; 20; 21; 27; 29; 31; 32; 33; 34; 36; 40; 42; 43; 45; 55; 63; 64; 65; 66; 67; ], [(mk_real_int64 488L); (mk_real_int64 316L); (mk_real_int64 384L); (mk_real_int64 336L); (mk_real_int64 208L); (mk_real_int64 304L); (mk_real_int64 467L); (mk_real_int64 116L); (mk_real_int64 319L); (mk_real_int64 396L); (mk_real_int64 8L); (mk_real_int64 348L); (mk_real_int64 452L); (mk_real_int64 520L); (mk_real_int64 416L); (mk_real_int64 240L); (mk_real_int64 435L); (mk_real_int64 80L); (mk_real_int64 244L); (mk_real_int64 80L); (mk_real_int64 128L); (mk_real_int64 120L); (mk_real_int64 240L); (mk_real_int64 36L); (mk_real_int64 596L); (mk_real_int64 84L); (mk_real_int64 44L); ]);\r
("y3_lo", [22; 24; 30; 38; 41; 44; 47; 53; 56; 57; 59; 61; ], [(mk_real_int64 148L); (mk_real_int64 272L); (mk_real_int64 184L); (mk_real_int64 325L); (mk_real_int64 496L); (mk_real_int64 332L); (mk_real_int64 512L); (mk_real_int64 384L); (mk_real_int64 520L); (mk_real_int64 184L); (mk_real_int64 232L); (mk_real_int64 344L); ]);\r
("y3_hi", [10; 12; 14; 15; 16; 17; 18; 19; 20; 21; 27; 29; 31; 32; 33; 34; 36; 40; 42; 43; 45; 55; 63; 64; 65; 66; 67; ], [(mk_real_int64 488L); (mk_real_int64 316L); (mk_real_int64 384L); (mk_real_int64 336L); (mk_real_int64 208L); (mk_real_int64 304L); (mk_real_int64 467L); (mk_real_int64 116L); (mk_real_int64 319L); (mk_real_int64 396L); (mk_real_int64 8L); (mk_real_int64 348L); (mk_real_int64 452L); (mk_real_int64 520L); (mk_real_int64 416L); (mk_real_int64 240L); (mk_real_int64 435L); (mk_real_int64 80L); (mk_real_int64 244L); (mk_real_int64 80L); (mk_real_int64 128L); (mk_real_int64 120L); (mk_real_int64 240L); (mk_real_int64 36L); (mk_real_int64 596L); (mk_real_int64 84L); (mk_real_int64 44L); ]);\r
("y4_lo", [0; 2; 6; 8; 14; 17; 19; 20; 21; 24; 31; 32; 33; 37; 42; 49; 50; 51; 52; ], [(mk_real_int64 20L); (mk_real_int64 779L); (mk_real_int64 320L); (mk_real_int64 108L); (mk_real_int64 847L); (mk_real_int64 70L); (mk_real_int64 95L); (mk_real_int64 209L); (mk_real_int64 455L); (mk_real_int64 500L); (mk_real_int64 160L); (mk_real_int64 85L); (mk_real_int64 500L); (mk_real_int64 120L); (mk_real_int64 16L); (mk_real_int64 510L); (mk_real_int64 115L); (mk_real_int64 465L); (mk_real_int64 485L); ]);\r
("y4_hi", [4; 5; 7; 9; 10; 11; 12; 15; 22; 23; 26; 28; 30; 34; 35; 39; 41; 43; 45; 47; 53; ], [(mk_real_int64 390L); (mk_real_int64 11L); (mk_real_int64 79L); (mk_real_int64 31L); (mk_real_int64 44L); (mk_real_int64 35L); (mk_real_int64 295L); (mk_real_int64 320L); (mk_real_int64 500L); (mk_real_int64 141L); (mk_real_int64 360L); (mk_real_int64 860L); (mk_real_int64 330L); (mk_real_int64 405L); (mk_real_int64 130L); (mk_real_int64 110L); (mk_real_int64 250L); (mk_real_int64 160L); (mk_real_int64 280L); (mk_real_int64 291L); (mk_real_int64 514L); ]);\r
("y5_lo", [12; 15; 18; 22; 24; 30; 34; 38; 41; 42; 43; 44; 47; 53; 56; 59; ], [(mk_real_int64 129L); (mk_real_int64 464L); (mk_real_int64 108L); (mk_real_int64 148L); (mk_real_int64 272L); (mk_real_int64 184L); (mk_real_int64 500L); (mk_real_int64 40L); (mk_real_int64 496L); (mk_real_int64 176L); (mk_real_int64 500L); (mk_real_int64 332L); (mk_real_int64 122L); (mk_real_int64 384L); (mk_real_int64 16L); (mk_real_int64 232L); ]);\r
("y5_hi", [10; 14; 16; 17; 19; 20; 21; 25; 27; 29; 31; 32; 33; 36; 40; 45; 55; 57; 61; 63; 64; 65; 66; 67; ], [(mk_real_int64 488L); (mk_real_int64 384L); (mk_real_int64 208L); (mk_real_int64 304L); (mk_real_int64 431L); (mk_real_int64 44L); (mk_real_int64 396L); (mk_real_int64 70L); (mk_real_int64 8L); (mk_real_int64 393L); (mk_real_int64 452L); (mk_real_int64 500L); (mk_real_int64 416L); (mk_real_int64 460L); (mk_real_int64 80L); (mk_real_int64 128L); (mk_real_int64 250L); (mk_real_int64 71L); (mk_real_int64 316L); (mk_real_int64 240L); (mk_real_int64 206L); (mk_real_int64 221L); (mk_real_int64 84L); (mk_real_int64 364L); ]);\r
("y6_lo", [12; 15; 16; 17; 18; 19; 22; 24; 25; 26; 30; 34; 38; 41; 42; 43; 44; 46; 47; 53; 54; 56; 57; 59; 63; 67; ], [(mk_real_int64 129L); (mk_real_int64 464L); (mk_real_int64 287000L); (mk_real_int64 41000L); (mk_real_int64 108L); (mk_real_int64 5000L); (mk_real_int64 38148L); (mk_real_int64 272L); (mk_real_int64 361930L); (mk_real_int64 57000L); (mk_real_int64 184L); (mk_real_int64 500L); (mk_real_int64 40L); (mk_real_int64 496L); (mk_real_int64 176L); (mk_real_int64 500L); (mk_real_int64 62000L); (mk_real_int64 153000L); (mk_real_int64 122L); (mk_real_int64 95000L); (mk_real_int64 264000L); (mk_real_int64 16L); (mk_real_int64 100000L); (mk_real_int64 232L); (mk_real_int64 114000L); (mk_real_int64 368000L); ]);\r
("y6_hi", [10; 14; 16; 17; 19; 20; 21; 27; 29; 31; 32; 33; 36; 40; 44; 45; 53; 55; 57; 61; 63; 64; 65; 66; 67; ], [(mk_real_int64 488L); (mk_real_int64 384L); (mk_real_int64 208L); (mk_real_int64 304L); (mk_real_int64 431L); (mk_real_int64 44L); (mk_real_int64 396L); (mk_real_int64 8L); (mk_real_int64 393L); (mk_real_int64 452L); (mk_real_int64 500L); (mk_real_int64 416L); (mk_real_int64 460L); (mk_real_int64 80L); (mk_real_int64 668L); (mk_real_int64 128L); (mk_real_int64 616L); (mk_real_int64 250L); (mk_real_int64 71L); (mk_real_int64 316L); (mk_real_int64 240L); (mk_real_int64 206L); (mk_real_int64 221L); (mk_real_int64 84L); (mk_real_int64 364L); ]);\r
("ye_lo", [19; 21; 27; 30; 31; 32; 33; 53; 60; 63; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 175000L); (mk_real_int64 352000L); (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
("ye_hi", [22; 25; 34; 42; 43; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("yn_hi", [5; 9; 10; 12; 13; ], [(mk_real_int64 228L); (mk_real_int64 1228L); (mk_real_int64 3052L); (mk_real_int64 1064L); (mk_real_int64 1228L); ]);\r
("yn_lo", [0; 1; 2; 3; 4; 6; 7; 8; 11; 14; ], [(mk_real_int64 772L); (mk_real_int64 993L); (mk_real_int64 772L); (mk_real_int64 772L); (mk_real_int64 73L); (mk_real_int64 184L); (mk_real_int64 1176L); (mk_real_int64 2324L); (mk_real_int64 2615L); (mk_real_int64 1424L); ]);\r
];;\r
let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
end;;\r
\r
concl (Test_case.result)\r