Update from HH

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

needs "nobranching_lp.hl";;
\r
module Test_case = struct\r
let hypermap_string = "28820130324 20 6 0 1 2 3 4 5 3 0 5 6 3 6 5 4 3 6 4 3 3 6 3 7 3 7 3 8 3 8 3 2 3 8 2 9 3 9 2 10 3 10 2 1 3 10 1 11 3 11 1 0 4 11 0 7 12 3 0 6 7 3 12 7 8 3 12 8 9 3 12 9 13 3 13 9 10 3 13 10 11 3 11 12 13 ";;\r
let precision = 3;;\r
(***************)\r
(* Constraints *)\r
(***************)\r
let constraints = [\r
("azim_sum_neg", [0; 1; 9; 10; ], [(mk_real_int64 2198L); (mk_real_int64 2199L); (mk_real_int64 85L); (mk_real_int64 49L); ]);\r
("azim_sum", [7; 8; 13; ], [(mk_real_int64 666L); (mk_real_int64 68L); (mk_real_int64 87L); ]);\r
("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 249L); (mk_real_int64 249L); (mk_real_int64 1210L); (mk_real_int64 1210L); (mk_real_int64 1210L); (mk_real_int64 1210L); (mk_real_int64 226L); (mk_real_int64 1210L); (mk_real_int64 1159L); (mk_real_int64 880L); (mk_real_int64 880L); (mk_real_int64 1210L); (mk_real_int64 1210L); (mk_real_int64 453L); ]);\r
("sol_sum3", [1; 7; ], [(mk_real_int64 2175L); (mk_real_int64 49L); ]);\r
("sol_sum3_neg", [3; 4; 5; 11; 12; ], [(mk_real_int64 843L); (mk_real_int64 68L); (mk_real_int64 50L); (mk_real_int64 844L); (mk_real_int64 68L); ]);\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 226L); (mk_real_int64 226L); (mk_real_int64 226L); (mk_real_int64 226L); (mk_real_int64 1141L); (mk_real_int64 1159L); (mk_real_int64 880L); (mk_real_int64 880L); (mk_real_int64 880L); (mk_real_int64 880L); (mk_real_int64 1210L); (mk_real_int64 226L); (mk_real_int64 1159L); (mk_real_int64 880L); (mk_real_int64 526L); (mk_real_int64 526L); (mk_real_int64 526L); (mk_real_int64 526L); ]);\r
("tau_sum4_neg", [0; ], [(mk_real_int64 1210L); ]);\r
("tau_sum6_neg", [0; ], [(mk_real_int64 1210L); ]);\r
("ln_def_neg", [2; 3; 4; 5; 7; 8; 11; 12; ], [(mk_real_int64 334L); (mk_real_int64 334L); (mk_real_int64 334L); (mk_real_int64 361L); (mk_real_int64 346L); (mk_real_int64 278L); (mk_real_int64 334L); (mk_real_int64 334L); ]);\r
("ln_def", [0; 1; 6; 9; 10; 13; ], [(mk_real_int64 725L); (mk_real_int64 725L); (mk_real_int64 751L); (mk_real_int64 30L); (mk_real_int64 30L); (mk_real_int64 501L); ]);\r
("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 1566L); (mk_real_int64 1566L); (mk_real_int64 7600L); (mk_real_int64 7600L); (mk_real_int64 7600L); (mk_real_int64 7605L); (mk_real_int64 1417L); (mk_real_int64 7600L); (mk_real_int64 7283L); (mk_real_int64 5528L); (mk_real_int64 5528L); (mk_real_int64 7600L); (mk_real_int64 7600L); (mk_real_int64 2843L); ]);\r
("edge_sym_neg", [1; 7; 19; 20; 23; 25; 26; 29; 35; 40; 42; 48; 51; 53; 54; 57; ], [(mk_real_int64 96L); (mk_real_int64 1033L); (mk_real_int64 17L); (mk_real_int64 17L); (mk_real_int64 151L); (mk_real_int64 38L); (mk_real_int64 111L); (mk_real_int64 359L); (mk_real_int64 239L); (mk_real_int64 780L); (mk_real_int64 377L); (mk_real_int64 202L); (mk_real_int64 241L); (mk_real_int64 224L); (mk_real_int64 40L); (mk_real_int64 139L); ]);\r
("edge_sym", [8; 11; 14; 16; 28; 32; 34; 60; ], [(mk_real_int64 846L); (mk_real_int64 1033L); (mk_real_int64 2011L); (mk_real_int64 35L); (mk_real_int64 72L); (mk_real_int64 51L); (mk_real_int64 152L); (mk_real_int64 87L); ]);\r
("y1_def", [7; 13; 15; 19; 21; 27; 30; 33; 44; ], [(mk_real_int64 1087L); (mk_real_int64 1088L); (mk_real_int64 742L); (mk_real_int64 12L); (mk_real_int64 19L); (mk_real_int64 11L); (mk_real_int64 24L); (mk_real_int64 24L); (mk_real_int64 422L); ]);\r
("y1_def_neg", [6; 8; 9; 10; 14; 17; 20; 23; 24; 25; 26; 28; 32; 34; 35; 37; 45; 46; 47; 49; 50; 51; 52; 53; 54; 55; 56; 57; 59; 60; 61; 62; ], [(mk_real_int64 591L); (mk_real_int64 41L); (mk_real_int64 272L); (mk_real_int64 328L); (mk_real_int64 631L); (mk_real_int64 484L); (mk_real_int64 11L); (mk_real_int64 203L); (mk_real_int64 114L); (mk_real_int64 105L); (mk_real_int64 26L); (mk_real_int64 368L); (mk_real_int64 166L); (mk_real_int64 198L); (mk_real_int64 269L); (mk_real_int64 218L); (mk_real_int64 163L); (mk_real_int64 69L); (mk_real_int64 19L); (mk_real_int64 198L); (mk_real_int64 184L); (mk_real_int64 116L); (mk_real_int64 266L); (mk_real_int64 161L); (mk_real_int64 26L); (mk_real_int64 95L); (mk_real_int64 161L); (mk_real_int64 183L); (mk_real_int64 87L); (mk_real_int64 308L); (mk_real_int64 243L); (mk_real_int64 379L); ]);\r
("y2_def_neg", [7; 8; 10; 13; 23; 26; 27; 28; 30; 33; 35; 37; 44; 46; 51; 54; 55; ], [(mk_real_int64 331L); (mk_real_int64 41L); (mk_real_int64 328L); (mk_real_int64 331L); (mk_real_int64 203L); (mk_real_int64 82L); (mk_real_int64 13L); (mk_real_int64 21L); (mk_real_int64 7L); (mk_real_int64 7L); (mk_real_int64 46L); (mk_real_int64 218L); (mk_real_int64 128L); (mk_real_int64 81L); (mk_real_int64 171L); (mk_real_int64 26L); (mk_real_int64 95L); ]);\r
("y2_def", [6; 9; 14; 15; 17; 19; 20; 21; 24; 25; 32; 34; 45; 47; 49; 50; 52; 53; 56; 57; 59; 60; 61; 62; ], [(mk_real_int64 358L); (mk_real_int64 318L); (mk_real_int64 318L); (mk_real_int64 192L); (mk_real_int64 294L); (mk_real_int64 12L); (mk_real_int64 7L); (mk_real_int64 19L); (mk_real_int64 69L); (mk_real_int64 64L); (mk_real_int64 48L); (mk_real_int64 120L); (mk_real_int64 614L); (mk_real_int64 96L); (mk_real_int64 120L); (mk_real_int64 127L); (mk_real_int64 162L); (mk_real_int64 98L); (mk_real_int64 98L); (mk_real_int64 111L); (mk_real_int64 53L); (mk_real_int64 187L); (mk_real_int64 147L); (mk_real_int64 230L); ]);\r
("y3_def_neg", [7; 8; 10; 13; 23; 26; 27; 28; 30; 33; 35; 37; 44; 46; 51; 54; 55; ], [(mk_real_int64 331L); (mk_real_int64 41L); (mk_real_int64 328L); (mk_real_int64 331L); (mk_real_int64 203L); (mk_real_int64 82L); (mk_real_int64 13L); (mk_real_int64 21L); (mk_real_int64 7L); (mk_real_int64 7L); (mk_real_int64 46L); (mk_real_int64 218L); (mk_real_int64 128L); (mk_real_int64 81L); (mk_real_int64 171L); (mk_real_int64 26L); (mk_real_int64 95L); ]);\r
("y3_def", [6; 9; 14; 15; 17; 19; 20; 21; 24; 25; 32; 34; 45; 47; 49; 50; 52; 53; 56; 57; 59; 60; 61; 62; ], [(mk_real_int64 358L); (mk_real_int64 318L); (mk_real_int64 318L); (mk_real_int64 192L); (mk_real_int64 294L); (mk_real_int64 12L); (mk_real_int64 7L); (mk_real_int64 19L); (mk_real_int64 69L); (mk_real_int64 64L); (mk_real_int64 48L); (mk_real_int64 120L); (mk_real_int64 614L); (mk_real_int64 96L); (mk_real_int64 120L); (mk_real_int64 127L); (mk_real_int64 162L); (mk_real_int64 98L); (mk_real_int64 98L); (mk_real_int64 111L); (mk_real_int64 53L); (mk_real_int64 187L); (mk_real_int64 147L); (mk_real_int64 230L); ]);\r
("y4_def", [1; 4; 7; 9; 20; 21; 24; 27; 34; ], [(mk_real_int64 1681L); (mk_real_int64 703L); (mk_real_int64 1681L); (mk_real_int64 486L); (mk_real_int64 18L); (mk_real_int64 44L); (mk_real_int64 38L); (mk_real_int64 38L); (mk_real_int64 652L); ]);\r
("y4_def_neg", [0; 2; 3; 8; 11; 13; 14; 15; 17; 18; 19; 22; 26; 28; 29; 31; 32; 35; 36; 37; 39; 40; 41; 42; 43; 44; 45; 46; 47; 49; 50; 51; 52; ], [(mk_real_int64 675L); (mk_real_int64 28L); (mk_real_int64 703L); (mk_real_int64 702L); (mk_real_int64 553L); (mk_real_int64 23L); (mk_real_int64 12L); (mk_real_int64 10L); (mk_real_int64 141L); (mk_real_int64 131L); (mk_real_int64 120L); (mk_real_int64 369L); (mk_real_int64 175L); (mk_real_int64 226L); (mk_real_int64 249L); (mk_real_int64 151L); (mk_real_int64 1L); (mk_real_int64 718L); (mk_real_int64 40L); (mk_real_int64 146L); (mk_real_int64 226L); (mk_real_int64 238L); (mk_real_int64 44L); (mk_real_int64 304L); (mk_real_int64 184L); (mk_real_int64 18L); (mk_real_int64 66L); (mk_real_int64 184L); (mk_real_int64 209L); (mk_real_int64 100L); (mk_real_int64 351L); (mk_real_int64 277L); (mk_real_int64 433L); ]);\r
("y5_def_neg", [7; 8; 13; 15; 19; 21; 23; 26; 30; 33; 35; 37; 44; 46; 51; 54; 55; ], [(mk_real_int64 331L); (mk_real_int64 28L); (mk_real_int64 331L); (mk_real_int64 293L); (mk_real_int64 23L); (mk_real_int64 10L); (mk_real_int64 141L); (mk_real_int64 61L); (mk_real_int64 7L); (mk_real_int64 7L); (mk_real_int64 6L); (mk_real_int64 151L); (mk_real_int64 128L); (mk_real_int64 57L); (mk_real_int64 123L); (mk_real_int64 18L); (mk_real_int64 66L); ]);\r
("y5_def", [6; 9; 10; 14; 17; 20; 24; 25; 27; 28; 32; 34; 45; 47; 49; 50; 52; 53; 56; 57; 59; 60; 61; 62; ], [(mk_real_int64 358L); (mk_real_int64 330L); (mk_real_int64 703L); (mk_real_int64 330L); (mk_real_int64 294L); (mk_real_int64 7L); (mk_real_int64 69L); (mk_real_int64 64L); (mk_real_int64 10L); (mk_real_int64 28L); (mk_real_int64 58L); (mk_real_int64 120L); (mk_real_int64 128L); (mk_real_int64 57L); (mk_real_int64 120L); (mk_real_int64 127L); (mk_real_int64 162L); (mk_real_int64 98L); (mk_real_int64 98L); (mk_real_int64 111L); (mk_real_int64 53L); (mk_real_int64 187L); (mk_real_int64 147L); (mk_real_int64 230L); ]);\r
("y6_def_neg", [7; 8; 13; 15; 19; 23; 26; 33; 35; 37; 44; 46; 51; 54; ], [(mk_real_int64 331L); (mk_real_int64 28L); (mk_real_int64 330L); (mk_real_int64 293L); (mk_real_int64 23L); (mk_real_int64 141L); (mk_real_int64 61L); (mk_real_int64 7L); (mk_real_int64 6L); (mk_real_int64 1L); (mk_real_int64 128L); (mk_real_int64 57L); (mk_real_int64 123L); (mk_real_int64 18L); ]);\r
("y6_def", [6; 9; 10; 14; 17; 20; 21; 22; 24; 25; 27; 28; 30; 32; 34; 38; 45; 47; 49; 50; 52; 53; 55; 56; 57; 58; 59; 60; 61; 62; 63; ], [(mk_real_int64 358L); (mk_real_int64 330L); (mk_real_int64 703L); (mk_real_int64 330L); (mk_real_int64 294L); (mk_real_int64 7L); (mk_real_int64 158L); (mk_real_int64 151L); (mk_real_int64 69L); (mk_real_int64 64L); (mk_real_int64 10L); (mk_real_int64 28L); (mk_real_int64 103L); (mk_real_int64 58L); (mk_real_int64 120L); (mk_real_int64 151L); (mk_real_int64 128L); (mk_real_int64 57L); (mk_real_int64 120L); (mk_real_int64 460L); (mk_real_int64 162L); (mk_real_int64 98L); (mk_real_int64 335L); (mk_real_int64 314L); (mk_real_int64 111L); (mk_real_int64 437L); (mk_real_int64 53L); (mk_real_int64 187L); (mk_real_int64 147L); (mk_real_int64 318L); (mk_real_int64 198L); ]);\r
("RHA", [0; 7; 10; 11; 13; 16; 17; 18; 19; 22; 23; 24; 25; 31; 32; 35; 40; 43; 45; 46; 47; 52; 53; 56; 57; 59; 60; 61; 62; ], [(mk_real_int64 1L); (mk_real_int64 24L); (mk_real_int64 24L); (mk_real_int64 24L); (mk_real_int64 24L); (mk_real_int64 984L); (mk_real_int64 177L); (mk_real_int64 68L); (mk_real_int64 68L); (mk_real_int64 50L); (mk_real_int64 50L); (mk_real_int64 89L); (mk_real_int64 155L); (mk_real_int64 330L); (mk_real_int64 108L); (mk_real_int64 98L); (mk_real_int64 1L); (mk_real_int64 985L); (mk_real_int64 178L); (mk_real_int64 50L); (mk_real_int64 50L); (mk_real_int64 239L); (mk_real_int64 85L); (mk_real_int64 85L); (mk_real_int64 49L); (mk_real_int64 208L); (mk_real_int64 170L); (mk_real_int64 278L); (mk_real_int64 51L); ]);\r
("RHB", [54; 55; 58; 63; ], [(mk_real_int64 74L); (mk_real_int64 74L); (mk_real_int64 74L); (mk_real_int64 74L); ]);\r
("yy10", [1; 8; 15; 16; 40; 42; ], [(mk_real_int64 96L); (mk_real_int64 1165L); (mk_real_int64 1165L); (mk_real_int64 745L); (mk_real_int64 780L); (mk_real_int64 377L); ]);\r
("tau4", [0; ], [(mk_real_int64 330L); ]);\r
("tau6", [0; ], [(mk_real_int64 1210L); ]);\r
("ineq105", [0; ], [(mk_real_int64 1L); ]);\r
("ineq106", [0; 8; 11; 14; 18; 19; 22; 26; 28; 29; 32; 35; 39; 40; 42; 43; 46; 47; 49; 50; 51; 52; ], [(mk_real_int64 985L); (mk_real_int64 984L); (mk_real_int64 807L); (mk_real_int64 18L); (mk_real_int64 191L); (mk_real_int64 175L); (mk_real_int64 330L); (mk_real_int64 222L); (mk_real_int64 330L); (mk_real_int64 231L); (mk_real_int64 1L); (mk_real_int64 806L); (mk_real_int64 330L); (mk_real_int64 279L); (mk_real_int64 444L); (mk_real_int64 268L); (mk_real_int64 268L); (mk_real_int64 304L); (mk_real_int64 145L); (mk_real_int64 513L); (mk_real_int64 405L); (mk_real_int64 632L); ]);\r
("ineq107", [1; 5; 7; 9; 20; 21; 24; 27; 34; 36; 41; ], [(mk_real_int64 2175L); (mk_real_int64 1L); (mk_real_int64 2175L); (mk_real_int64 843L); (mk_real_int64 85L); (mk_real_int64 36L); (mk_real_int64 49L); (mk_real_int64 49L); (mk_real_int64 844L); (mk_real_int64 18L); (mk_real_int64 85L); ]);\r
("ineq108", [3; 22; 37; 40; ], [(mk_real_int64 985L); (mk_real_int64 49L); (mk_real_int64 193L); (mk_real_int64 68L); ]);\r
("ineq109", [4; 21; ], [(mk_real_int64 2175L); (mk_real_int64 49L); ]);\r
("ineq110", [9; 13; 15; 35; 37; ], [(mk_real_int64 843L); (mk_real_int64 68L); (mk_real_int64 50L); (mk_real_int64 844L); (mk_real_int64 68L); ]);\r
("ineq111", [2; 3; 8; 13; 17; 20; 22; 26; 29; 31; 36; 41; 44; 45; ], [(mk_real_int64 226L); (mk_real_int64 226L); (mk_real_int64 226L); (mk_real_int64 78L); (mk_real_int64 1131L); (mk_real_int64 382L); (mk_real_int64 880L); (mk_real_int64 181L); (mk_real_int64 723L); (mk_real_int64 1210L); (mk_real_int64 433L); (mk_real_int64 880L); (mk_real_int64 144L); (mk_real_int64 526L); ]);\r
("ineq114", [10; 12; 15; 18; 19; 25; 26; 29; 33; 37; 42; 49; 50; 51; 52; ], [(mk_real_int64 226L); (mk_real_int64 1063L); (mk_real_int64 29L); (mk_real_int64 251L); (mk_real_int64 247L); (mk_real_int64 527L); (mk_real_int64 172L); (mk_real_int64 157L); (mk_real_int64 226L); (mk_real_int64 727L); (mk_real_int64 382L); (mk_real_int64 254L); (mk_real_int64 272L); (mk_real_int64 444L); (mk_real_int64 82L); ]);\r
("ineq116", [3; ], [(mk_real_int64 1190L); ]);\r
("ineq120", [1; 2; ], [(mk_real_int64 1L); (mk_real_int64 879L); ]);\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; ], [(mk_real_int64 950L); (mk_real_int64 950L); (mk_real_int64 4000L); (mk_real_int64 4000L); (mk_real_int64 4000L); (mk_real_int64 30125L); (mk_real_int64 1025L); (mk_real_int64 16000L); (mk_real_int64 3475L); (mk_real_int64 2600L); (mk_real_int64 2600L); (mk_real_int64 4000L); (mk_real_int64 4000L); (mk_real_int64 1475L); ]);\r
];;\r
\r
(*************************)\r
\r
let variable_bounds = [\r
("azim_hi", [4; 5; 16; 21; 24; 35; 41; 43; 47; 52; 54; 55; 58; 59; 60; 62; 63; ], [(mk_real_int64 2199000L); (mk_real_int64 2198000L); (mk_real_int64 476L); (mk_real_int64 154L); (mk_real_int64 126L); (mk_real_int64 282L); (mk_real_int64 282L); (mk_real_int64 476L); (mk_real_int64 102L); (mk_real_int64 132L); (mk_real_int64 24L); (mk_real_int64 24L); (mk_real_int64 24L); (mk_real_int64 4L); (mk_real_int64 272L); (mk_real_int64 332L); (mk_real_int64 24L); ]);\r
("azim_lo", [7; 10; 11; 18; 25; 31; 32; 40; 61; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 562L); (mk_real_int64 378L); (mk_real_int64 98L); (mk_real_int64 328L); (mk_real_int64 242L); (mk_real_int64 56L); ]);\r
("rhazim_hi", [0; 4; 5; 6; 7; 10; 11; 13; 24; 38; 40; 43; ], [(mk_real_int64 1000L); (mk_real_int64 961000L); (mk_real_int64 961000L); (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_lo", [18; 19; 22; 23; 35; 46; 47; 52; 53; 54; 55; 56; 57; 58; 59; 60; 61; 62; 63; ], [(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
("rho_lo", [0; 1; 5; ], [(mk_real_int64 1284L); (mk_real_int64 1284L); (mk_real_int64 1360L); ]);\r
("rho_hi", [2; 3; 4; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 3640L); (mk_real_int64 3640L); (mk_real_int64 3640L); (mk_real_int64 3184L); (mk_real_int64 3640L); (mk_real_int64 156L); (mk_real_int64 1920L); (mk_real_int64 1920L); (mk_real_int64 3640L); (mk_real_int64 3640L); (mk_real_int64 3652L); ]);\r
("tau_hi", [6; 14; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("y1_lo", [0; 9; 10; 13; 14; 15; 17; 19; 23; 24; 26; 27; 38; 47; 52; 62; ], [(mk_real_int64 315L); (mk_real_int64 155L); (mk_real_int64 425L); (mk_real_int64 500L); (mk_real_int64 80L); (mk_real_int64 160L); (mk_real_int64 200L); (mk_real_int64 200L); (mk_real_int64 580L); (mk_real_int64 600L); (mk_real_int64 260L); (mk_real_int64 399L); (mk_real_int64 600L); (mk_real_int64 515L); (mk_real_int64 400L); (mk_real_int64 200L); ]);\r
("y1_hi", [7; 8; 11; 20; 28; 30; 32; 33; 35; 37; 45; 46; 50; 51; 53; 54; 55; 56; 57; 60; ], [(mk_real_int64 500L); (mk_real_int64 320L); (mk_real_int64 500L); (mk_real_int64 200L); (mk_real_int64 85L); (mk_real_int64 500L); (mk_real_int64 220L); (mk_real_int64 500L); (mk_real_int64 260L); (mk_real_int64 200L); (mk_real_int64 120L); (mk_real_int64 60L); (mk_real_int64 620L); (mk_real_int64 100L); (mk_real_int64 200L); (mk_real_int64 80L); (mk_real_int64 320L); (mk_real_int64 200L); (mk_real_int64 600L); (mk_real_int64 200L); ]);\r
("y2_hi", [0; 6; 7; 8; 13; 15; 24; 26; 27; 28; 32; 34; 37; 38; 45; 46; 47; 49; 54; 55; 61; 62; ], [(mk_real_int64 402L); (mk_real_int64 540L); (mk_real_int64 400L); (mk_real_int64 320L); (mk_real_int64 400L); (mk_real_int64 204L); (mk_real_int64 524L); (mk_real_int64 320L); (mk_real_int64 129L); (mk_real_int64 556L); (mk_real_int64 228L); (mk_real_int64 120L); (mk_real_int64 200L); (mk_real_int64 364L); (mk_real_int64 104L); (mk_real_int64 324L); (mk_real_int64 92L); (mk_real_int64 120L); (mk_real_int64 80L); (mk_real_int64 320L); (mk_real_int64 420L); (mk_real_int64 48L); ]);\r
("y2_lo", [9; 10; 11; 14; 17; 19; 20; 23; 25; 30; 33; 35; 44; 50; 51; 52; 53; 56; 57; 59; 60; ], [(mk_real_int64 140L); (mk_real_int64 425L); (mk_real_int64 152L); (mk_real_int64 504L); (mk_real_int64 252L); (mk_real_int64 200L); (mk_real_int64 448L); (mk_real_int64 580L); (mk_real_int64 300L); (mk_real_int64 448L); (mk_real_int64 448L); (mk_real_int64 56L); (mk_real_int64 288L); (mk_real_int64 692L); (mk_real_int64 320L); (mk_real_int64 384L); (mk_real_int64 448L); (mk_real_int64 448L); (mk_real_int64 344L); (mk_real_int64 220L); (mk_real_int64 268L); ]);\r
("y3_hi", [0; 6; 7; 8; 13; 15; 24; 26; 27; 28; 32; 34; 37; 38; 45; 46; 47; 49; 54; 55; 61; 62; ], [(mk_real_int64 402L); (mk_real_int64 540L); (mk_real_int64 400L); (mk_real_int64 320L); (mk_real_int64 400L); (mk_real_int64 204L); (mk_real_int64 524L); (mk_real_int64 320L); (mk_real_int64 129L); (mk_real_int64 556L); (mk_real_int64 228L); (mk_real_int64 120L); (mk_real_int64 200L); (mk_real_int64 364L); (mk_real_int64 104L); (mk_real_int64 324L); (mk_real_int64 92L); (mk_real_int64 120L); (mk_real_int64 80L); (mk_real_int64 320L); (mk_real_int64 420L); (mk_real_int64 48L); ]);\r
("y3_lo", [9; 10; 11; 14; 17; 19; 20; 23; 25; 30; 33; 35; 44; 50; 51; 52; 53; 56; 57; 59; 60; ], [(mk_real_int64 140L); (mk_real_int64 425L); (mk_real_int64 152L); (mk_real_int64 504L); (mk_real_int64 252L); (mk_real_int64 200L); (mk_real_int64 448L); (mk_real_int64 580L); (mk_real_int64 300L); (mk_real_int64 448L); (mk_real_int64 448L); (mk_real_int64 56L); (mk_real_int64 288L); (mk_real_int64 692L); (mk_real_int64 320L); (mk_real_int64 384L); (mk_real_int64 448L); (mk_real_int64 448L); (mk_real_int64 344L); (mk_real_int64 220L); (mk_real_int64 268L); ]);\r
("y4_hi", [0; 1; 3; 4; 5; 7; 9; 11; 15; 18; 19; 26; 29; 32; 34; 35; 37; 40; 43; 45; 46; 47; 49; 52; ], [(mk_real_int64 275L); (mk_real_int64 275L); (mk_real_int64 25L); (mk_real_int64 1700L); (mk_real_int64 773L); (mk_real_int64 275L); (mk_real_int64 411L); (mk_real_int64 205L); (mk_real_int64 200L); (mk_real_int64 165L); (mk_real_int64 125L); (mk_real_int64 305L); (mk_real_int64 390L); (mk_real_int64 315L); (mk_real_int64 412L); (mk_real_int64 466L); (mk_real_int64 467L); (mk_real_int64 305L); (mk_real_int64 420L); (mk_real_int64 250L); (mk_real_int64 420L); (mk_real_int64 760L); (mk_real_int64 675L); (mk_real_int64 80L); ]);\r
("y4_lo", [2; 8; 13; 14; 17; 20; 21; 22; 24; 27; 28; 31; 36; 39; 41; 42; 50; 51; ], [(mk_real_int64 250L); (mk_real_int64 290L); (mk_real_int64 78L); (mk_real_int64 330L); (mk_real_int64 375L); (mk_real_int64 45L); (mk_real_int64 296L); (mk_real_int64 615L); (mk_real_int64 123L); (mk_real_int64 123L); (mk_real_int64 50L); (mk_real_int64 250L); (mk_real_int64 211L); (mk_real_int64 50L); (mk_real_int64 295L); (mk_real_int64 140L); (mk_real_int64 405L); (mk_real_int64 425L); ]);\r
("y5_hi", [0; 6; 7; 9; 10; 13; 21; 24; 26; 27; 32; 34; 38; 46; 49; 51; 55; 61; 62; ], [(mk_real_int64 402L); (mk_real_int64 540L); (mk_real_int64 400L); (mk_real_int64 290L); (mk_real_int64 1700L); (mk_real_int64 400L); (mk_real_int64 200L); (mk_real_int64 524L); (mk_real_int64 330L); (mk_real_int64 404L); (mk_real_int64 183L); (mk_real_int64 120L); (mk_real_int64 364L); (mk_real_int64 139L); (mk_real_int64 120L); (mk_real_int64 80L); (mk_real_int64 250L); (mk_real_int64 420L); (mk_real_int64 48L); ]);\r
("y5_lo", [8; 11; 14; 15; 17; 19; 20; 23; 25; 28; 30; 33; 35; 37; 44; 45; 47; 50; 52; 53; 56; 57; 59; 60; ], [(mk_real_int64 250L); (mk_real_int64 152L); (mk_real_int64 74L); (mk_real_int64 364L); (mk_real_int64 252L); (mk_real_int64 78L); (mk_real_int64 448L); (mk_real_int64 375L); (mk_real_int64 300L); (mk_real_int64 44L); (mk_real_int64 448L); (mk_real_int64 448L); (mk_real_int64 291L); (mk_real_int64 250L); (mk_real_int64 288L); (mk_real_int64 40L); (mk_real_int64 76L); (mk_real_int64 692L); (mk_real_int64 384L); (mk_real_int64 448L); (mk_real_int64 448L); (mk_real_int64 344L); (mk_real_int64 220L); (mk_real_int64 268L); ]);\r
("y6_hi", [0; 6; 7; 9; 10; 13; 21; 24; 26; 27; 30; 32; 34; 37; 38; 46; 49; 50; 51; 55; 56; 61; 62; ], [(mk_real_int64 402L); (mk_real_int64 540L); (mk_real_int64 400L); (mk_real_int64 290L); (mk_real_int64 1700L); (mk_real_int64 400L); (mk_real_int64 200L); (mk_real_int64 524L); (mk_real_int64 330L); (mk_real_int64 404L); (mk_real_int64 552L); (mk_real_int64 183L); (mk_real_int64 120L); (mk_real_int64 750L); (mk_real_int64 364L); (mk_real_int64 139L); (mk_real_int64 120L); (mk_real_int64 308L); (mk_real_int64 80L); (mk_real_int64 250L); (mk_real_int64 552L); (mk_real_int64 420L); (mk_real_int64 48L); ]);\r
("y6_lo", [8; 11; 13; 14; 15; 17; 19; 20; 21; 22; 23; 25; 28; 30; 33; 35; 37; 38; 44; 45; 47; 50; 52; 53; 55; 56; 57; 58; 59; 60; 62; 63; ], [(mk_real_int64 250L); (mk_real_int64 152L); (mk_real_int64 1000L); (mk_real_int64 74L); (mk_real_int64 364L); (mk_real_int64 252L); (mk_real_int64 78L); (mk_real_int64 448L); (mk_real_int64 168000L); (mk_real_int64 151000L); (mk_real_int64 375L); (mk_real_int64 300L); (mk_real_int64 44L); (mk_real_int64 111000L); (mk_real_int64 448L); (mk_real_int64 291L); (mk_real_int64 151000L); (mk_real_int64 151000L); (mk_real_int64 288L); (mk_real_int64 40L); (mk_real_int64 76L); (mk_real_int64 334000L); (mk_real_int64 384L); (mk_real_int64 448L); (mk_real_int64 401000L); (mk_real_int64 217000L); (mk_real_int64 344L); (mk_real_int64 437000L); (mk_real_int64 220L); (mk_real_int64 268L); (mk_real_int64 88000L); (mk_real_int64 198000L); ]);\r
("ye_lo", [6; 7; 25; 26; 33; 37; 48; 63; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 90000L); (mk_real_int64 1000L); (mk_real_int64 86000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("ye_hi", [17; 19; 20; 33; 49; 52; 59; 62; ], [(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_lo", [0; 5; 8; 10; ], [(mk_real_int64 175L); (mk_real_int64 436L); (mk_real_int64 128L); (mk_real_int64 1690L); ]);\r
("yn_hi", [1; 2; 3; 4; 6; 7; 9; 11; 12; 13; ], [(mk_real_int64 1825L); (mk_real_int64 1616L); (mk_real_int64 616L); (mk_real_int64 616L); (mk_real_int64 827L); (mk_real_int64 1704L); (mk_real_int64 310L); (mk_real_int64 616L); (mk_real_int64 1616L); (mk_real_int64 1577L); ]);\r
];;\r
let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
end;;\r
\r
concl (Test_case.result)\r