Update from HH

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

needs "nobranching_lp.hl";;
\r
module Test_case = struct\r
let hypermap_string = "86324340346 19 6 0 1 2 3 4 5 4 0 5 6 7 3 6 5 4 3 6 4 8 3 8 4 3 4 8 3 9 10 3 9 3 2 3 9 2 11 3 11 2 12 3 12 2 1 3 12 1 0 3 12 0 13 3 13 0 7 3 13 7 10 3 8 10 7 3 11 12 13 3 7 6 8 3 11 13 10 3 10 9 11 ";;\r
let precision = 3;;\r
(***************)\r
(* Constraints *)\r
(***************)\r
let constraints = [\r
("azim_sum", [5; 7; 9; 10; 11; ], [(mk_real_int64 54L); (mk_real_int64 458L); (mk_real_int64 216L); (mk_real_int64 137L); (mk_real_int64 543L); ]);\r
("azim_sum_neg", [0; 1; 4; 6; 8; 12; 13; ], [(mk_real_int64 26L); (mk_real_int64 19L); (mk_real_int64 460L); (mk_real_int64 137L); (mk_real_int64 26L); (mk_real_int64 93L); (mk_real_int64 50L); ]);\r
("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 972L); (mk_real_int64 1045L); (mk_real_int64 1026L); (mk_real_int64 1026L); (mk_real_int64 799L); (mk_real_int64 1026L); (mk_real_int64 799L); (mk_real_int64 1026L); (mk_real_int64 946L); (mk_real_int64 1026L); (mk_real_int64 1026L); (mk_real_int64 1026L); (mk_real_int64 1026L); (mk_real_int64 1015L); ]);\r
("sol_sum3", [0; 1; 6; 7; ], [(mk_real_int64 26L); (mk_real_int64 26L); (mk_real_int64 137L); (mk_real_int64 137L); ]);\r
("sol_sum3_neg", [5; 9; 10; 11; ], [(mk_real_int64 83L); (mk_real_int64 54L); (mk_real_int64 458L); (mk_real_int64 234L); ]);\r
("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; ], [(mk_real_int64 946L); (mk_real_int64 946L); (mk_real_int64 1026L); (mk_real_int64 1026L); (mk_real_int64 966L); (mk_real_int64 580L); (mk_real_int64 799L); (mk_real_int64 799L); (mk_real_int64 799L); (mk_real_int64 1026L); (mk_real_int64 1026L); (mk_real_int64 1026L); (mk_real_int64 799L); (mk_real_int64 946L); (mk_real_int64 1015L); (mk_real_int64 966L); ]);\r
("tau_sum4_neg", [0; 1; ], [(mk_real_int64 946L); (mk_real_int64 1026L); ]);\r
("tau_sum6_neg", [0; ], [(mk_real_int64 1026L); ]);\r
("ln_def_neg", [0; 1; 2; 3; 5; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 72L); (mk_real_int64 152L); (mk_real_int64 131L); (mk_real_int64 131L); (mk_real_int64 131L); (mk_real_int64 131L); (mk_real_int64 43L); (mk_real_int64 131L); (mk_real_int64 131L); (mk_real_int64 131L); (mk_real_int64 131L); (mk_real_int64 119L); ]);\r
("ln_def", [4; 6; ], [(mk_real_int64 119L); (mk_real_int64 119L); ]);\r
("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 6107L); (mk_real_int64 6564L); (mk_real_int64 6446L); (mk_real_int64 6446L); (mk_real_int64 5023L); (mk_real_int64 6446L); (mk_real_int64 5023L); (mk_real_int64 6446L); (mk_real_int64 5942L); (mk_real_int64 6446L); (mk_real_int64 6446L); (mk_real_int64 6446L); (mk_real_int64 6446L); (mk_real_int64 6379L); ]);\r
("edge_sym", [0; 5; 7; 22; 31; 37; 39; 43; 45; 52; ], [(mk_real_int64 22L); (mk_real_int64 22L); (mk_real_int64 79L); (mk_real_int64 55L); (mk_real_int64 94L); (mk_real_int64 277L); (mk_real_int64 231L); (mk_real_int64 30L); (mk_real_int64 47L); (mk_real_int64 148L); ]);\r
("edge_sym_neg", [12; 14; 15; 18; 25; 27; 28; 30; 40; 46; 49; 58; ], [(mk_real_int64 106L); (mk_real_int64 21L); (mk_real_int64 21L); (mk_real_int64 55L); (mk_real_int64 142L); (mk_real_int64 94L); (mk_real_int64 87L); (mk_real_int64 224L); (mk_real_int64 130L); (mk_real_int64 166L); (mk_real_int64 109L); (mk_real_int64 31L); ]);\r
("y1_def_neg", [0; 11; 12; 13; 15; 16; 18; 19; 25; 26; 28; 29; 32; 37; 39; 40; 41; 42; 43; 46; 50; 52; 53; 55; 57; 58; 59; 61; ], [(mk_real_int64 17L); (mk_real_int64 16L); (mk_real_int64 144L); (mk_real_int64 4L); (mk_real_int64 64L); (mk_real_int64 42L); (mk_real_int64 175L); (mk_real_int64 43L); (mk_real_int64 185L); (mk_real_int64 4L); (mk_real_int64 129L); (mk_real_int64 182L); (mk_real_int64 11L); (mk_real_int64 24L); (mk_real_int64 134L); (mk_real_int64 296L); (mk_real_int64 7L); (mk_real_int64 169L); (mk_real_int64 74L); (mk_real_int64 160L); (mk_real_int64 87L); (mk_real_int64 101L); (mk_real_int64 67L); (mk_real_int64 48L); (mk_real_int64 219L); (mk_real_int64 134L); (mk_real_int64 19L); (mk_real_int64 10L); ]);\r
("y1_def", [23; 31; 34; 36; 38; 44; 47; 48; 51; 54; 56; 60; ], [(mk_real_int64 47L); (mk_real_int64 31L); (mk_real_int64 100L); (mk_real_int64 141L); (mk_real_int64 68L); (mk_real_int64 334L); (mk_real_int64 9L); (mk_real_int64 35L); (mk_real_int64 68L); (mk_real_int64 13L); (mk_real_int64 25L); (mk_real_int64 17L); ]);\r
("y2_def", [0; 11; 16; 19; 26; 29; 31; 39; 40; 41; 43; 44; 48; 52; 53; 55; 58; 59; ], [(mk_real_int64 22L); (mk_real_int64 10L); (mk_real_int64 66L); (mk_real_int64 55L); (mk_real_int64 2L); (mk_real_int64 110L); (mk_real_int64 31L); (mk_real_int64 82L); (mk_real_int64 5L); (mk_real_int64 10L); (mk_real_int64 167L); (mk_real_int64 125L); (mk_real_int64 61L); (mk_real_int64 61L); (mk_real_int64 59L); (mk_real_int64 29L); (mk_real_int64 201L); (mk_real_int64 12L); ]);\r
("y2_def_neg", [12; 13; 15; 18; 23; 25; 28; 32; 34; 36; 37; 38; 42; 46; 47; 50; 51; 54; 56; 57; 60; 61; ], [(mk_real_int64 144L); (mk_real_int64 4L); (mk_real_int64 45L); (mk_real_int64 175L); (mk_real_int64 14L); (mk_real_int64 185L); (mk_real_int64 129L); (mk_real_int64 11L); (mk_real_int64 57L); (mk_real_int64 70L); (mk_real_int64 24L); (mk_real_int64 21L); (mk_real_int64 169L); (mk_real_int64 160L); (mk_real_int64 3L); (mk_real_int64 36L); (mk_real_int64 21L); (mk_real_int64 4L); (mk_real_int64 8L); (mk_real_int64 129L); (mk_real_int64 5L); (mk_real_int64 10L); ]);\r
("y3_def", [0; 11; 16; 19; 26; 29; 31; 39; 40; 41; 43; 44; 48; 52; 53; 55; 58; 59; ], [(mk_real_int64 22L); (mk_real_int64 10L); (mk_real_int64 66L); (mk_real_int64 55L); (mk_real_int64 2L); (mk_real_int64 110L); (mk_real_int64 31L); (mk_real_int64 82L); (mk_real_int64 5L); (mk_real_int64 10L); (mk_real_int64 167L); (mk_real_int64 125L); (mk_real_int64 61L); (mk_real_int64 61L); (mk_real_int64 59L); (mk_real_int64 29L); (mk_real_int64 201L); (mk_real_int64 12L); ]);\r
("y3_def_neg", [12; 13; 15; 18; 23; 25; 28; 32; 34; 36; 37; 38; 42; 46; 47; 50; 51; 54; 56; 57; 60; 61; ], [(mk_real_int64 144L); (mk_real_int64 4L); (mk_real_int64 45L); (mk_real_int64 175L); (mk_real_int64 14L); (mk_real_int64 185L); (mk_real_int64 129L); (mk_real_int64 11L); (mk_real_int64 57L); (mk_real_int64 70L); (mk_real_int64 24L); (mk_real_int64 21L); (mk_real_int64 169L); (mk_real_int64 160L); (mk_real_int64 3L); (mk_real_int64 36L); (mk_real_int64 21L); (mk_real_int64 4L); (mk_real_int64 8L); (mk_real_int64 129L); (mk_real_int64 5L); (mk_real_int64 10L); ]);\r
("y4_def_neg", [1; 2; 5; 6; 8; 11; 12; 14; 15; 17; 18; 23; 25; 26; 27; 28; 29; 32; 34; 36; 38; 39; 41; 43; 44; 45; 47; ], [(mk_real_int64 18L); (mk_real_int64 88L); (mk_real_int64 50L); (mk_real_int64 124L); (mk_real_int64 121L); (mk_real_int64 128L); (mk_real_int64 4L); (mk_real_int64 90L); (mk_real_int64 207L); (mk_real_int64 16L); (mk_real_int64 7L); (mk_real_int64 17L); (mk_real_int64 153L); (mk_real_int64 338L); (mk_real_int64 19L); (mk_real_int64 117L); (mk_real_int64 287L); (mk_real_int64 111L); (mk_real_int64 106L); (mk_real_int64 75L); (mk_real_int64 115L); (mk_real_int64 111L); (mk_real_int64 55L); (mk_real_int64 224L); (mk_real_int64 379L); (mk_real_int64 22L); (mk_real_int64 7L); ]);\r
("y4_def", [3; 9; 20; 22; 24; 30; 33; 37; 40; 42; 46; ], [(mk_real_int64 8L); (mk_real_int64 72L); (mk_real_int64 231L); (mk_real_int64 294L); (mk_real_int64 106L); (mk_real_int64 158L); (mk_real_int64 14L); (mk_real_int64 106L); (mk_real_int64 20L); (mk_real_int64 38L); (mk_real_int64 26L); ]);\r
("y5_def", [0; 11; 13; 16; 19; 26; 29; 34; 39; 40; 41; 43; 52; 53; 55; 58; 59; ], [(mk_real_int64 22L); (mk_real_int64 10L); (mk_real_int64 8L); (mk_real_int64 66L); (mk_real_int64 55L); (mk_real_int64 2L); (mk_real_int64 110L); (mk_real_int64 7L); (mk_real_int64 82L); (mk_real_int64 44L); (mk_real_int64 10L); (mk_real_int64 136L); (mk_real_int64 61L); (mk_real_int64 59L); (mk_real_int64 29L); (mk_real_int64 201L); (mk_real_int64 12L); ]);\r
("y5_def_neg", [12; 15; 18; 23; 25; 28; 31; 32; 36; 37; 38; 42; 44; 46; 47; 48; 50; 51; 54; 56; 57; 60; 61; ], [(mk_real_int64 88L); (mk_real_int64 29L); (mk_real_int64 121L); (mk_real_int64 14L); (mk_real_int64 128L); (mk_real_int64 90L); (mk_real_int64 16L); (mk_real_int64 7L); (mk_real_int64 5L); (mk_real_int64 17L); (mk_real_int64 21L); (mk_real_int64 117L); (mk_real_int64 138L); (mk_real_int64 111L); (mk_real_int64 3L); (mk_real_int64 61L); (mk_real_int64 19L); (mk_real_int64 21L); (mk_real_int64 4L); (mk_real_int64 8L); (mk_real_int64 74L); (mk_real_int64 5L); (mk_real_int64 7L); ]);\r
("y6_def", [0; 11; 13; 16; 17; 19; 23; 24; 26; 29; 34; 35; 39; 40; 41; 43; 44; 47; 50; 51; 52; 53; 54; 55; 56; 58; 59; 60; ], [(mk_real_int64 22L); (mk_real_int64 88L); (mk_real_int64 156L); (mk_real_int64 142L); (mk_real_int64 245L); (mk_real_int64 55L); (mk_real_int64 128L); (mk_real_int64 56L); (mk_real_int64 232L); (mk_real_int64 110L); (mk_real_int64 7L); (mk_real_int64 22L); (mk_real_int64 82L); (mk_real_int64 44L); (mk_real_int64 174L); (mk_real_int64 136L); (mk_real_int64 82L); (mk_real_int64 5L); (mk_real_int64 42L); (mk_real_int64 144L); (mk_real_int64 61L); (mk_real_int64 59L); (mk_real_int64 103L); (mk_real_int64 29L); (mk_real_int64 305L); (mk_real_int64 201L); (mk_real_int64 12L); (mk_real_int64 116L); ]);\r
("y6_def_neg", [12; 15; 18; 25; 28; 31; 32; 36; 37; 38; 42; 46; 48; 57; 61; ], [(mk_real_int64 88L); (mk_real_int64 29L); (mk_real_int64 121L); (mk_real_int64 128L); (mk_real_int64 90L); (mk_real_int64 16L); (mk_real_int64 7L); (mk_real_int64 5L); (mk_real_int64 17L); (mk_real_int64 21L); (mk_real_int64 117L); (mk_real_int64 111L); (mk_real_int64 61L); (mk_real_int64 74L); (mk_real_int64 7L); ]);\r
("RHA", [4; 6; 7; 9; 12; 14; 15; 17; 26; 27; 28; 29; 30; 31; 33; 37; 39; 50; 52; 59; 60; 61; ], [(mk_real_int64 19L); (mk_real_int64 80L); (mk_real_int64 26L); (mk_real_int64 80L); (mk_real_int64 99L); (mk_real_int64 99L); (mk_real_int64 61L); (mk_real_int64 19L); (mk_real_int64 54L); (mk_real_int64 60L); (mk_real_int64 50L); (mk_real_int64 133L); (mk_real_int64 446L); (mk_real_int64 219L); (mk_real_int64 227L); (mk_real_int64 227L); (mk_real_int64 3L); (mk_real_int64 163L); (mk_real_int64 58L); (mk_real_int64 28L); (mk_real_int64 60L); (mk_real_int64 50L); ]);\r
("RHB", [1; ], [(mk_real_int64 227L); ]);\r
("yy10", [6; ], [(mk_real_int64 22L); ]);\r
("tau6", [0; ], [(mk_real_int64 1026L); ]);\r
("ineq105", [0; 10; ], [(mk_real_int64 54L); (mk_real_int64 138L); ]);\r
("ineq106", [1; 5; 12; 15; 25; 26; 36; 38; 39; 41; 43; 44; 45; ], [(mk_real_int64 26L); (mk_real_int64 20L); (mk_real_int64 6L); (mk_real_int64 303L); (mk_real_int64 224L); (mk_real_int64 227L); (mk_real_int64 53L); (mk_real_int64 169L); (mk_real_int64 80L); (mk_real_int64 80L); (mk_real_int64 11L); (mk_real_int64 11L); (mk_real_int64 32L); ]);\r
("ineq107", [9; 20; 22; 24; 30; 33; 37; 40; 42; 46; ], [(mk_real_int64 93L); (mk_real_int64 242L); (mk_real_int64 323L); (mk_real_int64 137L); (mk_real_int64 321L); (mk_real_int64 18L); (mk_real_int64 137L); (mk_real_int64 26L); (mk_real_int64 50L); (mk_real_int64 33L); ]);\r
("ineq108", [6; 26; 27; 29; 34; 39; 43; 44; ], [(mk_real_int64 181L); (mk_real_int64 137L); (mk_real_int64 28L); (mk_real_int64 404L); (mk_real_int64 43L); (mk_real_int64 82L); (mk_real_int64 133L); (mk_real_int64 543L); ]);\r
("ineq109", [2; 3; 20; 22; ], [(mk_real_int64 26L); (mk_real_int64 26L); (mk_real_int64 137L); (mk_real_int64 137L); ]);\r
("ineq110", [17; 29; 30; 34; ], [(mk_real_int64 83L); (mk_real_int64 54L); (mk_real_int64 458L); (mk_real_int64 234L); ]);\r
("ineq111", [2; 5; 8; 11; 14; 18; 23; 26; 28; 32; 34; 36; 43; 47; ], [(mk_real_int64 775L); (mk_real_int64 292L); (mk_real_int64 970L); (mk_real_int64 1026L); (mk_real_int64 718L); (mk_real_int64 59L); (mk_real_int64 133L); (mk_real_int64 709L); (mk_real_int64 938L); (mk_real_int64 890L); (mk_real_int64 243L); (mk_real_int64 307L); (mk_real_int64 1008L); (mk_real_int64 54L); ]);\r
("ineq112", [20; ], [(mk_real_int64 160L); ]);\r
("ineq113", [12; ], [(mk_real_int64 151L); ]);\r
("ineq114", [2; 4; 5; 6; 13; 16; 19; 23; 25; 27; 32; 34; 35; 36; 38; 39; 41; 43; 45; ], [(mk_real_int64 170L); (mk_real_int64 170L); (mk_real_int64 484L); (mk_real_int64 56L); (mk_real_int64 96L); (mk_real_int64 580L); (mk_real_int64 580L); (mk_real_int64 666L); (mk_real_int64 90L); (mk_real_int64 88L); (mk_real_int64 136L); (mk_real_int64 425L); (mk_real_int64 358L); (mk_real_int64 181L); (mk_real_int64 312L); (mk_real_int64 601L); (mk_real_int64 345L); (mk_real_int64 7L); (mk_real_int64 912L); ]);\r
("ineq119", [2; 6; ], [(mk_real_int64 58L); (mk_real_int64 206L); ]);\r
("ineq120", [0; 3; 4; 7; ], [(mk_real_int64 177L); (mk_real_int64 711L); (mk_real_int64 103L); (mk_real_int64 717L); ]);\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 3275L); (mk_real_int64 3300L); (mk_real_int64 2950L); (mk_real_int64 2950L); (mk_real_int64 1975L); (mk_real_int64 2950L); (mk_real_int64 1975L); (mk_real_int64 2950L); (mk_real_int64 3150L); (mk_real_int64 2950L); (mk_real_int64 2950L); (mk_real_int64 2950L); (mk_real_int64 2950L); (mk_real_int64 2675L); ]);\r
];;\r
\r
(*************************)\r
\r
let variable_bounds = [\r
("azim_lo", [8; 15; 21; 26; 33; 34; 37; 39; 55; 59; ], [(mk_real_int64 274L); (mk_real_int64 16L); (mk_real_int64 318L); (mk_real_int64 109L); (mk_real_int64 920L); (mk_real_int64 120L); (mk_real_int64 1084L); (mk_real_int64 660L); (mk_real_int64 30L); (mk_real_int64 88L); ]);\r
("azim_hi", [1; 5; 6; 9; 12; 14; 16; 19; 22; 27; 30; 31; 41; 46; 48; 49; 50; 52; 53; 57; ], [(mk_real_int64 726952L); (mk_real_int64 26000L); (mk_real_int64 166L); (mk_real_int64 938L); (mk_real_int64 420L); (mk_real_int64 420L); (mk_real_int64 56L); (mk_real_int64 74L); (mk_real_int64 486L); (mk_real_int64 96L); (mk_real_int64 80L); (mk_real_int64 1000L); (mk_real_int64 88L); (mk_real_int64 136L); (mk_real_int64 50L); (mk_real_int64 108L); (mk_real_int64 306L); (mk_real_int64 312L); (mk_real_int64 226L); (mk_real_int64 382L); ]);\r
("rhazim_hi", [5; 15; 28; 29; 61; ], [(mk_real_int64 54000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("rho_hi", [0; 1; 2; 3; 5; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 1048L); (mk_real_int64 2780L); (mk_real_int64 1384L); (mk_real_int64 1384L); (mk_real_int64 1384L); (mk_real_int64 1384L); (mk_real_int64 2664L); (mk_real_int64 1384L); (mk_real_int64 1384L); (mk_real_int64 1384L); (mk_real_int64 1384L); ]);\r
("rho_lo", [4; 6; 13; ], [(mk_real_int64 2084L); (mk_real_int64 2084L); (mk_real_int64 740L); ]);\r
("tau_hi", [15; ], [(mk_real_int64 1000L); ]);\r
("tau_lo", [2; 7; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("y1_lo", [0; 15; 16; 19; 23; 28; 36; 39; 40; 43; 46; 50; 52; 53; 57; 58; 59; 60; ], [(mk_real_int64 10L); (mk_real_int64 560L); (mk_real_int64 535L); (mk_real_int64 470L); (mk_real_int64 500L); (mk_real_int64 240L); (mk_real_int64 187L); (mk_real_int64 400L); (mk_real_int64 15L); (mk_real_int64 420L); (mk_real_int64 200L); (mk_real_int64 60L); (mk_real_int64 400L); (mk_real_int64 270L); (mk_real_int64 295L); (mk_real_int64 205L); (mk_real_int64 200L); (mk_real_int64 500L); ]);\r
("y1_hi", [11; 12; 13; 18; 25; 26; 29; 31; 32; 34; 37; 38; 41; 42; 44; 48; 51; 61; ], [(mk_real_int64 400L); (mk_real_int64 574L); (mk_real_int64 74L); (mk_real_int64 400L); (mk_real_int64 320L); (mk_real_int64 400L); (mk_real_int64 200L); (mk_real_int64 540L); (mk_real_int64 380L); (mk_real_int64 313L); (mk_real_int64 60L); (mk_real_int64 500L); (mk_real_int64 420L); (mk_real_int64 160L); (mk_real_int64 540L); (mk_real_int64 75L); (mk_real_int64 500L); (mk_real_int64 280L); ]);\r
("y2_lo", [0; 11; 15; 16; 23; 28; 34; 39; 40; 46; 48; 53; 57; 59; 60; ], [(mk_real_int64 292L); (mk_real_int64 536L); (mk_real_int64 280L); (mk_real_int64 116L); (mk_real_int64 136L); (mk_real_int64 240L); (mk_real_int64 471L); (mk_real_int64 464L); (mk_real_int64 124L); (mk_real_int64 200L); (mk_real_int64 168L); (mk_real_int64 32L); (mk_real_int64 24L); (mk_real_int64 352L); (mk_real_int64 16L); ]);\r
("y2_hi", [12; 13; 18; 19; 25; 26; 29; 31; 32; 36; 37; 38; 41; 42; 43; 44; 47; 50; 51; 52; 54; 55; 56; 58; 61; ], [(mk_real_int64 574L); (mk_real_int64 74L); (mk_real_int64 400L); (mk_real_int64 476L); (mk_real_int64 320L); (mk_real_int64 184L); (mk_real_int64 292L); (mk_real_int64 540L); (mk_real_int64 380L); (mk_real_int64 217L); (mk_real_int64 60L); (mk_real_int64 176L); (mk_real_int64 192L); (mk_real_int64 160L); (mk_real_int64 576L); (mk_real_int64 248L); (mk_real_int64 264L); (mk_real_int64 32L); (mk_real_int64 176L); (mk_real_int64 516L); (mk_real_int64 48L); (mk_real_int64 120L); (mk_real_int64 400L); (mk_real_int64 656L); (mk_real_int64 280L); ]);\r
("y3_lo", [0; 11; 15; 16; 23; 28; 34; 39; 40; 46; 48; 53; 57; 59; 60; ], [(mk_real_int64 292L); (mk_real_int64 536L); (mk_real_int64 280L); (mk_real_int64 116L); (mk_real_int64 136L); (mk_real_int64 240L); (mk_real_int64 471L); (mk_real_int64 464L); (mk_real_int64 124L); (mk_real_int64 200L); (mk_real_int64 168L); (mk_real_int64 32L); (mk_real_int64 24L); (mk_real_int64 352L); (mk_real_int64 16L); ]);\r
("y3_hi", [12; 13; 18; 19; 25; 26; 29; 31; 32; 36; 37; 38; 41; 42; 43; 44; 47; 50; 51; 52; 54; 55; 56; 58; 61; ], [(mk_real_int64 574L); (mk_real_int64 74L); (mk_real_int64 400L); (mk_real_int64 476L); (mk_real_int64 320L); (mk_real_int64 184L); (mk_real_int64 292L); (mk_real_int64 540L); (mk_real_int64 380L); (mk_real_int64 217L); (mk_real_int64 60L); (mk_real_int64 176L); (mk_real_int64 192L); (mk_real_int64 160L); (mk_real_int64 576L); (mk_real_int64 248L); (mk_real_int64 264L); (mk_real_int64 32L); (mk_real_int64 176L); (mk_real_int64 516L); (mk_real_int64 48L); (mk_real_int64 120L); (mk_real_int64 400L); (mk_real_int64 656L); (mk_real_int64 280L); ]);\r
("y4_hi", [1; 3; 6; 14; 20; 22; 23; 26; 30; 34; 36; 39; 40; 41; 42; 45; 47; ], [(mk_real_int64 190L); (mk_real_int64 424L); (mk_real_int64 15L); (mk_real_int64 250L); (mk_real_int64 454L); (mk_real_int64 67L); (mk_real_int64 375L); (mk_real_int64 35L); (mk_real_int64 365L); (mk_real_int64 306L); (mk_real_int64 320L); (mk_real_int64 30L); (mk_real_int64 98L); (mk_real_int64 200L); (mk_real_int64 650L); (mk_real_int64 80L); (mk_real_int64 250L); ]);\r
("y4_lo", [2; 5; 8; 9; 11; 12; 15; 17; 18; 24; 25; 27; 28; 29; 32; 33; 37; 38; 43; 44; 46; ], [(mk_real_int64 451L); (mk_real_int64 200L); (mk_real_int64 250L); (mk_real_int64 111L); (mk_real_int64 250L); (mk_real_int64 110L); (mk_real_int64 555L); (mk_real_int64 268L); (mk_real_int64 375L); (mk_real_int64 99L); (mk_real_int64 440L); (mk_real_int64 180L); (mk_real_int64 250L); (mk_real_int64 324L); (mk_real_int64 250L); (mk_real_int64 86L); (mk_real_int64 99L); (mk_real_int64 765L); (mk_real_int64 640L); (mk_real_int64 490L); (mk_real_int64 491L); ]);\r
("y5_lo", [0; 11; 12; 15; 16; 18; 23; 25; 31; 32; 39; 40; 42; 44; 46; 50; 53; 59; 60; ], [(mk_real_int64 292L); (mk_real_int64 536L); (mk_real_int64 451L); (mk_real_int64 220L); (mk_real_int64 116L); (mk_real_int64 250L); (mk_real_int64 136L); (mk_real_int64 250L); (mk_real_int64 268L); (mk_real_int64 375L); (mk_real_int64 464L); (mk_real_int64 129L); (mk_real_int64 250L); (mk_real_int64 560L); (mk_real_int64 250L); (mk_real_int64 83L); (mk_real_int64 32L); (mk_real_int64 352L); (mk_real_int64 16L); ]);\r
("y5_hi", [13; 19; 26; 28; 29; 34; 36; 37; 38; 41; 43; 47; 48; 51; 52; 54; 55; 56; 57; 58; 61; ], [(mk_real_int64 424L); (mk_real_int64 476L); (mk_real_int64 184L); (mk_real_int64 250L); (mk_real_int64 292L); (mk_real_int64 604L); (mk_real_int64 292L); (mk_real_int64 375L); (mk_real_int64 176L); (mk_real_int64 192L); (mk_real_int64 472L); (mk_real_int64 264L); (mk_real_int64 413L); (mk_real_int64 176L); (mk_real_int64 516L); (mk_real_int64 48L); (mk_real_int64 120L); (mk_real_int64 400L); (mk_real_int64 416L); (mk_real_int64 656L); (mk_real_int64 250L); ]);\r
("y6_lo", [0; 11; 12; 13; 15; 16; 17; 18; 23; 24; 25; 26; 31; 32; 35; 39; 40; 41; 42; 44; 46; 47; 50; 51; 53; 54; 56; 59; 60; ], [(mk_real_int64 292L); (mk_real_int64 79000L); (mk_real_int64 451L); (mk_real_int64 148000L); (mk_real_int64 220L); (mk_real_int64 76116L); (mk_real_int64 245000L); (mk_real_int64 250L); (mk_real_int64 142136L); (mk_real_int64 56000L); (mk_real_int64 250L); (mk_real_int64 230000L); (mk_real_int64 268L); (mk_real_int64 375L); (mk_real_int64 22000L); (mk_real_int64 464L); (mk_real_int64 129L); (mk_real_int64 163808L); (mk_real_int64 250L); (mk_real_int64 220560L); (mk_real_int64 250L); (mk_real_int64 8000L); (mk_real_int64 61083L); (mk_real_int64 165000L); (mk_real_int64 32L); (mk_real_int64 107000L); (mk_real_int64 313000L); (mk_real_int64 352L); (mk_real_int64 121016L); ]);\r
("y6_hi", [11; 13; 19; 26; 28; 29; 34; 36; 37; 38; 43; 47; 48; 51; 52; 54; 55; 56; 57; 58; 61; ], [(mk_real_int64 464L); (mk_real_int64 424L); (mk_real_int64 476L); (mk_real_int64 184L); (mk_real_int64 250L); (mk_real_int64 292L); (mk_real_int64 604L); (mk_real_int64 292L); (mk_real_int64 375L); (mk_real_int64 176L); (mk_real_int64 472L); (mk_real_int64 264L); (mk_real_int64 413L); (mk_real_int64 176L); (mk_real_int64 516L); (mk_real_int64 48L); (mk_real_int64 120L); (mk_real_int64 400L); (mk_real_int64 416L); (mk_real_int64 656L); (mk_real_int64 250L); ]);\r
("ye_hi", [10; 30; 39; 41; 44; 46; ], [(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
("ye_lo", [7; 28; 43; 46; 47; 55; 57; ], [(mk_real_int64 79000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 84000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("yn_lo", [2; 3; 4; 5; 6; 10; 11; 13; ], [(mk_real_int64 956L); (mk_real_int64 956L); (mk_real_int64 837L); (mk_real_int64 956L); (mk_real_int64 1837L); (mk_real_int64 1956L); (mk_real_int64 956L); (mk_real_int64 2044L); ]);\r
("yn_hi", [0; 1; 7; 8; 9; 12; ], [(mk_real_int64 528L); (mk_real_int64 448L); (mk_real_int64 44L); (mk_real_int64 732L); (mk_real_int64 1044L); (mk_real_int64 44L); ]);\r
];;\r
let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
end;;\r
\r
concl (Test_case.result)\r