Update from HH

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

needs "nobranching_lp.hl";;
\r
module Test_case = struct\r
let hypermap_string = "195482381558 18 4 0 1 2 3 4 0 3 4 5 3 4 3 6 3 6 3 7 3 7 3 2 3 7 2 8 3 8 2 1 3 8 1 9 3 9 1 0 3 9 0 10 3 10 0 5 3 10 5 11 3 11 5 4 3 11 4 6 4 10 11 6 12 3 12 6 7 3 9 10 12 4 12 7 8 9 ";;\r
let precision = 3;;\r
(***************)\r
(* Constraints *)\r
(***************)\r
let constraints = [\r
("azim_sum", [0; 3; 7; 8; 10; 12; ], [(mk_real_int64 408L); (mk_real_int64 406L); (mk_real_int64 101L); (mk_real_int64 101L); (mk_real_int64 101L); (mk_real_int64 101L); ]);\r
("azim_sum_neg", [1; 2; 4; 5; 6; 11; ], [(mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 344L); (mk_real_int64 344L); ]);\r
("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 882L); (mk_real_int64 934L); (mk_real_int64 934L); (mk_real_int64 884L); (mk_real_int64 934L); (mk_real_int64 934L); (mk_real_int64 1026L); (mk_real_int64 1026L); (mk_real_int64 1026L); (mk_real_int64 1026L); (mk_real_int64 1026L); (mk_real_int64 1026L); (mk_real_int64 1026L); ]);\r
("sol_sum3_neg", [0; 1; 2; 6; 7; 8; ], [(mk_real_int64 164L); (mk_real_int64 245L); (mk_real_int64 164L); (mk_real_int64 162L); (mk_real_int64 249L); (mk_real_int64 162L); ]);\r
("sol_sum3", [3; 4; 5; 9; 10; 11; ], [(mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 172L); ]);\r
("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 882L); (mk_real_int64 882L); (mk_real_int64 882L); (mk_real_int64 934L); (mk_real_int64 934L); (mk_real_int64 934L); (mk_real_int64 884L); (mk_real_int64 878L); (mk_real_int64 884L); (mk_real_int64 934L); (mk_real_int64 934L); (mk_real_int64 934L); (mk_real_int64 1026L); (mk_real_int64 1026L); ]);\r
("tau_sum4_neg", [0; 1; 2; 3; ], [(mk_real_int64 761L); (mk_real_int64 761L); (mk_real_int64 1026L); (mk_real_int64 1026L); ]);\r
("ln_def", [0; 3; ], [(mk_real_int64 27L); (mk_real_int64 26L); ]);\r
("ln_def_neg", [1; 2; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 29L); (mk_real_int64 29L); (mk_real_int64 29L); (mk_real_int64 29L); (mk_real_int64 132L); (mk_real_int64 132L); (mk_real_int64 132L); (mk_real_int64 132L); (mk_real_int64 132L); (mk_real_int64 132L); (mk_real_int64 132L); ]);\r
("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 5542L); (mk_real_int64 5866L); (mk_real_int64 5866L); (mk_real_int64 5553L); (mk_real_int64 5866L); (mk_real_int64 5866L); (mk_real_int64 6449L); (mk_real_int64 6449L); (mk_real_int64 6449L); (mk_real_int64 6449L); (mk_real_int64 6449L); (mk_real_int64 6449L); (mk_real_int64 6449L); ]);\r
("edge_sym", [0; 2; 3; 5; 7; 9; 24; 28; ], [(mk_real_int64 97L); (mk_real_int64 96L); (mk_real_int64 193L); (mk_real_int64 96L); (mk_real_int64 97L); (mk_real_int64 126L); (mk_real_int64 73L); (mk_real_int64 126L); ]);\r
("edge_sym_neg", [10; 12; 13; 16; 22; 30; 31; 34; 40; ], [(mk_real_int64 73L); (mk_real_int64 126L); (mk_real_int64 126L); (mk_real_int64 73L); (mk_real_int64 73L); (mk_real_int64 126L); (mk_real_int64 126L); (mk_real_int64 73L); (mk_real_int64 73L); ]);\r
("y1_def_neg", [0; 3; 4; 5; 10; 12; 19; 22; 24; 26; 30; 36; 39; 40; 42; 43; 50; 51; ], [(mk_real_int64 76L); (mk_real_int64 75L); (mk_real_int64 76L); (mk_real_int64 75L); (mk_real_int64 13L); (mk_real_int64 19L); (mk_real_int64 49L); (mk_real_int64 194L); (mk_real_int64 89L); (mk_real_int64 14L); (mk_real_int64 112L); (mk_real_int64 63L); (mk_real_int64 168L); (mk_real_int64 26L); (mk_real_int64 63L); (mk_real_int64 26L); (mk_real_int64 127L); (mk_real_int64 127L); ]);\r
("y1_def", [8; 9; 14; 16; 20; 23; 27; 28; 31; 32; 34; 37; 38; 41; ], [(mk_real_int64 108L); (mk_real_int64 39L); (mk_real_int64 26L); (mk_real_int64 108L); (mk_real_int64 40L); (mk_real_int64 40L); (mk_real_int64 108L); (mk_real_int64 38L); (mk_real_int64 95L); (mk_real_int64 24L); (mk_real_int64 108L); (mk_real_int64 14L); (mk_real_int64 40L); (mk_real_int64 40L); ]);\r
("y2_def", [0; 3; 4; 5; 9; 10; 14; 26; 28; 31; 32; ], [(mk_real_int64 97L); (mk_real_int64 96L); (mk_real_int64 97L); (mk_real_int64 96L); (mk_real_int64 39L); (mk_real_int64 8L); (mk_real_int64 47L); (mk_real_int64 8L); (mk_real_int64 38L); (mk_real_int64 95L); (mk_real_int64 46L); ]);\r
("y2_def_neg", [8; 12; 16; 19; 20; 22; 23; 24; 27; 30; 34; 36; 37; 38; 39; 40; 41; 42; 43; 50; 51; ], [(mk_real_int64 33L); (mk_real_int64 19L); (mk_real_int64 33L); (mk_real_int64 101L); (mk_real_int64 12L); (mk_real_int64 194L); (mk_real_int64 12L); (mk_real_int64 89L); (mk_real_int64 33L); (mk_real_int64 112L); (mk_real_int64 33L); (mk_real_int64 63L); (mk_real_int64 38L); (mk_real_int64 12L); (mk_real_int64 168L); (mk_real_int64 26L); (mk_real_int64 12L); (mk_real_int64 63L); (mk_real_int64 26L); (mk_real_int64 127L); (mk_real_int64 127L); ]);\r
("y3_def", [0; 3; 4; 5; 9; 10; 14; 26; 28; 31; 32; ], [(mk_real_int64 97L); (mk_real_int64 96L); (mk_real_int64 97L); (mk_real_int64 96L); (mk_real_int64 39L); (mk_real_int64 8L); (mk_real_int64 47L); (mk_real_int64 8L); (mk_real_int64 38L); (mk_real_int64 95L); (mk_real_int64 46L); ]);\r
("y3_def_neg", [8; 12; 16; 19; 20; 22; 23; 24; 27; 30; 34; 36; 37; 38; 39; 40; 41; 42; 43; 50; 51; ], [(mk_real_int64 33L); (mk_real_int64 19L); (mk_real_int64 33L); (mk_real_int64 101L); (mk_real_int64 12L); (mk_real_int64 194L); (mk_real_int64 12L); (mk_real_int64 89L); (mk_real_int64 33L); (mk_real_int64 112L); (mk_real_int64 33L); (mk_real_int64 63L); (mk_real_int64 38L); (mk_real_int64 12L); (mk_real_int64 168L); (mk_real_int64 26L); (mk_real_int64 12L); (mk_real_int64 63L); (mk_real_int64 26L); (mk_real_int64 127L); (mk_real_int64 127L); ]);\r
("y4_def_neg", [1; 2; 4; 6; 14; 18; 20; 22; 23; 24; 28; 31; 34; 38; 39; ], [(mk_real_int64 48L); (mk_real_int64 15L); (mk_real_int64 126L); (mk_real_int64 63L); (mk_real_int64 61L); (mk_real_int64 16L); (mk_real_int64 49L); (mk_real_int64 77L); (mk_real_int64 49L); (mk_real_int64 64L); (mk_real_int64 44L); (mk_real_int64 117L); (mk_real_int64 44L); (mk_real_int64 88L); (mk_real_int64 88L); ]);\r
("y4_def", [0; 8; 11; 12; 15; 16; 19; 26; 29; 30; 32; 33; 35; ], [(mk_real_int64 166L); (mk_real_int64 166L); (mk_real_int64 73L); (mk_real_int64 61L); (mk_real_int64 61L); (mk_real_int64 12L); (mk_real_int64 167L); (mk_real_int64 167L); (mk_real_int64 117L); (mk_real_int64 61L); (mk_real_int64 56L); (mk_real_int64 61L); (mk_real_int64 56L); ]);\r
("y5_def", [0; 3; 4; 5; 10; 24; 26; 37; 40; 43; ], [(mk_real_int64 97L); (mk_real_int64 96L); (mk_real_int64 97L); (mk_real_int64 96L); (mk_real_int64 8L); (mk_real_int64 12L); (mk_real_int64 8L); (mk_real_int64 44L); (mk_real_int64 56L); (mk_real_int64 56L); ]);\r
("y5_def_neg", [8; 9; 12; 14; 16; 20; 22; 23; 27; 28; 30; 31; 32; 34; 36; 38; 39; 41; 42; 50; 51; ], [(mk_real_int64 33L); (mk_real_int64 48L); (mk_real_int64 126L); (mk_real_int64 40L); (mk_real_int64 33L); (mk_real_int64 12L); (mk_real_int64 61L); (mk_real_int64 12L); (mk_real_int64 33L); (mk_real_int64 49L); (mk_real_int64 77L); (mk_real_int64 49L); (mk_real_int64 40L); (mk_real_int64 33L); (mk_real_int64 44L); (mk_real_int64 12L); (mk_real_int64 117L); (mk_real_int64 12L); (mk_real_int64 44L); (mk_real_int64 88L); (mk_real_int64 88L); ]);\r
("y6_def", [0; 3; 4; 5; 10; 20; 23; 24; 26; 37; 38; 40; 41; 43; 48; 49; 51; 52; 53; ], [(mk_real_int64 97L); (mk_real_int64 96L); (mk_real_int64 97L); (mk_real_int64 96L); (mk_real_int64 8L); (mk_real_int64 61L); (mk_real_int64 61L); (mk_real_int64 12L); (mk_real_int64 8L); (mk_real_int64 44L); (mk_real_int64 61L); (mk_real_int64 56L); (mk_real_int64 61L); (mk_real_int64 56L); (mk_real_int64 88L); (mk_real_int64 214L); (mk_real_int64 126L); (mk_real_int64 88L); (mk_real_int64 88L); ]);\r
("y6_def_neg", [8; 9; 12; 14; 16; 22; 27; 28; 30; 31; 32; 34; 36; 39; 42; ], [(mk_real_int64 33L); (mk_real_int64 48L); (mk_real_int64 126L); (mk_real_int64 40L); (mk_real_int64 33L); (mk_real_int64 61L); (mk_real_int64 33L); (mk_real_int64 49L); (mk_real_int64 77L); (mk_real_int64 49L); (mk_real_int64 40L); (mk_real_int64 33L); (mk_real_int64 44L); (mk_real_int64 117L); (mk_real_int64 44L); ]);\r
("RHA", [0; 1; 2; 3; 4; 5; 6; 7; 8; 10; 11; 13; 14; 16; 17; 19; 20; 23; 25; 26; 27; 29; 30; 31; 32; 34; 35; 37; 38; 41; 43; ], [(mk_real_int64 122L); (mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 121L); (mk_real_int64 122L); (mk_real_int64 121L); (mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 52L); (mk_real_int64 122L); (mk_real_int64 144L); (mk_real_int64 144L); (mk_real_int64 122L); (mk_real_int64 52L); (mk_real_int64 93L); (mk_real_int64 93L); (mk_real_int64 93L); (mk_real_int64 93L); (mk_real_int64 93L); (mk_real_int64 120L); (mk_real_int64 50L); (mk_real_int64 148L); (mk_real_int64 5L); (mk_real_int64 148L); (mk_real_int64 120L); (mk_real_int64 50L); (mk_real_int64 93L); (mk_real_int64 93L); (mk_real_int64 93L); (mk_real_int64 93L); (mk_real_int64 93L); ]);\r
("yy10", [4; ], [(mk_real_int64 386L); ]);\r
("ineq105", [0; 3; 4; 5; ], [(mk_real_int64 241L); (mk_real_int64 239L); (mk_real_int64 241L); (mk_real_int64 239L); ]);\r
("ineq106", [2; 6; 18; 24; ], [(mk_real_int64 22L); (mk_real_int64 22L); (mk_real_int64 23L); (mk_real_int64 23L); ]);\r
("ineq107", [0; 8; 11; 12; 15; 19; 26; 29; 30; 33; ], [(mk_real_int64 215L); (mk_real_int64 215L); (mk_real_int64 79L); (mk_real_int64 79L); (mk_real_int64 79L); (mk_real_int64 216L); (mk_real_int64 216L); (mk_real_int64 79L); (mk_real_int64 79L); (mk_real_int64 79L); ]);\r
("ineq109", [11; 14; 16; 29; 32; 35; ], [(mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 172L); (mk_real_int64 172L); ]);\r
("ineq110", [1; 4; 6; 20; 23; 24; ], [(mk_real_int64 164L); (mk_real_int64 245L); (mk_real_int64 164L); (mk_real_int64 162L); (mk_real_int64 249L); (mk_real_int64 162L); ]);\r
("ineq111", [1; 4; 6; 11; 14; 16; 20; 22; 24; 28; 31; 34; 38; 39; ], [(mk_real_int64 130L); (mk_real_int64 623L); (mk_real_int64 130L); (mk_real_int64 349L); (mk_real_int64 934L); (mk_real_int64 349L); (mk_real_int64 134L); (mk_real_int64 620L); (mk_real_int64 134L); (mk_real_int64 349L); (mk_real_int64 934L); (mk_real_int64 349L); (mk_real_int64 703L); (mk_real_int64 703L); ]);\r
("ineq113", [0; 8; 19; 26; ], [(mk_real_int64 267L); (mk_real_int64 267L); (mk_real_int64 266L); (mk_real_int64 266L); ]);\r
("ineq114", [1; 2; 4; 6; 7; 9; 17; 18; 20; 22; 24; 25; 27; 35; 37; 38; 39; 40; ], [(mk_real_int64 390L); (mk_real_int64 96L); (mk_real_int64 259L); (mk_real_int64 96L); (mk_real_int64 390L); (mk_real_int64 585L); (mk_real_int64 585L); (mk_real_int64 94L); (mk_real_int64 389L); (mk_real_int64 259L); (mk_real_int64 94L); (mk_real_int64 389L); (mk_real_int64 585L); (mk_real_int64 585L); (mk_real_int64 162L); (mk_real_int64 162L); (mk_real_int64 162L); (mk_real_int64 162L); ]);\r
("ineq119", [9; 14; ], [(mk_real_int64 759L); (mk_real_int64 759L); ]);\r
("ineq120", [0; 3; 4; 5; 8; 10; 13; 15; ], [(mk_real_int64 379L); (mk_real_int64 382L); (mk_real_int64 379L); (mk_real_int64 382L); (mk_real_int64 134L); (mk_real_int64 134L); (mk_real_int64 134L); (mk_real_int64 134L); ]);\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 3150L); (mk_real_int64 2450L); (mk_real_int64 2450L); (mk_real_int64 2225L); (mk_real_int64 2450L); (mk_real_int64 2450L); (mk_real_int64 3425L); (mk_real_int64 3425L); (mk_real_int64 3425L); (mk_real_int64 3425L); (mk_real_int64 3425L); (mk_real_int64 3425L); (mk_real_int64 3425L); ]);\r
];;\r
\r
(*************************)\r
\r
let variable_bounds = [\r
("azim_hi", [0; 4; 9; 10; 14; 15; 17; 25; 30; 35; 43; 44; 45; 46; 49; 50; 51; 52; 55; 56; 57; ], [(mk_real_int64 282L); (mk_real_int64 282L); (mk_real_int64 140L); (mk_real_int64 1096L); (mk_real_int64 1096L); (mk_real_int64 140L); (mk_real_int64 210L); (mk_real_int64 210L); (mk_real_int64 134L); (mk_real_int64 210L); (mk_real_int64 210L); (mk_real_int64 572L); (mk_real_int64 173L); (mk_real_int64 572L); (mk_real_int64 412L); (mk_real_int64 412L); (mk_real_int64 412L); (mk_real_int64 412L); (mk_real_int64 572L); (mk_real_int64 173L); (mk_real_int64 572L); ]);\r
("azim_lo", [3; 5; 8; 12; 16; 26; 27; 28; 32; 33; 34; ], [(mk_real_int64 444L); (mk_real_int64 444L); (mk_real_int64 153L); (mk_real_int64 866L); (mk_real_int64 153L); (mk_real_int64 156L); (mk_real_int64 894L); (mk_real_int64 486L); (mk_real_int64 156L); (mk_real_int64 486L); (mk_real_int64 894L); ]);\r
("rhazim_lo", [0; 1; 2; 4; 6; 7; 30; ], [(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", [17; 19; 20; 23; 25; 26; 32; 35; 37; 38; 41; 43; ], [(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_hi", [0; 1; 2; 3; 4; 5; ], [(mk_real_int64 488L); (mk_real_int64 3256L); (mk_real_int64 3256L); (mk_real_int64 2056L); (mk_real_int64 3256L); (mk_real_int64 3256L); ]);\r
("rho_lo", [6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 1616L); (mk_real_int64 1616L); (mk_real_int64 1616L); (mk_real_int64 1616L); (mk_real_int64 1616L); (mk_real_int64 1616L); (mk_real_int64 1616L); ]);\r
("tau_lo", [8; 10; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("tau_hi", [2; 4; 9; 14; 15; 16; 17; ], [(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
("y1_hi", [0; 4; 24; 26; 30; 36; 40; 42; 43; 50; 51; ], [(mk_real_int64 85L); (mk_real_int64 85L); (mk_real_int64 208L); (mk_real_int64 200L); (mk_real_int64 400L); (mk_real_int64 180L); (mk_real_int64 28L); (mk_real_int64 180L); (mk_real_int64 28L); (mk_real_int64 460L); (mk_real_int64 460L); ]);\r
("y1_lo", [3; 5; 8; 9; 10; 12; 14; 16; 19; 20; 22; 23; 28; 31; 32; 37; 38; 39; 41; ], [(mk_real_int64 285L); (mk_real_int64 285L); (mk_real_int64 500L); (mk_real_int64 80L); (mk_real_int64 200L); (mk_real_int64 40L); (mk_real_int64 280L); (mk_real_int64 500L); (mk_real_int64 292L); (mk_real_int64 500L); (mk_real_int64 92L); (mk_real_int64 500L); (mk_real_int64 560L); (mk_real_int64 380L); (mk_real_int64 360L); (mk_real_int64 472L); (mk_real_int64 500L); (mk_real_int64 120L); (mk_real_int64 500L); ]);\r
("y2_lo", [0; 4; 9; 12; 14; 20; 22; 23; 28; 31; 32; 38; 39; 41; ], [(mk_real_int64 118L); (mk_real_int64 118L); (mk_real_int64 80L); (mk_real_int64 40L); (mk_real_int64 72L); (mk_real_int64 8L); (mk_real_int64 92L); (mk_real_int64 8L); (mk_real_int64 560L); (mk_real_int64 380L); (mk_real_int64 188L); (mk_real_int64 8L); (mk_real_int64 120L); (mk_real_int64 8L); ]);\r
("y2_hi", [3; 5; 8; 10; 16; 19; 24; 26; 27; 30; 34; 36; 37; 40; 42; 43; 50; 51; ], [(mk_real_int64 78L); (mk_real_int64 78L); (mk_real_int64 320L); (mk_real_int64 8L); (mk_real_int64 320L); (mk_real_int64 200L); (mk_real_int64 208L); (mk_real_int64 372L); (mk_real_int64 168L); (mk_real_int64 400L); (mk_real_int64 168L); (mk_real_int64 180L); (mk_real_int64 20L); (mk_real_int64 28L); (mk_real_int64 180L); (mk_real_int64 28L); (mk_real_int64 460L); (mk_real_int64 460L); ]);\r
("y3_lo", [0; 4; 9; 12; 14; 20; 22; 23; 28; 31; 32; 38; 39; 41; ], [(mk_real_int64 118L); (mk_real_int64 118L); (mk_real_int64 80L); (mk_real_int64 40L); (mk_real_int64 72L); (mk_real_int64 8L); (mk_real_int64 92L); (mk_real_int64 8L); (mk_real_int64 560L); (mk_real_int64 380L); (mk_real_int64 188L); (mk_real_int64 8L); (mk_real_int64 120L); (mk_real_int64 8L); ]);\r
("y3_hi", [3; 5; 8; 10; 16; 19; 24; 26; 27; 30; 34; 36; 37; 40; 42; 43; 50; 51; ], [(mk_real_int64 78L); (mk_real_int64 78L); (mk_real_int64 320L); (mk_real_int64 8L); (mk_real_int64 320L); (mk_real_int64 200L); (mk_real_int64 208L); (mk_real_int64 372L); (mk_real_int64 168L); (mk_real_int64 400L); (mk_real_int64 168L); (mk_real_int64 180L); (mk_real_int64 20L); (mk_real_int64 28L); (mk_real_int64 180L); (mk_real_int64 28L); (mk_real_int64 460L); (mk_real_int64 460L); ]);\r
("y4_hi", [0; 4; 8; 11; 12; 15; 16; 18; 20; 23; 28; 30; 31; 33; 34; 38; 39; ], [(mk_real_int64 195L); (mk_real_int64 105L); (mk_real_int64 195L); (mk_real_int64 170L); (mk_real_int64 67L); (mk_real_int64 67L); (mk_real_int64 103L); (mk_real_int64 245L); (mk_real_int64 498L); (mk_real_int64 196L); (mk_real_int64 375L); (mk_real_int64 67L); (mk_real_int64 250L); (mk_real_int64 67L); (mk_real_int64 375L); (mk_real_int64 125L); (mk_real_int64 125L); ]);\r
("y4_lo", [1; 2; 6; 14; 19; 22; 24; 26; 29; 32; 35; ], [(mk_real_int64 394L); (mk_real_int64 70L); (mk_real_int64 464L); (mk_real_int64 22L); (mk_real_int64 32L); (mk_real_int64 500L); (mk_real_int64 257L); (mk_real_int64 32L); (mk_real_int64 205L); (mk_real_int64 272L); (mk_real_int64 272L); ]);\r
("y5_lo", [0; 4; 9; 14; 20; 22; 23; 30; 32; 37; 38; 40; 41; 43; ], [(mk_real_int64 118L); (mk_real_int64 118L); (mk_real_int64 394L); (mk_real_int64 386L); (mk_real_int64 8L); (mk_real_int64 22L); (mk_real_int64 8L); (mk_real_int64 500L); (mk_real_int64 130L); (mk_real_int64 280L); (mk_real_int64 8L); (mk_real_int64 272L); (mk_real_int64 8L); (mk_real_int64 272L); ]);\r
("y5_hi", [3; 5; 8; 10; 12; 16; 19; 24; 26; 27; 28; 31; 34; 36; 39; 42; 50; 51; ], [(mk_real_int64 78L); (mk_real_int64 78L); (mk_real_int64 320L); (mk_real_int64 8L); (mk_real_int64 105L); (mk_real_int64 320L); (mk_real_int64 95L); (mk_real_int64 103L); (mk_real_int64 372L); (mk_real_int64 168L); (mk_real_int64 498L); (mk_real_int64 196L); (mk_real_int64 168L); (mk_real_int64 375L); (mk_real_int64 250L); (mk_real_int64 375L); (mk_real_int64 125L); (mk_real_int64 125L); ]);\r
("y6_lo", [0; 4; 9; 14; 20; 22; 23; 30; 32; 37; 38; 40; 41; 43; 48; 49; 50; 51; 52; 53; ], [(mk_real_int64 118L); (mk_real_int64 118L); (mk_real_int64 394L); (mk_real_int64 386L); (mk_real_int64 73008L); (mk_real_int64 22L); (mk_real_int64 73008L); (mk_real_int64 500L); (mk_real_int64 130L); (mk_real_int64 280L); (mk_real_int64 73008L); (mk_real_int64 272L); (mk_real_int64 73008L); (mk_real_int64 272L); (mk_real_int64 88000L); (mk_real_int64 214000L); (mk_real_int64 88000L); (mk_real_int64 214000L); (mk_real_int64 88000L); (mk_real_int64 88000L); ]);\r
("y6_hi", [3; 5; 8; 10; 12; 16; 19; 24; 26; 27; 28; 31; 34; 36; 39; 42; 50; 51; ], [(mk_real_int64 78L); (mk_real_int64 78L); (mk_real_int64 320L); (mk_real_int64 8L); (mk_real_int64 105L); (mk_real_int64 320L); (mk_real_int64 95L); (mk_real_int64 103L); (mk_real_int64 372L); (mk_real_int64 168L); (mk_real_int64 498L); (mk_real_int64 196L); (mk_real_int64 168L); (mk_real_int64 375L); (mk_real_int64 250L); (mk_real_int64 375L); (mk_real_int64 125L); (mk_real_int64 125L); ]);\r
("ye_hi", [32; ], [(mk_real_int64 1000L); ]);\r
("ye_lo", [26; 27; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("yn_lo", [1; 2; 3; 4; 5; 7; 8; 9; 10; 12; ], [(mk_real_int64 204L); (mk_real_int64 204L); (mk_real_int64 998L); (mk_real_int64 204L); (mk_real_int64 204L); (mk_real_int64 32L); (mk_real_int64 32L); (mk_real_int64 32L); (mk_real_int64 32L); (mk_real_int64 32L); ]);\r
("yn_hi", [0; 6; 11; ], [(mk_real_int64 1079L); (mk_real_int64 1968L); (mk_real_int64 1968L); ]);\r
];;\r
let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
end;;\r
\r
concl (Test_case.result)\r