Update from HH

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

needs "nobranching_lp.hl";;
\r
module Test_case = struct\r
let hypermap_string = "123040027899 25 4 0 1 2 3 3 0 3 4 3 4 3 5 3 5 3 6 3 6 3 2 3 6 2 7 3 7 2 8 3 8 2 1 3 8 1 9 3 9 1 10 3 10 1 0 3 10 0 11 3 11 0 4 3 11 4 5 3 11 5 12 3 12 5 6 3 12 6 7 3 12 7 13 3 13 7 8 3 13 8 9 3 13 9 14 3 14 9 10 3 14 10 11 3 14 11 12 3 12 13 14 ";;\r
let precision = 3;;\r
(***************)\r
(* Constraints *)\r
(***************)\r
let constraints = [\r
("azim_sum", [1; 2; 4; 5; 11; 12; 14; ], [(mk_real_int64 130L); (mk_real_int64 446L); (mk_real_int64 142L); (mk_real_int64 11L); (mk_real_int64 207L); (mk_real_int64 646L); (mk_real_int64 116L); ]);\r
("azim_sum_neg", [7; 8; 9; ], [(mk_real_int64 8L); (mk_real_int64 55L); (mk_real_int64 46L); ]);\r
("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 789L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1188L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); ]);\r
("sol_sum3", [5; 7; 17; 18; ], [(mk_real_int64 8L); (mk_real_int64 46L); (mk_real_int64 8L); (mk_real_int64 46L); ]);\r
("sol_sum3_neg", [13; 22; 23; ], [(mk_real_int64 48L); (mk_real_int64 116L); (mk_real_int64 3L); ]);\r
("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18; 19; 20; 21; 22; 23; ], [(mk_real_int64 910L); (mk_real_int64 910L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1188L); (mk_real_int64 1188L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 910L); (mk_real_int64 910L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1188L); (mk_real_int64 1188L); (mk_real_int64 1188L); (mk_real_int64 1190L); (mk_real_int64 1190L); (mk_real_int64 1190L); ]);\r
("tau_sum4_neg", [0; ], [(mk_real_int64 1190L); ]);\r
("ln_def_neg", [0; 1; 2; 3; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 312L); (mk_real_int64 312L); (mk_real_int64 312L); (mk_real_int64 312L); (mk_real_int64 312L); (mk_real_int64 312L); (mk_real_int64 312L); (mk_real_int64 312L); (mk_real_int64 310L); (mk_real_int64 312L); (mk_real_int64 312L); (mk_real_int64 312L); (mk_real_int64 312L); (mk_real_int64 312L); ]);\r
("ln_def", [4; ], [(mk_real_int64 130L); ]);\r
("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 7477L); (mk_real_int64 7477L); (mk_real_int64 7477L); (mk_real_int64 7477L); (mk_real_int64 4958L); (mk_real_int64 7477L); (mk_real_int64 7477L); (mk_real_int64 7477L); (mk_real_int64 7477L); (mk_real_int64 7465L); (mk_real_int64 7477L); (mk_real_int64 7477L); (mk_real_int64 7477L); (mk_real_int64 7477L); (mk_real_int64 7477L); ]);\r
("edge_sym_neg", [3; 5; 9; 11; 12; 15; 17; 18; 20; 21; 24; 27; 35; 36; 39; 48; 54; 57; 60; 62; 63; 69; 72; ], [(mk_real_int64 31L); (mk_real_int64 176L); (mk_real_int64 200L); (mk_real_int64 157L); (mk_real_int64 145L); (mk_real_int64 123L); (mk_real_int64 124L); (mk_real_int64 124L); (mk_real_int64 116L); (mk_real_int64 176L); (mk_real_int64 24L); (mk_real_int64 360L); (mk_real_int64 107L); (mk_real_int64 107L); (mk_real_int64 187L); (mk_real_int64 22L); (mk_real_int64 7L); (mk_real_int64 150L); (mk_real_int64 111L); (mk_real_int64 114L); (mk_real_int64 70L); (mk_real_int64 48L); (mk_real_int64 128L); ]);\r
("edge_sym", [6; 8; 26; 29; 30; 33; 42; 44; 45; 51; 53; 66; ], [(mk_real_int64 31L); (mk_real_int64 95L); (mk_real_int64 30L); (mk_real_int64 14L); (mk_real_int64 236L); (mk_real_int64 107L); (mk_real_int64 136L); (mk_real_int64 10L); (mk_real_int64 44L); (mk_real_int64 14L); (mk_real_int64 107L); (mk_real_int64 265L); ]);\r
("y1_def_neg", [4; 6; 8; 9; 10; 14; 16; 19; 20; 23; 25; 26; 29; 30; 31; 36; 37; 38; 40; 41; 42; 44; 45; 46; 47; 48; 49; 52; 54; 55; 56; 58; 59; 60; 61; 62; 63; 64; 65; 66; 67; 69; 71; 72; 73; 75; ], [(mk_real_int64 119L); (mk_real_int64 59L); (mk_real_int64 332L); (mk_real_int64 171L); (mk_real_int64 217L); (mk_real_int64 177L); (mk_real_int64 177L); (mk_real_int64 192L); (mk_real_int64 13L); (mk_real_int64 29L); (mk_real_int64 3L); (mk_real_int64 264L); (mk_real_int64 203L); (mk_real_int64 1L); (mk_real_int64 86L); (mk_real_int64 155L); (mk_real_int64 79L); (mk_real_int64 230L); (mk_real_int64 168L); (mk_real_int64 104L); (mk_real_int64 171L); (mk_real_int64 18L); (mk_real_int64 14L); (mk_real_int64 8L); (mk_real_int64 3L); (mk_real_int64 38L); (mk_real_int64 141L); (mk_real_int64 10L); (mk_real_int64 40L); (mk_real_int64 2L); (mk_real_int64 214L); (mk_real_int64 12L); (mk_real_int64 3L); (mk_real_int64 214L); (mk_real_int64 1L); (mk_real_int64 191L); (mk_real_int64 28L); (mk_real_int64 28L); (mk_real_int64 191L); (mk_real_int64 1L); (mk_real_int64 3L); (mk_real_int64 233L); (mk_real_int64 21L); (mk_real_int64 62L); (mk_real_int64 365L); (mk_real_int64 27L); ]);\r
("y1_def", [18; 21; 22; 28; 51; 53; 57; 70; 74; ], [(mk_real_int64 4L); (mk_real_int64 23L); (mk_real_int64 13L); (mk_real_int64 23L); (mk_real_int64 4L); (mk_real_int64 4L); (mk_real_int64 22L); (mk_real_int64 44L); (mk_real_int64 3L); ]);\r
("y2_def_neg", [6; 8; 10; 14; 16; 18; 19; 21; 22; 23; 25; 26; 28; 29; 31; 36; 41; 44; 48; 49; 51; 53; 54; 56; 57; 59; 60; 62; 65; 69; 72; ], [(mk_real_int64 59L); (mk_real_int64 62L); (mk_real_int64 210L); (mk_real_int64 177L); (mk_real_int64 177L); (mk_real_int64 1L); (mk_real_int64 192L); (mk_real_int64 7L); (mk_real_int64 4L); (mk_real_int64 29L); (mk_real_int64 8L); (mk_real_int64 44L); (mk_real_int64 7L); (mk_real_int64 68L); (mk_real_int64 86L); (mk_real_int64 155L); (mk_real_int64 104L); (mk_real_int64 42L); (mk_real_int64 38L); (mk_real_int64 12L); (mk_real_int64 1L); (mk_real_int64 1L); (mk_real_int64 40L); (mk_real_int64 214L); (mk_real_int64 8L); (mk_real_int64 8L); (mk_real_int64 214L); (mk_real_int64 221L); (mk_real_int64 221L); (mk_real_int64 109L); (mk_real_int64 62L); ]);\r
("y2_def", [4; 9; 20; 30; 37; 38; 40; 42; 45; 46; 47; 52; 55; 58; 61; 63; 64; 66; 67; 70; 71; 73; 74; 75; ], [(mk_real_int64 72L); (mk_real_int64 106L); (mk_real_int64 21L); (mk_real_int64 1L); (mk_real_int64 48L); (mk_real_int64 41L); (mk_real_int64 102L); (mk_real_int64 106L); (mk_real_int64 69L); (mk_real_int64 13L); (mk_real_int64 4L); (mk_real_int64 15L); (mk_real_int64 3L); (mk_real_int64 17L); (mk_real_int64 1L); (mk_real_int64 43L); (mk_real_int64 43L); (mk_real_int64 1L); (mk_real_int64 5L); (mk_real_int64 44L); (mk_real_int64 33L); (mk_real_int64 20L); (mk_real_int64 1L); (mk_real_int64 41L); ]);\r
("y3_def_neg", [6; 8; 10; 14; 16; 18; 19; 21; 22; 23; 25; 26; 28; 29; 31; 36; 41; 44; 48; 49; 51; 53; 54; 56; 57; 59; 60; 62; 65; 69; 72; ], [(mk_real_int64 59L); (mk_real_int64 62L); (mk_real_int64 210L); (mk_real_int64 177L); (mk_real_int64 177L); (mk_real_int64 1L); (mk_real_int64 192L); (mk_real_int64 7L); (mk_real_int64 4L); (mk_real_int64 29L); (mk_real_int64 8L); (mk_real_int64 44L); (mk_real_int64 7L); (mk_real_int64 68L); (mk_real_int64 86L); (mk_real_int64 155L); (mk_real_int64 104L); (mk_real_int64 42L); (mk_real_int64 38L); (mk_real_int64 12L); (mk_real_int64 1L); (mk_real_int64 1L); (mk_real_int64 40L); (mk_real_int64 214L); (mk_real_int64 8L); (mk_real_int64 8L); (mk_real_int64 214L); (mk_real_int64 221L); (mk_real_int64 221L); (mk_real_int64 109L); (mk_real_int64 62L); ]);\r
("y3_def", [4; 9; 20; 30; 37; 38; 40; 42; 45; 46; 47; 52; 55; 58; 61; 63; 64; 66; 67; 70; 71; 73; 74; 75; ], [(mk_real_int64 72L); (mk_real_int64 106L); (mk_real_int64 21L); (mk_real_int64 1L); (mk_real_int64 48L); (mk_real_int64 41L); (mk_real_int64 102L); (mk_real_int64 106L); (mk_real_int64 69L); (mk_real_int64 13L); (mk_real_int64 4L); (mk_real_int64 15L); (mk_real_int64 3L); (mk_real_int64 17L); (mk_real_int64 1L); (mk_real_int64 43L); (mk_real_int64 43L); (mk_real_int64 1L); (mk_real_int64 5L); (mk_real_int64 44L); (mk_real_int64 33L); (mk_real_int64 20L); (mk_real_int64 1L); (mk_real_int64 41L); ]);\r
("y4_def_neg", [0; 2; 4; 5; 6; 10; 12; 15; 16; 19; 22; 25; 26; 27; 32; 33; 34; 36; 37; 38; 41; 42; 43; 44; 45; 48; 50; 51; 52; 54; 56; 57; 58; 59; 60; 61; 62; 63; 65; 66; 67; 68; 69; 71; ], [(mk_real_int64 135L); (mk_real_int64 41L); (mk_real_int64 306L); (mk_real_int64 200L); (mk_real_int64 157L); (mk_real_int64 123L); (mk_real_int64 123L); (mk_real_int64 130L); (mk_real_int64 39L); (mk_real_int64 20L); (mk_real_int64 374L); (mk_real_int64 258L); (mk_real_int64 1L); (mk_real_int64 60L); (mk_real_int64 107L); (mk_real_int64 90L); (mk_real_int64 235L); (mk_real_int64 192L); (mk_real_int64 72L); (mk_real_int64 200L); (mk_real_int64 105L); (mk_real_int64 24L); (mk_real_int64 8L); (mk_real_int64 27L); (mk_real_int64 210L); (mk_real_int64 28L); (mk_real_int64 28L); (mk_real_int64 6L); (mk_real_int64 149L); (mk_real_int64 33L); (mk_real_int64 149L); (mk_real_int64 1L); (mk_real_int64 113L); (mk_real_int64 81L); (mk_real_int64 81L); (mk_real_int64 113L); (mk_real_int64 1L); (mk_real_int64 9L); (mk_real_int64 270L); (mk_real_int64 23L); (mk_real_int64 62L); (mk_real_int64 43L); (mk_real_int64 589L); (mk_real_int64 77L); ]);\r
("y4_def", [14; 17; 18; 21; 24; 40; 47; 49; 53; 55; 70; ], [(mk_real_int64 6L); (mk_real_int64 36L); (mk_real_int64 20L); (mk_real_int64 20L); (mk_real_int64 35L); (mk_real_int64 3L); (mk_real_int64 6L); (mk_real_int64 6L); (mk_real_int64 39L); (mk_real_int64 20L); (mk_real_int64 2L); ]);\r
("y5_def_neg", [0; 6; 8; 10; 14; 16; 18; 19; 21; 22; 23; 28; 29; 31; 36; 41; 44; 48; 51; 53; 54; 56; 57; 60; 62; 65; 69; 70; 72; 74; ], [(mk_real_int64 31L); (mk_real_int64 41L); (mk_real_int64 12L); (mk_real_int64 145L); (mk_real_int64 123L); (mk_real_int64 123L); (mk_real_int64 1L); (mk_real_int64 130L); (mk_real_int64 7L); (mk_real_int64 4L); (mk_real_int64 20L); (mk_real_int64 7L); (mk_real_int64 22L); (mk_real_int64 60L); (mk_real_int64 107L); (mk_real_int64 72L); (mk_real_int64 31L); (mk_real_int64 27L); (mk_real_int64 1L); (mk_real_int64 1L); (mk_real_int64 28L); (mk_real_int64 149L); (mk_real_int64 4L); (mk_real_int64 149L); (mk_real_int64 155L); (mk_real_int64 155L); (mk_real_int64 53L); (mk_real_int64 23L); (mk_real_int64 43L); (mk_real_int64 1L); ]);\r
("y5_def", [4; 9; 20; 25; 26; 30; 37; 38; 40; 42; 45; 46; 47; 49; 52; 55; 58; 59; 61; 63; 64; 66; 67; 71; 73; 75; ], [(mk_real_int64 72L); (mk_real_int64 106L); (mk_real_int64 21L); (mk_real_int64 14L); (mk_real_int64 10L); (mk_real_int64 1L); (mk_real_int64 48L); (mk_real_int64 59L); (mk_real_int64 102L); (mk_real_int64 106L); (mk_real_int64 41L); (mk_real_int64 13L); (mk_real_int64 4L); (mk_real_int64 16L); (mk_real_int64 15L); (mk_real_int64 3L); (mk_real_int64 17L); (mk_real_int64 14L); (mk_real_int64 1L); (mk_real_int64 43L); (mk_real_int64 43L); (mk_real_int64 1L); (mk_real_int64 5L); (mk_real_int64 33L); (mk_real_int64 85L); (mk_real_int64 41L); ]);\r
("y6_def_neg", [6; 8; 10; 18; 21; 23; 28; 29; 31; 36; 44; 48; 51; 53; 54; 57; 60; 62; 65; 69; 72; ], [(mk_real_int64 41L); (mk_real_int64 12L); (mk_real_int64 95L); (mk_real_int64 1L); (mk_real_int64 7L); (mk_real_int64 20L); (mk_real_int64 7L); (mk_real_int64 22L); (mk_real_int64 14L); (mk_real_int64 107L); (mk_real_int64 31L); (mk_real_int64 27L); (mk_real_int64 1L); (mk_real_int64 1L); (mk_real_int64 28L); (mk_real_int64 4L); (mk_real_int64 149L); (mk_real_int64 155L); (mk_real_int64 155L); (mk_real_int64 53L); (mk_real_int64 43L); ]);\r
("y6_def", [4; 7; 9; 13; 16; 19; 20; 22; 25; 26; 30; 32; 37; 38; 40; 41; 42; 45; 46; 47; 49; 50; 52; 55; 56; 58; 59; 61; 63; 64; 66; 67; 68; 70; 71; 73; 74; 75; ], [(mk_real_int64 72L); (mk_real_int64 388L); (mk_real_int64 106L); (mk_real_int64 279L); (mk_real_int64 117L); (mk_real_int64 67L); (mk_real_int64 21L); (mk_real_int64 136L); (mk_real_int64 14L); (mk_real_int64 10L); (mk_real_int64 501L); (mk_real_int64 60L); (mk_real_int64 48L); (mk_real_int64 59L); (mk_real_int64 459L); (mk_real_int64 286L); (mk_real_int64 106L); (mk_real_int64 41L); (mk_real_int64 13L); (mk_real_int64 195L); (mk_real_int64 16L); (mk_real_int64 335L); (mk_real_int64 15L); (mk_real_int64 3L); (mk_real_int64 186L); (mk_real_int64 285L); (mk_real_int64 541L); (mk_real_int64 347L); (mk_real_int64 43L); (mk_real_int64 271L); (mk_real_int64 1L); (mk_real_int64 5L); (mk_real_int64 169L); (mk_real_int64 58L); (mk_real_int64 33L); (mk_real_int64 85L); (mk_real_int64 618L); (mk_real_int64 41L); ]);\r
("y8_def_neg", [1; ], [(mk_real_int64 31L); ]);\r
("RHA", [4; 5; 25; 37; 59; ], [(mk_real_int64 83L); (mk_real_int64 280L); (mk_real_int64 2L); (mk_real_int64 149L); (mk_real_int64 2L); ]);\r
("RHB", [6; 7; 39; 41; ], [(mk_real_int64 120L); (mk_real_int64 120L); (mk_real_int64 120L); (mk_real_int64 120L); ]);\r
("yy10", [71; ], [(mk_real_int64 12L); ]);\r
("tau4", [0; ], [(mk_real_int64 430L); ]);\r
("ineq106", [0; 4; 5; 22; 25; 26; 33; 34; 36; 38; 54; 57; 59; 60; 62; ], [(mk_real_int64 198L); (mk_real_int64 280L); (mk_real_int64 280L); (mk_real_int64 2L); (mk_real_int64 2L); (mk_real_int64 2L); (mk_real_int64 132L); (mk_real_int64 280L); (mk_real_int64 280L); (mk_real_int64 280L); (mk_real_int64 2L); (mk_real_int64 2L); (mk_real_int64 2L); (mk_real_int64 2L); (mk_real_int64 2L); ]);\r
("ineq107", [14; 17; 18; 21; 24; 40; 47; 49; 53; 55; 58; 61; 70; ], [(mk_real_int64 8L); (mk_real_int64 47L); (mk_real_int64 26L); (mk_real_int64 7L); (mk_real_int64 46L); (mk_real_int64 37L); (mk_real_int64 8L); (mk_real_int64 8L); (mk_real_int64 47L); (mk_real_int64 7L); (mk_real_int64 46L); (mk_real_int64 46L); (mk_real_int64 3L); ]);\r
("ineq108", [5; 6; 16; 22; 25; 38; 41; 42; 43; 45; 48; 51; 54; 59; 60; 63; 65; 67; 69; 71; ], [(mk_real_int64 11L); (mk_real_int64 11L); (mk_real_int64 57L); (mk_real_int64 364L); (mk_real_int64 223L); (mk_real_int64 11L); (mk_real_int64 139L); (mk_real_int64 35L); (mk_real_int64 11L); (mk_real_int64 215L); (mk_real_int64 41L); (mk_real_int64 8L); (mk_real_int64 46L); (mk_real_int64 116L); (mk_real_int64 116L); (mk_real_int64 13L); (mk_real_int64 207L); (mk_real_int64 91L); (mk_real_int64 643L); (mk_real_int64 113L); ]);\r
("ineq109", [15; 21; 53; 55; ], [(mk_real_int64 8L); (mk_real_int64 46L); (mk_real_int64 8L); (mk_real_int64 46L); ]);\r
("ineq110", [41; 66; 70; ], [(mk_real_int64 48L); (mk_real_int64 116L); (mk_real_int64 3L); ]);\r
("ineq111", [2; 4; 6; 10; 12; 15; 19; 22; 25; 27; 32; 34; 37; 40; 44; 45; 50; 52; 56; 58; 61; 65; 68; 69; ], [(mk_real_int64 329L); (mk_real_int64 910L); (mk_real_int64 1190L); (mk_real_int64 983L); (mk_real_int64 983L); (mk_real_int64 1061L); (mk_real_int64 158L); (mk_real_int64 985L); (mk_real_int64 832L); (mk_real_int64 478L); (mk_real_int64 859L); (mk_real_int64 341L); (mk_real_int64 579L); (mk_real_int64 204L); (mk_real_int64 213L); (mk_real_int64 501L); (mk_real_int64 223L); (mk_real_int64 1190L); (mk_real_int64 1188L); (mk_real_int64 1188L); (mk_real_int64 1188L); (mk_real_int64 1026L); (mk_real_int64 344L); (mk_real_int64 1190L); ]);\r
("ineq113", [18; ], [(mk_real_int64 113L); ]);\r
("ineq114", [0; 1; 11; 13; 16; 19; 20; 22; 25; 28; 32; 33; 36; 39; 41; 42; 45; 48; 63; 68; ], [(mk_real_int64 132L); (mk_real_int64 448L); (mk_real_int64 207L); (mk_real_int64 207L); (mk_real_int64 129L); (mk_real_int64 207L); (mk_real_int64 712L); (mk_real_int64 203L); (mk_real_int64 356L); (mk_real_int64 712L); (mk_real_int64 331L); (mk_real_int64 569L); (mk_real_int64 331L); (mk_real_int64 254L); (mk_real_int64 732L); (mk_real_int64 977L); (mk_real_int64 689L); (mk_real_int64 967L); (mk_real_int64 164L); (mk_real_int64 847L); ]);\r
("ineq120", [1; 2; ], [(mk_real_int64 588L); (mk_real_int64 171L); ]);\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 3525L); (mk_real_int64 3525L); (mk_real_int64 3525L); (mk_real_int64 3525L); (mk_real_int64 2350L); (mk_real_int64 3525L); (mk_real_int64 3525L); (mk_real_int64 3525L); (mk_real_int64 3525L); (mk_real_int64 3625L); (mk_real_int64 3525L); (mk_real_int64 3525L); (mk_real_int64 3525L); (mk_real_int64 3525L); (mk_real_int64 3525L); ]);\r
];;\r
\r
(*************************)\r
\r
let variable_bounds = [\r
("azim_lo", [1; 2; 4; 6; 7; 15; 17; 20; 22; 23; 24; 26; 29; 32; 39; 41; 45; 67; ], [(mk_real_int64 296L); (mk_real_int64 382L); (mk_real_int64 368L); (mk_real_int64 880L); (mk_real_int64 880L); (mk_real_int64 418L); (mk_real_int64 418L); (mk_real_int64 246L); (mk_real_int64 267L); (mk_real_int64 418L); (mk_real_int64 288L); (mk_real_int64 922L); (mk_real_int64 144L); (mk_real_int64 288L); (mk_real_int64 880L); (mk_real_int64 880L); (mk_real_int64 768L); (mk_real_int64 336L); ]);\r
("azim_hi", [5; 36; 37; 40; 43; 46; 49; 52; 72; ], [(mk_real_int64 448L); (mk_real_int64 206L); (mk_real_int64 194L); (mk_real_int64 206L); (mk_real_int64 4L); (mk_real_int64 602L); (mk_real_int64 314L); (mk_real_int64 342L); (mk_real_int64 222L); ]);\r
("rhazim_hi", [4; 6; 7; 37; 39; 41; ], [(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; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 76L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 392L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 960L); ]);\r
("tau_lo", [0; 1; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("tau_hi", [23; ], [(mk_real_int64 1000L); ]);\r
("y1_hi", [4; 8; 9; 10; 14; 16; 21; 23; 36; 38; 42; 47; 49; 52; 55; 57; 60; 62; 65; 70; 72; 75; ], [(mk_real_int64 200L); (mk_real_int64 200L); (mk_real_int64 415L); (mk_real_int64 215L); (mk_real_int64 60L); (mk_real_int64 60L); (mk_real_int64 500L); (mk_real_int64 560L); (mk_real_int64 380L); (mk_real_int64 620L); (mk_real_int64 415L); (mk_real_int64 415L); (mk_real_int64 295L); (mk_real_int64 365L); (mk_real_int64 120L); (mk_real_int64 292L); (mk_real_int64 160L); (mk_real_int64 160L); (mk_real_int64 160L); (mk_real_int64 80L); (mk_real_int64 80L); (mk_real_int64 445L); ]);\r
("y1_lo", [6; 19; 20; 25; 26; 29; 30; 31; 37; 41; 44; 45; 46; 48; 54; 56; 58; 59; 61; 63; 64; 66; 67; 69; 71; 73; 74; ], [(mk_real_int64 220L); (mk_real_int64 188L); (mk_real_int64 395L); (mk_real_int64 446L); (mk_real_int64 40L); (mk_real_int64 365L); (mk_real_int64 200L); (mk_real_int64 40L); (mk_real_int64 200L); (mk_real_int64 220L); (mk_real_int64 220L); (mk_real_int64 425L); (mk_real_int64 225L); (mk_real_int64 340L); (mk_real_int64 140L); (mk_real_int64 200L); (mk_real_int64 10L); (mk_real_int64 446L); (mk_real_int64 200L); (mk_real_int64 460L); (mk_real_int64 460L); (mk_real_int64 200L); (mk_real_int64 55L); (mk_real_int64 325L); (mk_real_int64 385L); (mk_real_int64 305L); (mk_real_int64 360L); ]);\r
("y2_hi", [4; 8; 14; 16; 22; 23; 28; 29; 36; 37; 47; 49; 58; 60; 62; 65; 70; 71; 72; 75; ], [(mk_real_int64 72L); (mk_real_int64 120L); (mk_real_int64 60L); (mk_real_int64 60L); (mk_real_int64 48L); (mk_real_int64 560L); (mk_real_int64 8L); (mk_real_int64 140L); (mk_real_int64 380L); (mk_real_int64 48L); (mk_real_int64 4L); (mk_real_int64 80L); (mk_real_int64 472L); (mk_real_int64 160L); (mk_real_int64 168L); (mk_real_int64 168L); (mk_real_int64 80L); (mk_real_int64 124L); (mk_real_int64 80L); (mk_real_int64 132L); ]);\r
("y2_lo", [6; 9; 10; 18; 19; 20; 21; 25; 26; 30; 31; 38; 40; 41; 42; 44; 45; 46; 48; 51; 52; 53; 54; 55; 56; 57; 59; 61; 63; 64; 66; 67; 69; 73; 74; ], [(mk_real_int64 220L); (mk_real_int64 76L); (mk_real_int64 196L); (mk_real_int64 216L); (mk_real_int64 188L); (mk_real_int64 252L); (mk_real_int64 144L); (mk_real_int64 10L); (mk_real_int64 76L); (mk_real_int64 272L); (mk_real_int64 40L); (mk_real_int64 460L); (mk_real_int64 80L); (mk_real_int64 220L); (mk_real_int64 76L); (mk_real_int64 344L); (mk_real_int64 164L); (mk_real_int64 260L); (mk_real_int64 340L); (mk_real_int64 216L); (mk_real_int64 76L); (mk_real_int64 216L); (mk_real_int64 140L); (mk_real_int64 88L); (mk_real_int64 200L); (mk_real_int64 352L); (mk_real_int64 10L); (mk_real_int64 272L); (mk_real_int64 48L); (mk_real_int64 48L); (mk_real_int64 272L); (mk_real_int64 268L); (mk_real_int64 332L); (mk_real_int64 148L); (mk_real_int64 316L); ]);\r
("y3_hi", [4; 8; 14; 16; 22; 23; 28; 29; 36; 37; 47; 49; 58; 60; 62; 65; 70; 71; 72; 75; ], [(mk_real_int64 72L); (mk_real_int64 120L); (mk_real_int64 60L); (mk_real_int64 60L); (mk_real_int64 48L); (mk_real_int64 560L); (mk_real_int64 8L); (mk_real_int64 140L); (mk_real_int64 380L); (mk_real_int64 48L); (mk_real_int64 4L); (mk_real_int64 80L); (mk_real_int64 472L); (mk_real_int64 160L); (mk_real_int64 168L); (mk_real_int64 168L); (mk_real_int64 80L); (mk_real_int64 124L); (mk_real_int64 80L); (mk_real_int64 132L); ]);\r
("y3_lo", [6; 9; 10; 18; 19; 20; 21; 25; 26; 30; 31; 38; 40; 41; 42; 44; 45; 46; 48; 51; 52; 53; 54; 55; 56; 57; 59; 61; 63; 64; 66; 67; 69; 73; 74; ], [(mk_real_int64 220L); (mk_real_int64 76L); (mk_real_int64 196L); (mk_real_int64 216L); (mk_real_int64 188L); (mk_real_int64 252L); (mk_real_int64 144L); (mk_real_int64 10L); (mk_real_int64 76L); (mk_real_int64 272L); (mk_real_int64 40L); (mk_real_int64 460L); (mk_real_int64 80L); (mk_real_int64 220L); (mk_real_int64 76L); (mk_real_int64 344L); (mk_real_int64 164L); (mk_real_int64 260L); (mk_real_int64 340L); (mk_real_int64 216L); (mk_real_int64 76L); (mk_real_int64 216L); (mk_real_int64 140L); (mk_real_int64 88L); (mk_real_int64 200L); (mk_real_int64 352L); (mk_real_int64 10L); (mk_real_int64 272L); (mk_real_int64 48L); (mk_real_int64 48L); (mk_real_int64 272L); (mk_real_int64 268L); (mk_real_int64 332L); (mk_real_int64 148L); (mk_real_int64 316L); ]);\r
("y4_lo", [0; 2; 15; 16; 25; 26; 32; 33; 37; 48; 53; 57; 62; 65; 67; 69; 70; 71; ], [(mk_real_int64 630L); (mk_real_int64 125L); (mk_real_int64 33L); (mk_real_int64 45L); (mk_real_int64 125L); (mk_real_int64 370L); (mk_real_int64 375L); (mk_real_int64 420L); (mk_real_int64 375L); (mk_real_int64 85L); (mk_real_int64 77L); (mk_real_int64 370L); (mk_real_int64 370L); (mk_real_int64 45L); (mk_real_int64 335L); (mk_real_int64 205L); (mk_real_int64 269L); (mk_real_int64 405L); ]);\r
("y4_hi", [4; 5; 6; 10; 12; 14; 17; 18; 19; 21; 22; 24; 27; 34; 36; 38; 40; 41; 42; 43; 44; 45; 47; 49; 50; 51; 52; 54; 55; 56; 58; 59; 60; 61; 63; 66; ], [(mk_real_int64 450L); (mk_real_int64 665L); (mk_real_int64 715L); (mk_real_int64 125L); (mk_real_int64 125L); (mk_real_int64 184L); (mk_real_int64 331L); (mk_real_int64 98L); (mk_real_int64 250L); (mk_real_int64 315L); (mk_real_int64 165L); (mk_real_int64 558L); (mk_real_int64 250L); (mk_real_int64 575L); (mk_real_int64 200L); (mk_real_int64 665L); (mk_real_int64 101L); (mk_real_int64 377L); (mk_real_int64 25L); (mk_real_int64 465L); (mk_real_int64 375L); (mk_real_int64 100L); (mk_real_int64 184L); (mk_real_int64 184L); (mk_real_int64 125L); (mk_real_int64 520L); (mk_real_int64 250L); (mk_real_int64 120L); (mk_real_int64 315L); (mk_real_int64 500L); (mk_real_int64 58L); (mk_real_int64 170L); (mk_real_int64 170L); (mk_real_int64 58L); (mk_real_int64 95L); (mk_real_int64 264L); ]);\r
("y5_hi", [4; 8; 10; 14; 16; 22; 23; 26; 28; 31; 37; 38; 45; 47; 48; 54; 56; 58; 60; 69; 70; 71; 73; 75; ], [(mk_real_int64 72L); (mk_real_int64 170L); (mk_real_int64 254L); (mk_real_int64 125L); (mk_real_int64 125L); (mk_real_int64 48L); (mk_real_int64 250L); (mk_real_int64 99L); (mk_real_int64 8L); (mk_real_int64 250L); (mk_real_int64 48L); (mk_real_int64 295L); (mk_real_int64 188L); (mk_real_int64 4L); (mk_real_int64 375L); (mk_real_int64 125L); (mk_real_int64 250L); (mk_real_int64 472L); (mk_real_int64 500L); (mk_real_int64 98L); (mk_real_int64 264L); (mk_real_int64 124L); (mk_real_int64 302L); (mk_real_int64 132L); ]);\r
("y5_lo", [6; 9; 18; 19; 20; 21; 25; 29; 30; 36; 40; 41; 42; 44; 46; 49; 51; 52; 53; 55; 57; 59; 61; 62; 63; 64; 65; 66; 67; 74; ], [(mk_real_int64 125L); (mk_real_int64 76L); (mk_real_int64 216L); (mk_real_int64 33L); (mk_real_int64 252L); (mk_real_int64 144L); (mk_real_int64 160L); (mk_real_int64 100L); (mk_real_int64 272L); (mk_real_int64 375L); (mk_real_int64 80L); (mk_real_int64 375L); (mk_real_int64 76L); (mk_real_int64 124L); (mk_real_int64 260L); (mk_real_int64 365L); (mk_real_int64 216L); (mk_real_int64 76L); (mk_real_int64 216L); (mk_real_int64 88L); (mk_real_int64 552L); (mk_real_int64 160L); (mk_real_int64 272L); (mk_real_int64 492L); (mk_real_int64 48L); (mk_real_int64 48L); (mk_real_int64 492L); (mk_real_int64 272L); (mk_real_int64 268L); (mk_real_int64 44L); ]);\r
("y6_hi", [4; 8; 10; 14; 22; 23; 26; 28; 31; 37; 38; 45; 47; 48; 54; 56; 58; 59; 60; 69; 71; 73; 75; ], [(mk_real_int64 72L); (mk_real_int64 170L); (mk_real_int64 254L); (mk_real_int64 125L); (mk_real_int64 48L); (mk_real_int64 250L); (mk_real_int64 99L); (mk_real_int64 8L); (mk_real_int64 250L); (mk_real_int64 48L); (mk_real_int64 295L); (mk_real_int64 188L); (mk_real_int64 4L); (mk_real_int64 375L); (mk_real_int64 125L); (mk_real_int64 250L); (mk_real_int64 472L); (mk_real_int64 840L); (mk_real_int64 500L); (mk_real_int64 98L); (mk_real_int64 124L); (mk_real_int64 302L); (mk_real_int64 132L); ]);\r
("y6_lo", [6; 7; 9; 10; 13; 14; 16; 18; 19; 20; 21; 22; 25; 29; 30; 31; 32; 36; 40; 41; 42; 44; 46; 47; 49; 50; 51; 52; 53; 55; 56; 57; 58; 59; 61; 62; 63; 64; 65; 66; 67; 68; 70; 74; ], [(mk_real_int64 125L); (mk_real_int64 388000L); (mk_real_int64 76L); (mk_real_int64 50000L); (mk_real_int64 279000L); (mk_real_int64 123000L); (mk_real_int64 239875L); (mk_real_int64 216L); (mk_real_int64 197033L); (mk_real_int64 252L); (mk_real_int64 144L); (mk_real_int64 140000L); (mk_real_int64 160L); (mk_real_int64 100L); (mk_real_int64 500272L); (mk_real_int64 46000L); (mk_real_int64 60000L); (mk_real_int64 375L); (mk_real_int64 357080L); (mk_real_int64 358375L); (mk_real_int64 76L); (mk_real_int64 124L); (mk_real_int64 260L); (mk_real_int64 191000L); (mk_real_int64 365L); (mk_real_int64 335000L); (mk_real_int64 216L); (mk_real_int64 76L); (mk_real_int64 216L); (mk_real_int64 88L); (mk_real_int64 335000L); (mk_real_int64 552L); (mk_real_int64 268000L); (mk_real_int64 528000L); (mk_real_int64 346272L); (mk_real_int64 492L); (mk_real_int64 48L); (mk_real_int64 228048L); (mk_real_int64 492L); (mk_real_int64 272L); (mk_real_int64 268L); (mk_real_int64 169000L); (mk_real_int64 80736L); (mk_real_int64 619044L); ]);\r
("y8_hi", [1; ], [(mk_real_int64 31000L); ]);\r
("ye_lo", [8; 13; 33; 47; 53; 59; 60; 66; 71; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 167000L); (mk_real_int64 1000L); (mk_real_int64 164000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 335000L); (mk_real_int64 1000L); ]);\r
("ye_hi", [51; 62; 63; 64; 65; 66; ], [(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", [3; ], [(mk_real_int64 712L); ]);\r
("yn_hi", [0; 1; 2; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 288L); (mk_real_int64 288L); (mk_real_int64 288L); (mk_real_int64 10L); (mk_real_int64 288L); (mk_real_int64 1288L); (mk_real_int64 1288L); (mk_real_int64 288L); (mk_real_int64 1440L); (mk_real_int64 288L); (mk_real_int64 1288L); (mk_real_int64 1288L); (mk_real_int64 1288L); (mk_real_int64 1288L); ]);\r
];;\r
let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
end;;\r
\r
concl (Test_case.result)\r