Update from HH

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

needs "nobranching_lp.hl";;
\r
module Test_case = struct\r
let hypermap_string = "75655754509 17 6 0 1 2 3 4 5 3 0 5 6 3 6 5 4 3 6 4 7 4 7 4 8 9 3 8 4 3 3 8 3 10 3 10 3 2 3 10 2 1 3 10 1 11 3 11 1 0 4 11 0 12 9 3 12 0 6 3 11 9 8 3 8 10 11 3 12 6 7 3 7 9 12 ";;\r
let precision = 3;;\r
(***************)\r
(* Constraints *)\r
(***************)\r
let constraints = [\r
("azim_sum_neg", [0; 3; 7; 9; 10; 12; ], [(mk_real_int64 249L); (mk_real_int64 600L); (mk_real_int64 58L); (mk_real_int64 302L); (mk_real_int64 327L); (mk_real_int64 327L); ]);\r
("azim_sum", [6; 8; ], [(mk_real_int64 160L); (mk_real_int64 160L); ]);\r
("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 849L); (mk_real_int64 1009L); (mk_real_int64 884L); (mk_real_int64 740L); (mk_real_int64 884L); (mk_real_int64 1009L); (mk_real_int64 1009L); (mk_real_int64 740L); (mk_real_int64 1009L); (mk_real_int64 955L); (mk_real_int64 1009L); (mk_real_int64 1009L); (mk_real_int64 1009L); ]);\r
("sol_sum3_neg", [4; 7; 11; ], [(mk_real_int64 10L); (mk_real_int64 10L); (mk_real_int64 499L); ]);\r
("sol_sum3", [5; 6; 12; ], [(mk_real_int64 189L); (mk_real_int64 189L); (mk_real_int64 311L); ]);\r
("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 653L); (mk_real_int64 653L); (mk_real_int64 653L); (mk_real_int64 884L); (mk_real_int64 672L); (mk_real_int64 740L); (mk_real_int64 740L); (mk_real_int64 672L); (mk_real_int64 884L); (mk_real_int64 653L); (mk_real_int64 939L); (mk_real_int64 670L); (mk_real_int64 871L); (mk_real_int64 682L); ]);\r
("tau_sum4_neg", [0; 1; ], [(mk_real_int64 1009L); (mk_real_int64 1009L); ]);\r
("tau_sum6_neg", [0; ], [(mk_real_int64 884L); ]);\r
("ln_def_neg", [1; 5; 6; 8; 9; 10; 11; 12; ], [(mk_real_int64 112L); (mk_real_int64 112L); (mk_real_int64 112L); (mk_real_int64 112L); (mk_real_int64 53L); (mk_real_int64 112L); (mk_real_int64 112L); (mk_real_int64 112L); ]);\r
("ln_def", [0; 2; 3; 4; 7; ], [(mk_real_int64 64L); (mk_real_int64 26L); (mk_real_int64 184L); (mk_real_int64 26L); (mk_real_int64 184L); ]);\r
("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 5333L); (mk_real_int64 6339L); (mk_real_int64 5551L); (mk_real_int64 4648L); (mk_real_int64 5551L); (mk_real_int64 6339L); (mk_real_int64 6339L); (mk_real_int64 4648L); (mk_real_int64 6339L); (mk_real_int64 6001L); (mk_real_int64 6339L); (mk_real_int64 6339L); (mk_real_int64 6339L); ]);\r
("edge_sym", [0; 3; 4; 5; 8; 11; 24; 30; 32; 33; 52; ], [(mk_real_int64 50L); (mk_real_int64 50L); (mk_real_int64 19L); (mk_real_int64 50L); (mk_real_int64 31L); (mk_real_int64 31L); (mk_real_int64 132L); (mk_real_int64 379L); (mk_real_int64 132L); (mk_real_int64 132L); (mk_real_int64 128L); ]);\r
("edge_sym_neg", [7; 21; 23; 27; 46; ], [(mk_real_int64 19L); (mk_real_int64 132L); (mk_real_int64 379L); (mk_real_int64 2L); (mk_real_int64 74L); ]);\r
("y1_def_neg", [0; 4; 8; 12; 14; 19; 20; 21; 22; 23; 26; 30; 31; 33; 34; 35; 36; 41; 42; 45; 50; 51; 52; 54; 55; ], [(mk_real_int64 39L); (mk_real_int64 39L); (mk_real_int64 15L); (mk_real_int64 15L); (mk_real_int64 17L); (mk_real_int64 19L); (mk_real_int64 75L); (mk_real_int64 91L); (mk_real_int64 238L); (mk_real_int64 59L); (mk_real_int64 28L); (mk_real_int64 28L); (mk_real_int64 59L); (mk_real_int64 228L); (mk_real_int64 29L); (mk_real_int64 91L); (mk_real_int64 75L); (mk_real_int64 17L); (mk_real_int64 15L); (mk_real_int64 79L); (mk_real_int64 73L); (mk_real_int64 88L); (mk_real_int64 120L); (mk_real_int64 73L); (mk_real_int64 64L); ]);\r
("y1_def", [7; 10; 27; 29; 47; 48; ], [(mk_real_int64 27L); (mk_real_int64 11L); (mk_real_int64 206L); (mk_real_int64 206L); (mk_real_int64 190L); (mk_real_int64 111L); ]);\r
("y2_def", [0; 4; 14; 19; 20; 22; 33; 34; 36; 41; 47; 50; 54; ], [(mk_real_int64 50L); (mk_real_int64 50L); (mk_real_int64 11L); (mk_real_int64 17L); (mk_real_int64 46L); (mk_real_int64 177L); (mk_real_int64 177L); (mk_real_int64 17L); (mk_real_int64 46L); (mk_real_int64 11L); (mk_real_int64 190L); (mk_real_int64 44L); (mk_real_int64 44L); ]);\r
("y2_def_neg", [7; 8; 10; 12; 21; 23; 26; 27; 29; 30; 31; 35; 42; 45; 48; 51; 52; 55; ], [(mk_real_int64 8L); (mk_real_int64 15L); (mk_real_int64 23L); (mk_real_int64 15L); (mk_real_int64 91L); (mk_real_int64 59L); (mk_real_int64 28L); (mk_real_int64 63L); (mk_real_int64 63L); (mk_real_int64 28L); (mk_real_int64 59L); (mk_real_int64 91L); (mk_real_int64 15L); (mk_real_int64 11L); (mk_real_int64 34L); (mk_real_int64 88L); (mk_real_int64 2L); (mk_real_int64 64L); ]);\r
("y3_def", [0; 4; 14; 19; 20; 22; 33; 34; 36; 41; 47; 50; 54; ], [(mk_real_int64 50L); (mk_real_int64 50L); (mk_real_int64 11L); (mk_real_int64 17L); (mk_real_int64 46L); (mk_real_int64 177L); (mk_real_int64 177L); (mk_real_int64 17L); (mk_real_int64 46L); (mk_real_int64 11L); (mk_real_int64 190L); (mk_real_int64 44L); (mk_real_int64 44L); ]);\r
("y3_def_neg", [7; 8; 10; 12; 21; 23; 26; 27; 29; 30; 31; 35; 42; 45; 48; 51; 52; 55; ], [(mk_real_int64 8L); (mk_real_int64 15L); (mk_real_int64 23L); (mk_real_int64 15L); (mk_real_int64 91L); (mk_real_int64 59L); (mk_real_int64 28L); (mk_real_int64 63L); (mk_real_int64 63L); (mk_real_int64 28L); (mk_real_int64 59L); (mk_real_int64 91L); (mk_real_int64 15L); (mk_real_int64 11L); (mk_real_int64 34L); (mk_real_int64 88L); (mk_real_int64 2L); (mk_real_int64 64L); ]);\r
("y4_def", [1; 4; 16; 17; 19; 20; 34; 38; ], [(mk_real_int64 41L); (mk_real_int64 31L); (mk_real_int64 61L); (mk_real_int64 318L); (mk_real_int64 318L); (mk_real_int64 61L); (mk_real_int64 171L); (mk_real_int64 17L); ]);\r
("y4_def_neg", [2; 6; 8; 9; 10; 11; 12; 13; 21; 23; 24; 25; 26; 27; 28; 31; 33; 36; 37; 40; 41; ], [(mk_real_int64 11L); (mk_real_int64 11L); (mk_real_int64 20L); (mk_real_int64 33L); (mk_real_int64 86L); (mk_real_int64 63L); (mk_real_int64 333L); (mk_real_int64 46L); (mk_real_int64 46L); (mk_real_int64 333L); (mk_real_int64 33L); (mk_real_int64 63L); (mk_real_int64 86L); (mk_real_int64 20L); (mk_real_int64 11L); (mk_real_int64 74L); (mk_real_int64 98L); (mk_real_int64 84L); (mk_real_int64 61L); (mk_real_int64 84L); (mk_real_int64 44L); ]);\r
("y5_def", [0; 4; 14; 19; 20; 22; 26; 30; 33; 34; 36; 41; 50; 52; 54; ], [(mk_real_int64 50L); (mk_real_int64 50L); (mk_real_int64 11L); (mk_real_int64 17L); (mk_real_int64 46L); (mk_real_int64 177L); (mk_real_int64 61L); (mk_real_int64 61L); (mk_real_int64 177L); (mk_real_int64 17L); (mk_real_int64 46L); (mk_real_int64 11L); (mk_real_int64 44L); (mk_real_int64 145L); (mk_real_int64 44L); ]);\r
("y5_def_neg", [7; 8; 10; 12; 21; 23; 27; 29; 31; 35; 42; 47; 48; 51; 55; ], [(mk_real_int64 8L); (mk_real_int64 11L); (mk_real_int64 19L); (mk_real_int64 11L); (mk_real_int64 63L); (mk_real_int64 46L); (mk_real_int64 63L); (mk_real_int64 63L); (mk_real_int64 46L); (mk_real_int64 63L); (mk_real_int64 11L); (mk_real_int64 98L); (mk_real_int64 34L); (mk_real_int64 61L); (mk_real_int64 44L); ]);\r
("y6_def", [0; 4; 9; 14; 19; 20; 22; 26; 28; 30; 33; 34; 36; 41; 50; 52; 54; ], [(mk_real_int64 50L); (mk_real_int64 50L); (mk_real_int64 37L); (mk_real_int64 11L); (mk_real_int64 17L); (mk_real_int64 46L); (mk_real_int64 177L); (mk_real_int64 63L); (mk_real_int64 3L); (mk_real_int64 61L); (mk_real_int64 177L); (mk_real_int64 17L); (mk_real_int64 46L); (mk_real_int64 11L); (mk_real_int64 44L); (mk_real_int64 145L); (mk_real_int64 44L); ]);\r
("y6_def_neg", [7; 8; 10; 12; 21; 23; 27; 29; 31; 35; 42; 47; 48; 51; 55; ], [(mk_real_int64 8L); (mk_real_int64 11L); (mk_real_int64 19L); (mk_real_int64 11L); (mk_real_int64 63L); (mk_real_int64 46L); (mk_real_int64 63L); (mk_real_int64 61L); (mk_real_int64 46L); (mk_real_int64 63L); (mk_real_int64 11L); (mk_real_int64 98L); (mk_real_int64 34L); (mk_real_int64 61L); (mk_real_int64 44L); ]);\r
("RHA", [0; 4; 6; 7; 8; 9; 10; 11; 12; 13; 14; 19; 23; 24; 26; 30; 31; 32; 33; 34; 41; 42; 43; 44; 46; 47; 48; 49; 50; 51; 52; 53; 54; 55; ], [(mk_real_int64 125L); (mk_real_int64 125L); (mk_real_int64 356L); (mk_real_int64 196L); (mk_real_int64 302L); (mk_real_int64 302L); (mk_real_int64 196L); (mk_real_int64 356L); (mk_real_int64 302L); (mk_real_int64 356L); (mk_real_int64 327L); (mk_real_int64 104L); (mk_real_int64 212L); (mk_real_int64 68L); (mk_real_int64 144L); (mk_real_int64 144L); (mk_real_int64 68L); (mk_real_int64 212L); (mk_real_int64 27L); (mk_real_int64 77L); (mk_real_int64 327L); (mk_real_int64 356L); (mk_real_int64 302L); (mk_real_int64 70L); (mk_real_int64 70L); (mk_real_int64 339L); (mk_real_int64 70L); (mk_real_int64 339L); (mk_real_int64 16L); (mk_real_int64 84L); (mk_real_int64 16L); (mk_real_int64 327L); (mk_real_int64 205L); (mk_real_int64 327L); ]);\r
("yy10", [4; 6; ], [(mk_real_int64 32L); (mk_real_int64 32L); ]);\r
("tau4", [0; 1; ], [(mk_real_int64 77L); (mk_real_int64 77L); ]);\r
("tau6", [0; ], [(mk_real_int64 884L); ]);\r
("ineq105", [0; 4; ], [(mk_real_int64 125L); (mk_real_int64 125L); ]);\r
("ineq106", [8; 9; 10; 12; 23; 24; 26; 27; 31; 36; 38; 40; ], [(mk_real_int64 29L); (mk_real_int64 21L); (mk_real_int64 125L); (mk_real_int64 337L); (mk_real_int64 310L); (mk_real_int64 48L); (mk_real_int64 125L); (mk_real_int64 29L); (mk_real_int64 70L); (mk_real_int64 122L); (mk_real_int64 122L); (mk_real_int64 122L); ]);\r
("ineq107", [1; 4; 17; 19; 34; ], [(mk_real_int64 53L); (mk_real_int64 53L); (mk_real_int64 412L); (mk_real_int64 412L); (mk_real_int64 222L); ]);\r
("ineq108", [9; 12; 23; ], [(mk_real_int64 27L); (mk_real_int64 150L); (mk_real_int64 176L); ]);\r
("ineq109", [16; 20; 38; ], [(mk_real_int64 189L); (mk_real_int64 189L); (mk_real_int64 311L); ]);\r
("ineq110", [13; 21; 33; ], [(mk_real_int64 10L); (mk_real_int64 10L); (mk_real_int64 499L); ]);\r
("ineq111", [2; 4; 6; 11; 13; 21; 25; 28; 31; 37; 41; ], [(mk_real_int64 85L); (mk_real_int64 85L); (mk_real_int64 85L); (mk_real_int64 505L); (mk_real_int64 349L); (mk_real_int64 349L); (mk_real_int64 505L); (mk_real_int64 85L); (mk_real_int64 204L); (mk_real_int64 490L); (mk_real_int64 355L); ]);\r
("ineq112", [34; ], [(mk_real_int64 370L); ]);\r
("ineq113", [34; ], [(mk_real_int64 300L); ]);\r
("ineq114", [0; 5; 7; 9; 13; 15; 16; 18; 20; 22; 24; 28; 30; 32; 37; 40; ], [(mk_real_int64 568L); (mk_real_int64 568L); (mk_real_int64 568L); (mk_real_int64 379L); (mk_real_int64 322L); (mk_real_int64 209L); (mk_real_int64 531L); (mk_real_int64 209L); (mk_real_int64 531L); (mk_real_int64 322L); (mk_real_int64 379L); (mk_real_int64 568L); (mk_real_int64 367L); (mk_real_int64 367L); (mk_real_int64 149L); (mk_real_int64 327L); ]);\r
("ineq119", [0; 6; ], [(mk_real_int64 721L); (mk_real_int64 721L); ]);\r
("ineq120", [2; 4; ], [(mk_real_int64 211L); (mk_real_int64 211L); ]);\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 2725L); (mk_real_int64 2675L); (mk_real_int64 2575L); (mk_real_int64 2600L); (mk_real_int64 2575L); (mk_real_int64 2675L); (mk_real_int64 2675L); (mk_real_int64 2600L); (mk_real_int64 2675L); (mk_real_int64 2825L); (mk_real_int64 2675L); (mk_real_int64 2675L); (mk_real_int64 2675L); ]);\r
];;\r
\r
(*************************)\r
\r
let variable_bounds = [\r
("azim_lo", [6; 11; 13; 17; 23; 25; 26; 27; 28; 29; 30; 32; 33; 37; 42; 44; 46; 48; 54; ], [(mk_real_int64 432L); (mk_real_int64 432L); (mk_real_int64 432L); (mk_real_int64 62L); (mk_real_int64 428L); (mk_real_int64 166L); (mk_real_int64 594L); (mk_real_int64 1000L); (mk_real_int64 166L); (mk_real_int64 1000L); (mk_real_int64 594L); (mk_real_int64 428L); (mk_real_int64 1000L); (mk_real_int64 62L); (mk_real_int64 432L); (mk_real_int64 258L); (mk_real_int64 258L); (mk_real_int64 290L); (mk_real_int64 298L); ]);\r
("azim_hi", [2; 5; 15; 19; 34; 39; 51; ], [(mk_real_int64 600000L); (mk_real_int64 249000L); (mk_real_int64 387L); (mk_real_int64 254L); (mk_real_int64 254L); (mk_real_int64 387L); (mk_real_int64 274L); ]);\r
("rhazim_hi", [2; 5; ], [(mk_real_int64 144000L); (mk_real_int64 35000L); ]);\r
("rho_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 2116L); (mk_real_int64 1556L); (mk_real_int64 4056L); (mk_real_int64 2160L); (mk_real_int64 4056L); (mk_real_int64 1556L); (mk_real_int64 1556L); (mk_real_int64 2160L); (mk_real_int64 1556L); (mk_real_int64 220L); (mk_real_int64 1556L); (mk_real_int64 1556L); (mk_real_int64 1556L); ]);\r
("tau_lo", [6; 9; 13; 15; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 233000L); ]);\r
("tau_hi", [15; ], [(mk_real_int64 1000L); ]);\r
("y1_lo", [0; 4; 7; 8; 12; 14; 23; 26; 30; 31; 41; 42; 47; 50; 51; 52; 54; ], [(mk_real_int64 375L); (mk_real_int64 375L); (mk_real_int64 500L); (mk_real_int64 300L); (mk_real_int64 300L); (mk_real_int64 400L); (mk_real_int64 20L); (mk_real_int64 539L); (mk_real_int64 539L); (mk_real_int64 20L); (mk_real_int64 400L); (mk_real_int64 300L); (mk_real_int64 380L); (mk_real_int64 200L); (mk_real_int64 200L); (mk_real_int64 161L); (mk_real_int64 200L); ]);\r
("y1_hi", [10; 19; 21; 22; 33; 34; 35; 45; 55; ], [(mk_real_int64 200L); (mk_real_int64 55L); (mk_real_int64 100L); (mk_real_int64 550L); (mk_real_int64 640L); (mk_real_int64 200L); (mk_real_int64 100L); (mk_real_int64 280L); (mk_real_int64 100L); ]);\r
("y2_hi", [0; 4; 19; 21; 22; 27; 29; 34; 35; 48; 50; 54; 55; ], [(mk_real_int64 250L); (mk_real_int64 250L); (mk_real_int64 472L); (mk_real_int64 100L); (mk_real_int64 268L); (mk_real_int64 376L); (mk_real_int64 376L); (mk_real_int64 472L); (mk_real_int64 100L); (mk_real_int64 256L); (mk_real_int64 408L); (mk_real_int64 408L); (mk_real_int64 100L); ]);\r
("y2_lo", [7; 8; 10; 12; 14; 20; 23; 26; 30; 31; 33; 36; 41; 42; 45; 47; 51; 52; ], [(mk_real_int64 56L); (mk_real_int64 300L); (mk_real_int64 356L); (mk_real_int64 300L); (mk_real_int64 444L); (mk_real_int64 500L); (mk_real_int64 20L); (mk_real_int64 539L); (mk_real_int64 539L); (mk_real_int64 20L); (mk_real_int64 96L); (mk_real_int64 500L); (mk_real_int64 444L); (mk_real_int64 300L); (mk_real_int64 240L); (mk_real_int64 380L); (mk_real_int64 200L); (mk_real_int64 553L); ]);\r
("y3_hi", [0; 4; 19; 21; 22; 27; 29; 34; 35; 48; 50; 54; 55; ], [(mk_real_int64 250L); (mk_real_int64 250L); (mk_real_int64 472L); (mk_real_int64 100L); (mk_real_int64 268L); (mk_real_int64 376L); (mk_real_int64 376L); (mk_real_int64 472L); (mk_real_int64 100L); (mk_real_int64 256L); (mk_real_int64 408L); (mk_real_int64 408L); (mk_real_int64 100L); ]);\r
("y3_lo", [7; 8; 10; 12; 14; 20; 23; 26; 30; 31; 33; 36; 41; 42; 45; 47; 51; 52; ], [(mk_real_int64 56L); (mk_real_int64 300L); (mk_real_int64 356L); (mk_real_int64 300L); (mk_real_int64 444L); (mk_real_int64 500L); (mk_real_int64 20L); (mk_real_int64 539L); (mk_real_int64 539L); (mk_real_int64 20L); (mk_real_int64 96L); (mk_real_int64 500L); (mk_real_int64 444L); (mk_real_int64 300L); (mk_real_int64 240L); (mk_real_int64 380L); (mk_real_int64 200L); (mk_real_int64 553L); ]);\r
("y4_hi", [2; 6; 8; 9; 10; 13; 16; 17; 19; 20; 21; 23; 24; 26; 27; 28; 31; 33; 34; 36; 38; 40; ], [(mk_real_int64 375L); (mk_real_int64 375L); (mk_real_int64 135L); (mk_real_int64 120L); (mk_real_int64 375L); (mk_real_int64 415L); (mk_real_int64 236L); (mk_real_int64 476L); (mk_real_int64 476L); (mk_real_int64 236L); (mk_real_int64 415L); (mk_real_int64 90L); (mk_real_int64 120L); (mk_real_int64 375L); (mk_real_int64 135L); (mk_real_int64 375L); (mk_real_int64 550L); (mk_real_int64 196L); (mk_real_int64 606L); (mk_real_int64 430L); (mk_real_int64 194L); (mk_real_int64 430L); ]);\r
("y4_lo", [1; 4; 11; 12; 25; 37; 41; ], [(mk_real_int64 31L); (mk_real_int64 656L); (mk_real_int64 125L); (mk_real_int64 595L); (mk_real_int64 125L); (mk_real_int64 250L); (mk_real_int64 375L); ]);\r
("y5_hi", [0; 4; 8; 10; 12; 19; 22; 23; 26; 27; 29; 30; 31; 34; 42; 47; 48; 50; 52; 54; ], [(mk_real_int64 250L); (mk_real_int64 250L); (mk_real_int64 375L); (mk_real_int64 319L); (mk_real_int64 375L); (mk_real_int64 472L); (mk_real_int64 268L); (mk_real_int64 415L); (mk_real_int64 236L); (mk_real_int64 376L); (mk_real_int64 376L); (mk_real_int64 236L); (mk_real_int64 415L); (mk_real_int64 472L); (mk_real_int64 375L); (mk_real_int64 196L); (mk_real_int64 256L); (mk_real_int64 408L); (mk_real_int64 172L); (mk_real_int64 408L); ]);\r
("y5_lo", [7; 14; 20; 21; 33; 35; 36; 41; 45; 51; 55; ], [(mk_real_int64 56L); (mk_real_int64 444L); (mk_real_int64 500L); (mk_real_int64 125L); (mk_real_int64 96L); (mk_real_int64 125L); (mk_real_int64 500L); (mk_real_int64 444L); (mk_real_int64 20L); (mk_real_int64 250L); (mk_real_int64 375L); ]);\r
("y6_hi", [0; 4; 8; 10; 12; 19; 22; 23; 26; 27; 29; 30; 31; 34; 42; 47; 48; 50; 52; 54; ], [(mk_real_int64 250L); (mk_real_int64 250L); (mk_real_int64 375L); (mk_real_int64 319L); (mk_real_int64 375L); (mk_real_int64 472L); (mk_real_int64 268L); (mk_real_int64 415L); (mk_real_int64 236L); (mk_real_int64 376L); (mk_real_int64 376L); (mk_real_int64 236L); (mk_real_int64 415L); (mk_real_int64 472L); (mk_real_int64 375L); (mk_real_int64 196L); (mk_real_int64 256L); (mk_real_int64 408L); (mk_real_int64 172L); (mk_real_int64 408L); ]);\r
("y6_lo", [7; 9; 14; 20; 21; 26; 28; 29; 33; 35; 36; 41; 45; 51; 55; ], [(mk_real_int64 56L); (mk_real_int64 37000L); (mk_real_int64 444L); (mk_real_int64 500L); (mk_real_int64 125L); (mk_real_int64 2000L); (mk_real_int64 3000L); (mk_real_int64 2000L); (mk_real_int64 96L); (mk_real_int64 125L); (mk_real_int64 500L); (mk_real_int64 444L); (mk_real_int64 20L); (mk_real_int64 250L); (mk_real_int64 375L); ]);\r
("ye_lo", [4; 6; 8; 9; 22; 24; 28; 32; 33; 49; ], [(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
("yn_hi", [1; 3; 5; 7; 9; 12; ], [(mk_real_int64 488L); (mk_real_int64 2168L); (mk_real_int64 488L); (mk_real_int64 1168L); (mk_real_int64 1972L); (mk_real_int64 488L); ]);\r
("yn_lo", [0; 2; 4; 6; 8; 10; 11; ], [(mk_real_int64 72L); (mk_real_int64 998L); (mk_real_int64 998L); (mk_real_int64 512L); (mk_real_int64 512L); (mk_real_int64 512L); (mk_real_int64 512L); ]);\r
];;\r
let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
end;;\r
\r
concl (Test_case.result)\r