Update from HH

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

needs "nobranching_lp.hl";;
\r
module Test_case = struct\r
let hypermap_string = "211626865969 19 4 0 1 2 3 4 0 3 4 5 3 4 3 6 3 6 3 2 3 6 2 7 3 7 2 1 3 7 1 8 3 8 1 9 3 9 1 0 3 9 0 10 3 10 0 5 4 9 10 5 11 3 11 5 4 3 11 4 12 3 12 4 6 3 12 6 7 3 12 7 8 3 11 12 8 3 8 9 11 ";;\r
let precision = 4;;\r
(***************)\r
(* Constraints *)\r
(***************)\r
let constraints = [\r
("azim_sum", [2; 3; 6; ], [(mk_real_int64 1891L); (mk_real_int64 319L); (mk_real_int64 2854L); ]);\r
("azim_sum_neg", [1; 4; 5; 7; 8; 9; 10; 12; ], [(mk_real_int64 3198L); (mk_real_int64 3393L); (mk_real_int64 1554L); (mk_real_int64 1828L); (mk_real_int64 2751L); (mk_real_int64 704L); (mk_real_int64 394L); (mk_real_int64 293L); ]);\r
("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 9935L); (mk_real_int64 9935L); (mk_real_int64 9935L); (mk_real_int64 9935L); (mk_real_int64 7489L); (mk_real_int64 9043L); (mk_real_int64 9935L); (mk_real_int64 10537L); (mk_real_int64 9935L); (mk_real_int64 9365L); (mk_real_int64 8232L); (mk_real_int64 9320L); (mk_real_int64 8433L); ]);\r
("sol_sum3_neg", [0; 10; 11; 15; ], [(mk_real_int64 1356L); (mk_real_int64 713L); (mk_real_int64 707L); (mk_real_int64 5090L); ]);\r
("sol_sum3", [1; 2; 9; 12; 13; 14; ], [(mk_real_int64 1227L); (mk_real_int64 2993L); (mk_real_int64 293L); (mk_real_int64 101L); (mk_real_int64 355L); (mk_real_int64 293L); ]);\r
("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; ], [(mk_real_int64 8579L); (mk_real_int64 9935L); (mk_real_int64 9935L); (mk_real_int64 7273L); (mk_real_int64 7273L); (mk_real_int64 7838L); (mk_real_int64 9320L); (mk_real_int64 7489L); (mk_real_int64 7489L); (mk_real_int64 8433L); (mk_real_int64 7427L); (mk_real_int64 7954L); (mk_real_int64 7285L); (mk_real_int64 7540L); (mk_real_int64 7091L); (mk_real_int64 3050L); ]);\r
("tau_sum4_neg", [0; 1; 2; ], [(mk_real_int64 9935L); (mk_real_int64 9935L); (mk_real_int64 7489L); ]);\r
("ln_def_neg", [0; 1; 2; 3; 6; 7; 8; 9; 11; ], [(mk_real_int64 954L); (mk_real_int64 954L); (mk_real_int64 954L); (mk_real_int64 954L); (mk_real_int64 954L); (mk_real_int64 1617L); (mk_real_int64 954L); (mk_real_int64 326L); (mk_real_int64 276L); ]);\r
("ln_def", [4; 5; 10; 12; ], [(mk_real_int64 1743L); (mk_real_int64 30L); (mk_real_int64 924L); (mk_real_int64 702L); ]);\r
("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 62425L); (mk_real_int64 62425L); (mk_real_int64 62425L); (mk_real_int64 62425L); (mk_real_int64 47055L); (mk_real_int64 56818L); (mk_real_int64 62425L); (mk_real_int64 66203L); (mk_real_int64 62425L); (mk_real_int64 58842L); (mk_real_int64 51723L); (mk_real_int64 58560L); (mk_real_int64 52986L); ]);\r
("edge_sym", [0; 1; 6; 15; 16; 19; 21; 22; 24; 25; 37; 38; 41; 43; 44; 53; 56; ], [(mk_real_int64 13L); (mk_real_int64 13L); (mk_real_int64 106L); (mk_real_int64 95L); (mk_real_int64 285L); (mk_real_int64 401L); (mk_real_int64 1198L); (mk_real_int64 192L); (mk_real_int64 356L); (mk_real_int64 356L); (mk_real_int64 262L); (mk_real_int64 998L); (mk_real_int64 496L); (mk_real_int64 50L); (mk_real_int64 50L); (mk_real_int64 278L); (mk_real_int64 998L); ]);\r
("edge_sym_neg", [7; 9; 13; 28; 30; 31; 47; 50; ], [(mk_real_int64 1457L); (mk_real_int64 1124L); (mk_real_int64 1985L); (mk_real_int64 2642L); (mk_real_int64 497L); (mk_real_int64 736L); (mk_real_int64 1859L); (mk_real_int64 278L); ]);\r
("y1_def_neg", [1; 8; 12; 13; 15; 16; 22; 24; 25; 27; 28; 30; 35; 38; 39; 41; 44; 46; 47; 48; 49; 50; 51; 54; 55; 56; ], [(mk_real_int64 10L); (mk_real_int64 643L); (mk_real_int64 288L); (mk_real_int64 988L); (mk_real_int64 1109L); (mk_real_int64 452L); (mk_real_int64 339L); (mk_real_int64 264L); (mk_real_int64 889L); (mk_real_int64 814L); (mk_real_int64 1699L); (mk_real_int64 137L); (mk_real_int64 577L); (mk_real_int64 205L); (mk_real_int64 224L); (mk_real_int64 134L); (mk_real_int64 312L); (mk_real_int64 1064L); (mk_real_int64 497L); (mk_real_int64 4L); (mk_real_int64 15L); (mk_real_int64 451L); (mk_real_int64 323L); (mk_real_int64 805L); (mk_real_int64 547L); (mk_real_int64 131L); ]);\r
("y1_def", [10; 17; 18; 20; 31; 32; 40; 42; 57; ], [(mk_real_int64 336L); (mk_real_int64 44L); (mk_real_int64 268L); (mk_real_int64 44L); (mk_real_int64 1604L); (mk_real_int64 928L); (mk_real_int64 325L); (mk_real_int64 271L); (mk_real_int64 1934L); ]);\r
("y2_def", [1; 8; 10; 12; 22; 25; 27; 30; 35; 38; 41; 42; 44; 46; 48; 51; 54; 56; 57; ], [(mk_real_int64 13L); (mk_real_int64 390L); (mk_real_int64 336L); (mk_real_int64 447L); (mk_real_int64 206L); (mk_real_int64 539L); (mk_real_int64 912L); (mk_real_int64 83L); (mk_real_int64 736L); (mk_real_int64 262L); (mk_real_int64 10L); (mk_real_int64 271L); (mk_real_int64 190L); (mk_real_int64 645L); (mk_real_int64 2L); (mk_real_int64 109L); (mk_real_int64 488L); (mk_real_int64 90L); (mk_real_int64 1934L); ]);\r
("y2_def_neg", [13; 15; 16; 17; 18; 20; 24; 28; 31; 32; 39; 40; 47; 49; 50; 55; ], [(mk_real_int64 2273L); (mk_real_int64 1242L); (mk_real_int64 452L); (mk_real_int64 14L); (mk_real_int64 81L); (mk_real_int64 14L); (mk_real_int64 264L); (mk_real_int64 1384L); (mk_real_int64 608L); (mk_real_int64 316L); (mk_real_int64 224L); (mk_real_int64 99L); (mk_real_int64 469L); (mk_real_int64 15L); (mk_real_int64 451L); (mk_real_int64 547L); ]);\r
("y3_def", [1; 8; 10; 12; 22; 25; 27; 30; 35; 38; 41; 42; 44; 46; 48; 51; 54; 56; 57; ], [(mk_real_int64 13L); (mk_real_int64 390L); (mk_real_int64 336L); (mk_real_int64 447L); (mk_real_int64 206L); (mk_real_int64 539L); (mk_real_int64 912L); (mk_real_int64 83L); (mk_real_int64 736L); (mk_real_int64 262L); (mk_real_int64 10L); (mk_real_int64 271L); (mk_real_int64 190L); (mk_real_int64 645L); (mk_real_int64 2L); (mk_real_int64 109L); (mk_real_int64 488L); (mk_real_int64 90L); (mk_real_int64 1934L); ]);\r
("y3_def_neg", [13; 15; 16; 17; 18; 20; 24; 28; 31; 32; 39; 40; 47; 49; 50; 55; ], [(mk_real_int64 2273L); (mk_real_int64 1242L); (mk_real_int64 452L); (mk_real_int64 14L); (mk_real_int64 81L); (mk_real_int64 14L); (mk_real_int64 264L); (mk_real_int64 1384L); (mk_real_int64 608L); (mk_real_int64 316L); (mk_real_int64 224L); (mk_real_int64 99L); (mk_real_int64 469L); (mk_real_int64 15L); (mk_real_int64 451L); (mk_real_int64 547L); ]);\r
("y4_def_neg", [0; 2; 4; 7; 14; 16; 17; 19; 20; 22; 27; 29; 30; 32; 34; 35; 36; 38; 39; 42; 43; 44; 45; ], [(mk_real_int64 734L); (mk_real_int64 390L); (mk_real_int64 841L); (mk_real_int64 683L); (mk_real_int64 387L); (mk_real_int64 183L); (mk_real_int64 1015L); (mk_real_int64 1717L); (mk_real_int64 1268L); (mk_real_int64 156L); (mk_real_int64 155L); (mk_real_int64 7L); (mk_real_int64 140L); (mk_real_int64 357L); (mk_real_int64 1214L); (mk_real_int64 695L); (mk_real_int64 4L); (mk_real_int64 313L); (mk_real_int64 192L); (mk_real_int64 920L); (mk_real_int64 380L); (mk_real_int64 158L); (mk_real_int64 998L); ]);\r
("y4_def", [5; 8; 9; 10; 12; 23; 24; 28; 37; ], [(mk_real_int64 678L); (mk_real_int64 967L); (mk_real_int64 69L); (mk_real_int64 414L); (mk_real_int64 69L); (mk_real_int64 2558L); (mk_real_int64 1457L); (mk_real_int64 503L); (mk_real_int64 33L); ]);\r
("y5_def", [1; 8; 12; 16; 22; 25; 27; 30; 35; 38; 41; 44; 46; 48; 49; 51; 54; 56; ], [(mk_real_int64 13L); (mk_real_int64 390L); (mk_real_int64 447L); (mk_real_int64 967L); (mk_real_int64 206L); (mk_real_int64 539L); (mk_real_int64 912L); (mk_real_int64 83L); (mk_real_int64 736L); (mk_real_int64 262L); (mk_real_int64 149L); (mk_real_int64 190L); (mk_real_int64 645L); (mk_real_int64 2L); (mk_real_int64 33L); (mk_real_int64 278L); (mk_real_int64 488L); (mk_real_int64 229L); ]);\r
("y5_def_neg", [4; 10; 13; 15; 17; 18; 20; 24; 28; 31; 32; 39; 40; 42; 47; 50; 55; 57; ], [(mk_real_int64 1457L); (mk_real_int64 390L); (mk_real_int64 1145L); (mk_real_int64 872L); (mk_real_int64 14L); (mk_real_int64 81L); (mk_real_int64 14L); (mk_real_int64 183L); (mk_real_int64 925L); (mk_real_int64 580L); (mk_real_int64 308L); (mk_real_int64 155L); (mk_real_int64 99L); (mk_real_int64 140L); (mk_real_int64 645L); (mk_real_int64 313L); (mk_real_int64 380L); (mk_real_int64 998L); ]);\r
("y6_def", [1; 8; 12; 14; 16; 22; 25; 27; 30; 32; 34; 35; 38; 41; 44; 46; 48; 49; 51; 54; 55; 56; ], [(mk_real_int64 13L); (mk_real_int64 390L); (mk_real_int64 1145L); (mk_real_int64 1890L); (mk_real_int64 967L); (mk_real_int64 206L); (mk_real_int64 539L); (mk_real_int64 912L); (mk_real_int64 83L); (mk_real_int64 497L); (mk_real_int64 308L); (mk_real_int64 736L); (mk_real_int64 262L); (mk_real_int64 149L); (mk_real_int64 190L); (mk_real_int64 645L); (mk_real_int64 2140L); (mk_real_int64 33L); (mk_real_int64 278L); (mk_real_int64 488L); (mk_real_int64 413L); (mk_real_int64 229L); ]);\r
("y6_def_neg", [10; 13; 15; 17; 18; 20; 24; 28; 31; 39; 40; 42; 47; 50; 57; ], [(mk_real_int64 390L); (mk_real_int64 1145L); (mk_real_int64 872L); (mk_real_int64 14L); (mk_real_int64 81L); (mk_real_int64 14L); (mk_real_int64 183L); (mk_real_int64 925L); (mk_real_int64 580L); (mk_real_int64 155L); (mk_real_int64 99L); (mk_real_int64 140L); (mk_real_int64 645L); (mk_real_int64 313L); (mk_real_int64 356L); ]);\r
("y8_def_neg", [5; ], [(mk_real_int64 1457L); ]);\r
("RHA", [8; 9; 10; 11; 14; 17; 18; 19; 20; 21; 22; 23; 24; 28; 29; 30; 33; 34; 35; 37; 38; 40; 41; 42; 43; 44; 45; 46; 47; 48; 49; 50; 51; 52; 53; 55; 56; 57; 58; 59; ], [(mk_real_int64 284L); (mk_real_int64 1356L); (mk_real_int64 1957L); (mk_real_int64 601L); (mk_real_int64 601L); (mk_real_int64 2662L); (mk_real_int64 2662L); (mk_real_int64 2662L); (mk_real_int64 2662L); (mk_real_int64 2662L); (mk_real_int64 394L); (mk_real_int64 394L); (mk_real_int64 2097L); (mk_real_int64 288L); (mk_real_int64 1831L); (mk_real_int64 2218L); (mk_real_int64 2446L); (mk_real_int64 1554L); (mk_real_int64 1831L); (mk_real_int64 1554L); (mk_real_int64 944L); (mk_real_int64 610L); (mk_real_int64 1353L); (mk_real_int64 1006L); (mk_real_int64 2508L); (mk_real_int64 1417L); (mk_real_int64 1411L); (mk_real_int64 208L); (mk_real_int64 2582L); (mk_real_int64 2073L); (mk_real_int64 3251L); (mk_real_int64 2650L); (mk_real_int64 1377L); (mk_real_int64 2396L); (mk_real_int64 692L); (mk_real_int64 2274L); (mk_real_int64 1141L); (mk_real_int64 5182L); (mk_real_int64 6270L); (mk_real_int64 5383L); ]);\r
("RHB", [7; ], [(mk_real_int64 892L); ]);\r
("ineq105", [1; 8; 11; ], [(mk_real_int64 32L); (mk_real_int64 1831L); (mk_real_int64 651L); ]);\r
("ineq106", [0; 14; 17; 19; 20; 22; 29; 32; 34; 36; 39; 42; ], [(mk_real_int64 1072L); (mk_real_int64 565L); (mk_real_int64 1482L); (mk_real_int64 615L); (mk_real_int64 327L); (mk_real_int64 228L); (mk_real_int64 149L); (mk_real_int64 521L); (mk_real_int64 1773L); (mk_real_int64 6L); (mk_real_int64 448L); (mk_real_int64 1342L); ]);\r
("ineq107", [5; 7; 9; 10; 12; 23; 24; 28; ], [(mk_real_int64 1971L); (mk_real_int64 205L); (mk_real_int64 89L); (mk_real_int64 536L); (mk_real_int64 89L); (mk_real_int64 3393L); (mk_real_int64 1908L); (mk_real_int64 651L); ]);\r
("ineq108", [4; 19; 35; 44; ], [(mk_real_int64 1227L); (mk_real_int64 1891L); (mk_real_int64 47L); (mk_real_int64 369L); ]);\r
("ineq109", [5; 8; 29; 37; 39; 44; ], [(mk_real_int64 1227L); (mk_real_int64 2993L); (mk_real_int64 293L); (mk_real_int64 101L); (mk_real_int64 355L); (mk_real_int64 293L); ]);\r
("ineq110", [2; 30; 35; 45; ], [(mk_real_int64 1356L); (mk_real_int64 713L); (mk_real_int64 707L); (mk_real_int64 5090L); ]);\r
("ineq111", [2; 5; 7; 16; 20; 23; 24; 27; 35; 38; 43; ], [(mk_real_int64 995L); (mk_real_int64 9935L); (mk_real_int64 6729L); (mk_real_int64 1468L); (mk_real_int64 8350L); (mk_real_int64 512L); (mk_real_int64 144L); (mk_real_int64 1244L); (mk_real_int64 4191L); (mk_real_int64 2503L); (mk_real_int64 3041L); ]);\r
("ineq112", [24; ], [(mk_real_int64 2928L); ]);\r
("ineq113", [2; 45; ], [(mk_real_int64 4738L); (mk_real_int64 1165L); ]);\r
("ineq114", [0; 6; 8; 11; 13; 16; 20; 21; 22; 25; 29; 31; 34; 36; 37; 39; 41; 43; 44; 46; ], [(mk_real_int64 2846L); (mk_real_int64 2820L); (mk_real_int64 386L); (mk_real_int64 7273L); (mk_real_int64 7273L); (mk_real_int64 6371L); (mk_real_int64 970L); (mk_real_int64 2925L); (mk_real_int64 4052L); (mk_real_int64 4417L); (mk_real_int64 7189L); (mk_real_int64 7427L); (mk_real_int64 3763L); (mk_real_int64 2348L); (mk_real_int64 2434L); (mk_real_int64 1642L); (mk_real_int64 1045L); (mk_real_int64 2976L); (mk_real_int64 1073L); (mk_real_int64 1885L); ]);\r
("ineq119", [2; 7; 9; ], [(mk_real_int64 7059L); (mk_real_int64 5746L); (mk_real_int64 7489L); ]);\r
("ineq120", [0; 1; 4; 6; ], [(mk_real_int64 421L); (mk_real_int64 2455L); (mk_real_int64 421L); (mk_real_int64 3768L); ]);\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; ], [(mk_real_int64 46550L); (mk_real_int64 46550L); (mk_real_int64 46550L); (mk_real_int64 46550L); (mk_real_int64 35530L); (mk_real_int64 41228L); (mk_real_int64 46550L); (mk_real_int64 49938L); (mk_real_int64 46550L); (mk_real_int64 51132L); (mk_real_int64 37858L); (mk_real_int64 45760L); (mk_real_int64 42556L); ]);\r
];;\r
\r
(*************************)\r
\r
let variable_bounds = [\r
("azim_lo", [0; 4; 6; 7; 8; 10; 14; 16; 19; 21; 30; 48; 49; 51; 55; ], [(mk_real_int64 1767L); (mk_real_int64 1767L); (mk_real_int64 4936L); (mk_real_int64 3920L); (mk_real_int64 4040L); (mk_real_int64 1420L); (mk_real_int64 6800L); (mk_real_int64 3640L); (mk_real_int64 1020L); (mk_real_int64 1020L); (mk_real_int64 4480L); (mk_real_int64 1520L); (mk_real_int64 3160L); (mk_real_int64 1080L); (mk_real_int64 240L); ]);\r
("azim_hi", [1; 2; 24; 28; 29; 32; 33; 36; 41; 43; 46; 53; 56; 57; 58; ], [(mk_real_int64 1715L); (mk_real_int64 2730L); (mk_real_int64 2460L); (mk_real_int64 2200L); (mk_real_int64 500L); (mk_real_int64 5040L); (mk_real_int64 420L); (mk_real_int64 4830L); (mk_real_int64 3140L); (mk_real_int64 3020L); (mk_real_int64 6380L); (mk_real_int64 11700L); (mk_real_int64 6980L); (mk_real_int64 2650L); (mk_real_int64 100L); ]);\r
("rhazim_lo", [10; 11; 14; 47; 48; 49; ], [(mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); ]);\r
("rhazim_hi", [52; ], [(mk_real_int64 10000L); ]);\r
("rho_lo", [0; 1; 2; 3; 4; 6; 8; 11; ], [(mk_real_int64 14080L); (mk_real_int64 14080L); (mk_real_int64 14080L); (mk_real_int64 14080L); (mk_real_int64 1152L); (mk_real_int64 14080L); (mk_real_int64 14080L); (mk_real_int64 5760L); ]);\r
("rho_hi", [5; 7; 9; 10; 12; ], [(mk_real_int64 9776L); (mk_real_int64 30784L); (mk_real_int64 1680L); (mk_real_int64 3024L); (mk_real_int64 2256L); ]);\r
("tau_lo", [16; 17; ], [(mk_real_int64 48530000L); (mk_real_int64 10000L); ]);\r
("tau_hi", [7; ], [(mk_real_int64 10000L); ]);\r
("y1_lo", [1; 8; 12; 13; 24; 25; 28; 38; 42; 44; 49; 54; 55; ], [(mk_real_int64 800L); (mk_real_int64 2000L); (mk_real_int64 3450L); (mk_real_int64 770L); (mk_real_int64 2400L); (mk_real_int64 2000L); (mk_real_int64 2000L); (mk_real_int64 650L); (mk_real_int64 600L); (mk_real_int64 6000L); (mk_real_int64 2510L); (mk_real_int64 2000L); (mk_real_int64 3800L); ]);\r
("y1_hi", [10; 15; 16; 17; 20; 27; 30; 31; 32; 35; 39; 40; 41; 46; 47; 48; 50; 51; 56; 57; ], [(mk_real_int64 1800L); (mk_real_int64 2800L); (mk_real_int64 570L); (mk_real_int64 5000L); (mk_real_int64 5000L); (mk_real_int64 6150L); (mk_real_int64 2000L); (mk_real_int64 3400L); (mk_real_int64 800L); (mk_real_int64 2350L); (mk_real_int64 800L); (mk_real_int64 5000L); (mk_real_int64 3570L); (mk_real_int64 2000L); (mk_real_int64 2350L); (mk_real_int64 4000L); (mk_real_int64 4600L); (mk_real_int64 5950L); (mk_real_int64 420L); (mk_real_int64 2000L); ]);\r
("y2_lo", [1; 12; 13; 15; 18; 22; 24; 27; 28; 30; 38; 41; 42; 44; 49; 55; ], [(mk_real_int64 1360L); (mk_real_int64 4947L); (mk_real_int64 1690L); (mk_real_int64 3800L); (mk_real_int64 4720L); (mk_real_int64 3965L); (mk_real_int64 2400L); (mk_real_int64 666L); (mk_real_int64 47L); (mk_real_int64 308L); (mk_real_int64 2980L); (mk_real_int64 219L); (mk_real_int64 600L); (mk_real_int64 4081L); (mk_real_int64 2510L); (mk_real_int64 3800L); ]);\r
("y2_hi", [8; 10; 16; 17; 20; 25; 31; 32; 35; 39; 40; 46; 47; 48; 50; 51; 54; 56; 57; ], [(mk_real_int64 1008L); (mk_real_int64 1800L); (mk_real_int64 570L); (mk_real_int64 4720L); (mk_real_int64 4720L); (mk_real_int64 2998L); (mk_real_int64 1040L); (mk_real_int64 640L); (mk_real_int64 620L); (mk_real_int64 800L); (mk_real_int64 480L); (mk_real_int64 1947L); (mk_real_int64 3833L); (mk_real_int64 1834L); (mk_real_int64 4600L); (mk_real_int64 4222L); (mk_real_int64 3538L); (mk_real_int64 361L); (mk_real_int64 2000L); ]);\r
("y3_lo", [1; 12; 13; 15; 18; 22; 24; 27; 28; 30; 38; 41; 42; 44; 49; 55; ], [(mk_real_int64 1360L); (mk_real_int64 4947L); (mk_real_int64 1690L); (mk_real_int64 3800L); (mk_real_int64 4720L); (mk_real_int64 3965L); (mk_real_int64 2400L); (mk_real_int64 666L); (mk_real_int64 47L); (mk_real_int64 308L); (mk_real_int64 2980L); (mk_real_int64 219L); (mk_real_int64 600L); (mk_real_int64 4081L); (mk_real_int64 2510L); (mk_real_int64 3800L); ]);\r
("y3_hi", [8; 10; 16; 17; 20; 25; 31; 32; 35; 39; 40; 46; 47; 48; 50; 51; 54; 56; 57; ], [(mk_real_int64 1008L); (mk_real_int64 1800L); (mk_real_int64 570L); (mk_real_int64 4720L); (mk_real_int64 4720L); (mk_real_int64 2998L); (mk_real_int64 1040L); (mk_real_int64 640L); (mk_real_int64 620L); (mk_real_int64 800L); (mk_real_int64 480L); (mk_real_int64 1947L); (mk_real_int64 3833L); (mk_real_int64 1834L); (mk_real_int64 4600L); (mk_real_int64 4222L); (mk_real_int64 3538L); (mk_real_int64 361L); (mk_real_int64 2000L); ]);\r
("y4_hi", [4; 5; 7; 8; 10; 19; 20; 23; 28; 30; 32; 35; 38; 42; 45; ], [(mk_real_int64 5050L); (mk_real_int64 2744L); (mk_real_int64 3400L); (mk_real_int64 3376L); (mk_real_int64 3280L); (mk_real_int64 3900L); (mk_real_int64 2550L); (mk_real_int64 7890L); (mk_real_int64 2230L); (mk_real_int64 2520L); (mk_real_int64 1150L); (mk_real_int64 3580L); (mk_real_int64 1250L); (mk_real_int64 7300L); (mk_real_int64 3600L); ]);\r
("y4_lo", [0; 2; 9; 12; 14; 16; 17; 22; 24; 27; 29; 34; 36; 37; 39; 43; 44; ], [(mk_real_int64 3200L); (mk_real_int64 1510L); (mk_real_int64 2030L); (mk_real_int64 2030L); (mk_real_int64 250L); (mk_real_int64 5000L); (mk_real_int64 1700L); (mk_real_int64 1800L); (mk_real_int64 1160L); (mk_real_int64 5000L); (mk_real_int64 3674L); (mk_real_int64 5050L); (mk_real_int64 1100L); (mk_real_int64 3568L); (mk_real_int64 1440L); (mk_real_int64 1250L); (mk_real_int64 674L); ]);\r
("y5_hi", [8; 13; 16; 17; 20; 25; 28; 31; 35; 40; 42; 46; 48; 50; 54; 57; ], [(mk_real_int64 1008L); (mk_real_int64 994L); (mk_real_int64 3376L); (mk_real_int64 4720L); (mk_real_int64 4720L); (mk_real_int64 2998L); (mk_real_int64 2453L); (mk_real_int64 2640L); (mk_real_int64 620L); (mk_real_int64 480L); (mk_real_int64 2520L); (mk_real_int64 1947L); (mk_real_int64 1834L); (mk_real_int64 1250L); (mk_real_int64 3538L); (mk_real_int64 3600L); ]);\r
("y5_lo", [1; 10; 12; 15; 18; 22; 24; 27; 30; 32; 38; 39; 41; 44; 47; 49; 51; 55; 56; ], [(mk_real_int64 1360L); (mk_real_int64 1510L); (mk_real_int64 4947L); (mk_real_int64 2850L); (mk_real_int64 4720L); (mk_real_int64 3965L); (mk_real_int64 5000L); (mk_real_int64 666L); (mk_real_int64 308L); (mk_real_int64 160L); (mk_real_int64 2980L); (mk_real_int64 5000L); (mk_real_int64 813L); (mk_real_int64 4081L); (mk_real_int64 3437L); (mk_real_int64 3568L); (mk_real_int64 2368L); (mk_real_int64 1250L); (mk_real_int64 233L); ]);\r
("y6_hi", [8; 13; 16; 17; 20; 25; 28; 31; 35; 40; 42; 46; 50; 54; 57; ], [(mk_real_int64 1008L); (mk_real_int64 994L); (mk_real_int64 3376L); (mk_real_int64 4720L); (mk_real_int64 4720L); (mk_real_int64 2998L); (mk_real_int64 2453L); (mk_real_int64 2640L); (mk_real_int64 620L); (mk_real_int64 480L); (mk_real_int64 2520L); (mk_real_int64 1947L); (mk_real_int64 1250L); (mk_real_int64 3538L); (mk_real_int64 3600L); ]);\r
("y6_lo", [1; 10; 12; 14; 15; 18; 22; 24; 27; 30; 32; 34; 38; 39; 41; 44; 47; 48; 49; 51; 55; 56; 57; ], [(mk_real_int64 1360L); (mk_real_int64 1510L); (mk_real_int64 6984947L); (mk_real_int64 18900000L); (mk_real_int64 2850L); (mk_real_int64 4720L); (mk_real_int64 3965L); (mk_real_int64 5000L); (mk_real_int64 666L); (mk_real_int64 308L); (mk_real_int64 8050160L); (mk_real_int64 3080000L); (mk_real_int64 2980L); (mk_real_int64 5000L); (mk_real_int64 813L); (mk_real_int64 4081L); (mk_real_int64 3437L); (mk_real_int64 21378166L); (mk_real_int64 3568L); (mk_real_int64 2368L); (mk_real_int64 7931250L); (mk_real_int64 233L); (mk_real_int64 6420000L); ]);\r
("y8_hi", [5; ], [(mk_real_int64 14570000L); ]);\r
("ye_hi", [11; 18; 21; 39; 40; 41; 48; 49; ], [(mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); ]);\r
("ye_lo", [6; 13; 16; 19; 21; 29; 42; 56; ], [(mk_real_int64 1060000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 9240000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 6610000L); ]);\r
("yn_lo", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; ], [(mk_real_int64 3626L); (mk_real_int64 3626L); (mk_real_int64 13626L); (mk_real_int64 3626L); (mk_real_int64 7890L); (mk_real_int64 6900L); (mk_real_int64 13626L); (mk_real_int64 3473L); (mk_real_int64 13626L); (mk_real_int64 694L); (mk_real_int64 18520L); (mk_real_int64 2244L); ]);\r
("yn_hi", [12; ], [(mk_real_int64 10540L); ]);\r
];;\r
let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
end;;\r
\r
concl (Test_case.result)\r