Update from HH

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

needs "nobranching_lp.hl";;
\r
module Test_case = struct\r
let hypermap_string = "176747399778 21 6 0 1 2 3 4 5 3 0 5 6 3 6 5 4 3 6 4 7 3 7 4 3 3 7 3 8 3 8 3 9 3 9 3 2 3 9 2 10 3 10 2 11 3 11 2 1 3 11 1 12 3 12 1 0 3 12 0 13 3 13 0 6 4 13 6 7 8 3 13 8 14 3 14 8 9 3 14 9 10 4 14 10 11 12 3 12 13 14 ";;\r
let precision = 3;;\r
(***************)\r
(* Constraints *)\r
(***************)\r
let constraints = [\r
("azim_sum_neg", [0; 10; ], [(mk_real_int64 14L); (mk_real_int64 52L); ]);\r
("azim_sum", [8; 13; 14; ], [(mk_real_int64 247L); (mk_real_int64 469L); (mk_real_int64 106L); ]);\r
("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 773L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 979L); (mk_real_int64 826L); (mk_real_int64 826L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 1169L); ]);\r
("sol_sum3_neg", [14; ], [(mk_real_int64 106L); ]);\r
("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; ], [(mk_real_int64 773L); (mk_real_int64 773L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 979L); (mk_real_int64 979L); (mk_real_int64 826L); (mk_real_int64 826L); (mk_real_int64 826L); (mk_real_int64 826L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 979L); (mk_real_int64 826L); (mk_real_int64 1169L); ]);\r
("tau_sum4_neg", [0; 1; ], [(mk_real_int64 1169L); (mk_real_int64 826L); ]);\r
("tau_sum6_neg", [0; ], [(mk_real_int64 1169L); ]);\r
("ln_def_neg", [1; 2; 3; 4; 5; 6; 7; 8; 9; 12; 13; 14; ], [(mk_real_int64 289L); (mk_real_int64 289L); (mk_real_int64 289L); (mk_real_int64 289L); (mk_real_int64 289L); (mk_real_int64 289L); (mk_real_int64 289L); (mk_real_int64 289L); (mk_real_int64 80L); (mk_real_int64 289L); (mk_real_int64 289L); (mk_real_int64 289L); ]);\r
("ln_def", [0; 10; 11; ], [(mk_real_int64 148L); (mk_real_int64 89L); (mk_real_int64 89L); ]);\r
("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 4856L); (mk_real_int64 7345L); (mk_real_int64 7345L); (mk_real_int64 7345L); (mk_real_int64 7345L); (mk_real_int64 7345L); (mk_real_int64 7345L); (mk_real_int64 7345L); (mk_real_int64 7345L); (mk_real_int64 6154L); (mk_real_int64 5191L); (mk_real_int64 5191L); (mk_real_int64 7345L); (mk_real_int64 7345L); (mk_real_int64 7345L); ]);\r
("edge_sym_neg", [1; 7; 13; 17; 19; 22; 23; 26; 28; 29; 38; 41; 43; 44; 53; 54; 57; 60; ], [(mk_real_int64 64L); (mk_real_int64 210L); (mk_real_int64 146L); (mk_real_int64 146L); (mk_real_int64 87L); (mk_real_int64 151L); (mk_real_int64 42L); (mk_real_int64 117L); (mk_real_int64 91L); (mk_real_int64 290L); (mk_real_int64 63L); (mk_real_int64 146L); (mk_real_int64 52L); (mk_real_int64 52L); (mk_real_int64 272L); (mk_real_int64 149L); (mk_real_int64 155L); (mk_real_int64 39L); ]);\r
("edge_sym", [4; 8; 11; 31; 35; 37; 64; ], [(mk_real_int64 61L); (mk_real_int64 199L); (mk_real_int64 146L); (mk_real_int64 130L); (mk_real_int64 64L); (mk_real_int64 146L); (mk_real_int64 101L); ]);\r
("y1_def", [7; 29; 30; ], [(mk_real_int64 7L); (mk_real_int64 26L); (mk_real_int64 26L); ]);\r
("y1_def_neg", [6; 8; 9; 10; 11; 12; 15; 20; 21; 22; 25; 26; 27; 28; 31; 34; 35; 37; 38; 41; 43; 45; 47; 52; 53; 54; 55; 56; 58; 59; 60; 61; 64; 66; 67; ], [(mk_real_int64 227L); (mk_real_int64 372L); (mk_real_int64 111L); (mk_real_int64 34L); (mk_real_int64 159L); (mk_real_int64 210L); (mk_real_int64 210L); (mk_real_int64 171L); (mk_real_int64 114L); (mk_real_int64 126L); (mk_real_int64 67L); (mk_real_int64 253L); (mk_real_int64 92L); (mk_real_int64 354L); (mk_real_int64 91L); (mk_real_int64 5L); (mk_real_int64 111L); (mk_real_int64 354L); (mk_real_int64 206L); (mk_real_int64 210L); (mk_real_int64 75L); (mk_real_int64 75L); (mk_real_int64 167L); (mk_real_int64 61L); (mk_real_int64 33L); (mk_real_int64 140L); (mk_real_int64 139L); (mk_real_int64 254L); (mk_real_int64 230L); (mk_real_int64 92L); (mk_real_int64 123L); (mk_real_int64 30L); (mk_real_int64 49L); (mk_real_int64 127L); (mk_real_int64 25L); ]);\r
("y2_def_neg", [7; 10; 12; 15; 20; 22; 26; 28; 29; 30; 31; 34; 37; 41; 43; 47; 54; 56; 60; 66; ], [(mk_real_int64 2L); (mk_real_int64 43L); (mk_real_int64 210L); (mk_real_int64 210L); (mk_real_int64 135L); (mk_real_int64 44L); (mk_real_int64 86L); (mk_real_int64 24L); (mk_real_int64 8L); (mk_real_int64 8L); (mk_real_int64 47L); (mk_real_int64 5L); (mk_real_int64 24L); (mk_real_int64 210L); (mk_real_int64 75L); (mk_real_int64 167L); (mk_real_int64 140L); (mk_real_int64 31L); (mk_real_int64 157L); (mk_real_int64 68L); ]);\r
("y2_def", [6; 8; 9; 11; 21; 25; 27; 35; 38; 45; 52; 53; 55; 58; 59; 61; 64; 67; ], [(mk_real_int64 138L); (mk_real_int64 10L); (mk_real_int64 68L); (mk_real_int64 97L); (mk_real_int64 69L); (mk_real_int64 41L); (mk_real_int64 56L); (mk_real_int64 67L); (mk_real_int64 125L); (mk_real_int64 116L); (mk_real_int64 94L); (mk_real_int64 52L); (mk_real_int64 107L); (mk_real_int64 163L); (mk_real_int64 56L); (mk_real_int64 39L); (mk_real_int64 63L); (mk_real_int64 38L); ]);\r
("y3_def_neg", [7; 10; 12; 15; 20; 22; 26; 28; 29; 30; 31; 34; 37; 41; 43; 47; 54; 56; 60; 66; ], [(mk_real_int64 2L); (mk_real_int64 43L); (mk_real_int64 210L); (mk_real_int64 210L); (mk_real_int64 135L); (mk_real_int64 44L); (mk_real_int64 86L); (mk_real_int64 24L); (mk_real_int64 8L); (mk_real_int64 8L); (mk_real_int64 47L); (mk_real_int64 5L); (mk_real_int64 24L); (mk_real_int64 210L); (mk_real_int64 75L); (mk_real_int64 167L); (mk_real_int64 140L); (mk_real_int64 31L); (mk_real_int64 157L); (mk_real_int64 68L); ]);\r
("y3_def", [6; 8; 9; 11; 21; 25; 27; 35; 38; 45; 52; 53; 55; 58; 59; 61; 64; 67; ], [(mk_real_int64 138L); (mk_real_int64 10L); (mk_real_int64 68L); (mk_real_int64 97L); (mk_real_int64 69L); (mk_real_int64 41L); (mk_real_int64 56L); (mk_real_int64 67L); (mk_real_int64 125L); (mk_real_int64 116L); (mk_real_int64 94L); (mk_real_int64 52L); (mk_real_int64 107L); (mk_real_int64 163L); (mk_real_int64 56L); (mk_real_int64 39L); (mk_real_int64 63L); (mk_real_int64 38L); ]);\r
("y4_def", [1; 23; 24; ], [(mk_real_int64 10L); (mk_real_int64 40L); (mk_real_int64 40L); ]);\r
("y4_def_neg", [0; 2; 3; 4; 5; 6; 9; 14; 15; 16; 19; 20; 21; 22; 25; 28; 29; 31; 32; 35; 37; 39; 41; 42; 43; 44; 45; 46; 48; 49; 50; 52; 53; ], [(mk_real_int64 259L); (mk_real_int64 364L); (mk_real_int64 127L); (mk_real_int64 18L); (mk_real_int64 182L); (mk_real_int64 146L); (mk_real_int64 146L); (mk_real_int64 151L); (mk_real_int64 130L); (mk_real_int64 110L); (mk_real_int64 76L); (mk_real_int64 222L); (mk_real_int64 105L); (mk_real_int64 338L); (mk_real_int64 76L); (mk_real_int64 3L); (mk_real_int64 126L); (mk_real_int64 338L); (mk_real_int64 235L); (mk_real_int64 146L); (mk_real_int64 52L); (mk_real_int64 218L); (mk_real_int64 116L); (mk_real_int64 178L); (mk_real_int64 97L); (mk_real_int64 146L); (mk_real_int64 202L); (mk_real_int64 263L); (mk_real_int64 307L); (mk_real_int64 105L); (mk_real_int64 63L); (mk_real_int64 140L); (mk_real_int64 72L); ]);\r
("y5_def_neg", [7; 10; 12; 15; 20; 22; 26; 29; 30; 31; 34; 41; 43; 47; 54; 60; 66; ], [(mk_real_int64 2L); (mk_real_int64 31L); (mk_real_int64 146L); (mk_real_int64 146L); (mk_real_int64 87L); (mk_real_int64 21L); (mk_real_int64 41L); (mk_real_int64 8L); (mk_real_int64 8L); (mk_real_int64 27L); (mk_real_int64 3L); (mk_real_int64 146L); (mk_real_int64 52L); (mk_real_int64 116L); (mk_real_int64 146L); (mk_real_int64 111L); (mk_real_int64 36L); ]);\r
("y5_def", [6; 8; 9; 11; 21; 25; 27; 28; 35; 37; 38; 45; 52; 53; 55; 56; 58; 59; 61; 64; 67; ], [(mk_real_int64 138L); (mk_real_int64 51L); (mk_real_int64 68L); (mk_real_int64 97L); (mk_real_int64 69L); (mk_real_int64 41L); (mk_real_int64 56L); (mk_real_int64 21L); (mk_real_int64 67L); (mk_real_int64 21L); (mk_real_int64 125L); (mk_real_int64 116L); (mk_real_int64 94L); (mk_real_int64 52L); (mk_real_int64 107L); (mk_real_int64 7L); (mk_real_int64 163L); (mk_real_int64 56L); (mk_real_int64 39L); (mk_real_int64 63L); (mk_real_int64 38L); ]);\r
("y6_def_neg", [7; 10; 12; 22; 26; 29; 34; 41; 43; 47; 54; 60; ], [(mk_real_int64 2L); (mk_real_int64 31L); (mk_real_int64 146L); (mk_real_int64 21L); (mk_real_int64 41L); (mk_real_int64 8L); (mk_real_int64 3L); (mk_real_int64 146L); (mk_real_int64 52L); (mk_real_int64 116L); (mk_real_int64 146L); (mk_real_int64 97L); ]);\r
("y6_def", [6; 8; 9; 11; 14; 15; 16; 18; 21; 24; 25; 27; 28; 30; 31; 32; 35; 36; 37; 38; 40; 42; 45; 46; 52; 53; 55; 56; 58; 59; 61; 64; 65; 66; 67; ], [(mk_real_int64 366L); (mk_real_int64 51L); (mk_real_int64 422L); (mk_real_int64 97L); (mk_real_int64 146L); (mk_real_int64 146L); (mk_real_int64 146L); (mk_real_int64 297L); (mk_real_int64 108L); (mk_real_int64 332L); (mk_real_int64 41L); (mk_real_int64 56L); (mk_real_int64 21L); (mk_real_int64 119L); (mk_real_int64 90L); (mk_real_int64 84L); (mk_real_int64 67L); (mk_real_int64 149L); (mk_real_int64 21L); (mk_real_int64 275L); (mk_real_int64 146L); (mk_real_int64 198L); (mk_real_int64 168L); (mk_real_int64 135L); (mk_real_int64 94L); (mk_real_int64 52L); (mk_real_int64 265L); (mk_real_int64 244L); (mk_real_int64 163L); (mk_real_int64 708L); (mk_real_int64 39L); (mk_real_int64 63L); (mk_real_int64 161L); (mk_real_int64 110L); (mk_real_int64 38L); ]);\r
("RHA", [6; 9; 11; 22; 25; 26; 31; 34; 35; 61; 64; ], [(mk_real_int64 18L); (mk_real_int64 210L); (mk_real_int64 131L); (mk_real_int64 104L); (mk_real_int64 78L); (mk_real_int64 17L); (mk_real_int64 296L); (mk_real_int64 343L); (mk_real_int64 158L); (mk_real_int64 343L); (mk_real_int64 343L); ]);\r
("RHB", [5; ], [(mk_real_int64 396L); ]);\r
("yy10", [1; ], [(mk_real_int64 64L); ]);\r
("tau4", [0; ], [(mk_real_int64 222L); ]);\r
("tau6", [0; ], [(mk_real_int64 1169L); ]);\r
("ineq105", [10; 13; ], [(mk_real_int64 96L); (mk_real_int64 156L); ]);\r
("ineq106", [0; 2; 3; 5; 15; 16; 19; 20; 21; 22; 25; 29; 31; 32; 45; 46; 48; 49; ], [(mk_real_int64 378L); (mk_real_int64 396L); (mk_real_int64 186L); (mk_real_int64 265L); (mk_real_int64 190L); (mk_real_int64 85L); (mk_real_int64 112L); (mk_real_int64 173L); (mk_real_int64 153L); (mk_real_int64 343L); (mk_real_int64 46L); (mk_real_int64 184L); (mk_real_int64 343L); (mk_real_int64 343L); (mk_real_int64 190L); (mk_real_int64 190L); (mk_real_int64 343L); (mk_real_int64 153L); ]);\r
("ineq107", [1; 4; 23; 24; 50; ], [(mk_real_int64 14L); (mk_real_int64 14L); (mk_real_int64 52L); (mk_real_int64 52L); (mk_real_int64 52L); ]);\r
("ineq108", [14; 39; 42; 43; 45; 46; 48; 52; 53; ], [(mk_real_int64 61L); (mk_real_int64 319L); (mk_real_int64 259L); (mk_real_int64 142L); (mk_real_int64 106L); (mk_real_int64 68L); (mk_real_int64 106L); (mk_real_int64 99L); (mk_real_int64 106L); ]);\r
("ineq110", [44; ], [(mk_real_int64 106L); ]);\r
("ineq111", [2; 4; 6; 9; 14; 16; 20; 22; 25; 28; 31; 35; 37; 41; 44; 46; 50; 52; ], [(mk_real_int64 744L); (mk_real_int64 228L); (mk_real_int64 1169L); (mk_real_int64 1169L); (mk_real_int64 872L); (mk_real_int64 418L); (mk_real_int64 828L); (mk_real_int64 826L); (mk_real_int64 353L); (mk_real_int64 26L); (mk_real_int64 826L); (mk_real_int64 1169L); (mk_real_int64 419L); (mk_real_int64 928L); (mk_real_int64 1002L); (mk_real_int64 693L); (mk_real_int64 826L); (mk_real_int64 576L); ]);\r
("ineq114", [0; 3; 5; 14; 15; 16; 19; 20; 25; 28; 29; 38; 39; 42; 46; 52; ], [(mk_real_int64 29L); (mk_real_int64 336L); (mk_real_int64 209L); (mk_real_int64 297L); (mk_real_int64 395L); (mk_real_int64 167L); (mk_real_int64 124L); (mk_real_int64 26L); (mk_real_int64 473L); (mk_real_int64 547L); (mk_real_int64 253L); (mk_real_int64 750L); (mk_real_int64 241L); (mk_real_int64 167L); (mk_real_int64 287L); (mk_real_int64 593L); ]);\r
("ineq119", [5; ], [(mk_real_int64 114L); ]);\r
("ineq120", [0; 3; 4; 7; ], [(mk_real_int64 620L); (mk_real_int64 327L); (mk_real_int64 465L); (mk_real_int64 247L); ]);\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 2200L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3050L); (mk_real_int64 2575L); (mk_real_int64 2575L); (mk_real_int64 3625L); (mk_real_int64 3625L); (mk_real_int64 3625L); ]);\r
];;\r
\r
(*************************)\r
\r
let variable_bounds = [\r
("azim_hi", [5; 6; 9; 21; 22; 31; 35; 44; 45; 48; 51; 52; 53; 56; 62; 64; 66; ], [(mk_real_int64 479696L); (mk_real_int64 154L); (mk_real_int64 336L); (mk_real_int64 270L); (mk_real_int64 542L); (mk_real_int64 98L); (mk_real_int64 378L); (mk_real_int64 500L); (mk_real_int64 866L); (mk_real_int64 960L); (mk_real_int64 866L); (mk_real_int64 542L); (mk_real_int64 1000L); (mk_real_int64 662L); (mk_real_int64 358L); (mk_real_int64 226L); (mk_real_int64 1218L); ]);\r
("azim_lo", [11; 20; 25; 26; 34; 61; ], [(mk_real_int64 166L); (mk_real_int64 78L); (mk_real_int64 376L); (mk_real_int64 724L); (mk_real_int64 578L); (mk_real_int64 530L); ]);\r
("rhazim_lo", [22; 31; 35; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("rho_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 12; 13; 14; ], [(mk_real_int64 1532L); (mk_real_int64 996L); (mk_real_int64 996L); (mk_real_int64 996L); (mk_real_int64 996L); (mk_real_int64 996L); (mk_real_int64 996L); (mk_real_int64 996L); (mk_real_int64 996L); (mk_real_int64 996L); (mk_real_int64 996L); (mk_real_int64 996L); ]);\r
("rho_lo", [9; 10; 11; ], [(mk_real_int64 1964L); (mk_real_int64 416L); (mk_real_int64 416L); ]);\r
("tau_hi", [6; 17; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
("tau_lo", [7; ], [(mk_real_int64 1000L); ]);\r
("y1_lo", [9; 10; 12; 15; 20; 22; 25; 28; 31; 37; 41; 43; 47; 53; 54; 56; 58; 61; 64; ], [(mk_real_int64 600L); (mk_real_int64 40L); (mk_real_int64 420L); (mk_real_int64 420L); (mk_real_int64 295L); (mk_real_int64 240L); (mk_real_int64 200L); (mk_real_int64 480L); (mk_real_int64 140L); (mk_real_int64 480L); (mk_real_int64 420L); (mk_real_int64 420L); (mk_real_int64 40L); (mk_real_int64 370L); (mk_real_int64 80L); (mk_real_int64 720L); (mk_real_int64 710L); (mk_real_int64 240L); (mk_real_int64 140L); ]);\r
("y1_hi", [6; 8; 26; 27; 34; 35; 38; 45; 52; 55; 59; 60; 66; 67; ], [(mk_real_int64 200L); (mk_real_int64 480L); (mk_real_int64 160L); (mk_real_int64 200L); (mk_real_int64 320L); (mk_real_int64 600L); (mk_real_int64 200L); (mk_real_int64 35L); (mk_real_int64 135L); (mk_real_int64 90L); (mk_real_int64 200L); (mk_real_int64 320L); (mk_real_int64 55L); (mk_real_int64 90L); ]);\r
("y2_lo", [6; 7; 9; 10; 11; 12; 15; 22; 25; 26; 27; 35; 38; 41; 43; 47; 53; 54; 59; 61; 64; ], [(mk_real_int64 408L); (mk_real_int64 128L); (mk_real_int64 296L); (mk_real_int64 168L); (mk_real_int64 540L); (mk_real_int64 420L); (mk_real_int64 420L); (mk_real_int64 300L); (mk_real_int64 232L); (mk_real_int64 68L); (mk_real_int64 308L); (mk_real_int64 24L); (mk_real_int64 148L); (mk_real_int64 420L); (mk_real_int64 420L); (mk_real_int64 40L); (mk_real_int64 312L); (mk_real_int64 80L); (mk_real_int64 308L); (mk_real_int64 408L); (mk_real_int64 288L); ]);\r
("y2_hi", [8; 20; 21; 28; 29; 30; 31; 34; 37; 45; 52; 55; 56; 58; 60; 66; 67; ], [(mk_real_int64 224L); (mk_real_int64 244L); (mk_real_int64 160L); (mk_real_int64 172L); (mk_real_int64 96L); (mk_real_int64 96L); (mk_real_int64 204L); (mk_real_int64 320L); (mk_real_int64 172L); (mk_real_int64 116L); (mk_real_int64 276L); (mk_real_int64 744L); (mk_real_int64 172L); (mk_real_int64 436L); (mk_real_int64 416L); (mk_real_int64 356L); (mk_real_int64 584L); ]);\r
("y3_lo", [6; 7; 9; 10; 11; 12; 15; 22; 25; 26; 27; 35; 38; 41; 43; 47; 53; 54; 59; 61; 64; ], [(mk_real_int64 408L); (mk_real_int64 128L); (mk_real_int64 296L); (mk_real_int64 168L); (mk_real_int64 540L); (mk_real_int64 420L); (mk_real_int64 420L); (mk_real_int64 300L); (mk_real_int64 232L); (mk_real_int64 68L); (mk_real_int64 308L); (mk_real_int64 24L); (mk_real_int64 148L); (mk_real_int64 420L); (mk_real_int64 420L); (mk_real_int64 40L); (mk_real_int64 312L); (mk_real_int64 80L); (mk_real_int64 308L); (mk_real_int64 408L); (mk_real_int64 288L); ]);\r
("y3_hi", [8; 20; 21; 28; 29; 30; 31; 34; 37; 45; 52; 55; 56; 58; 60; 66; 67; ], [(mk_real_int64 224L); (mk_real_int64 244L); (mk_real_int64 160L); (mk_real_int64 172L); (mk_real_int64 96L); (mk_real_int64 96L); (mk_real_int64 204L); (mk_real_int64 320L); (mk_real_int64 172L); (mk_real_int64 116L); (mk_real_int64 276L); (mk_real_int64 744L); (mk_real_int64 172L); (mk_real_int64 436L); (mk_real_int64 416L); (mk_real_int64 356L); (mk_real_int64 584L); ]);\r
("y4_lo", [2; 3; 6; 9; 15; 16; 19; 20; 22; 28; 29; 31; 35; 37; 39; 43; 44; 45; 46; 48; 50; 53; ], [(mk_real_int64 260L); (mk_real_int64 410L); (mk_real_int64 125L); (mk_real_int64 125L); (mk_real_int64 150L); (mk_real_int64 475L); (mk_real_int64 720L); (mk_real_int64 5L); (mk_real_int64 205L); (mk_real_int64 250L); (mk_real_int64 40L); (mk_real_int64 205L); (mk_real_int64 125L); (mk_real_int64 375L); (mk_real_int64 515L); (mk_real_int64 270L); (mk_real_int64 26L); (mk_real_int64 760L); (mk_real_int64 355L); (mk_real_int64 565L); (mk_real_int64 54L); (mk_real_int64 610L); ]);\r
("y4_hi", [0; 1; 4; 5; 14; 21; 23; 24; 25; 32; 42; 49; 52; ], [(mk_real_int64 70L); (mk_real_int64 822L); (mk_real_int64 322L); (mk_real_int64 475L); (mk_real_int64 215L); (mk_real_int64 195L); (mk_real_int64 196L); (mk_real_int64 196L); (mk_real_int64 365L); (mk_real_int64 45L); (mk_real_int64 585L); (mk_real_int64 195L); (mk_real_int64 185L); ]);\r
("y5_lo", [6; 7; 9; 11; 12; 15; 22; 25; 27; 31; 34; 35; 38; 41; 43; 53; 54; 59; 60; 61; 64; ], [(mk_real_int64 408L); (mk_real_int64 128L); (mk_real_int64 296L); (mk_real_int64 540L); (mk_real_int64 125L); (mk_real_int64 125L); (mk_real_int64 310L); (mk_real_int64 232L); (mk_real_int64 308L); (mk_real_int64 381L); (mk_real_int64 250L); (mk_real_int64 24L); (mk_real_int64 148L); (mk_real_int64 125L); (mk_real_int64 375L); (mk_real_int64 312L); (mk_real_int64 26L); (mk_real_int64 308L); (mk_real_int64 154L); (mk_real_int64 408L); (mk_real_int64 288L); ]);\r
("y5_hi", [8; 10; 20; 21; 26; 28; 29; 30; 37; 45; 52; 55; 56; 58; 66; 67; ], [(mk_real_int64 144L); (mk_real_int64 372L); (mk_real_int64 204L); (mk_real_int64 160L); (mk_real_int64 472L); (mk_real_int64 602L); (mk_real_int64 96L); (mk_real_int64 96L); (mk_real_int64 602L); (mk_real_int64 116L); (mk_real_int64 276L); (mk_real_int64 744L); (mk_real_int64 287L); (mk_real_int64 436L); (mk_real_int64 36L); (mk_real_int64 584L); ]);\r
("y6_lo", [6; 7; 9; 11; 12; 14; 15; 16; 18; 20; 21; 22; 24; 25; 27; 30; 31; 32; 34; 35; 36; 38; 40; 41; 42; 43; 45; 46; 53; 54; 55; 56; 59; 60; 61; 64; 65; 66; ], [(mk_real_int64 229000L); (mk_real_int64 128L); (mk_real_int64 354296L); (mk_real_int64 540L); (mk_real_int64 125L); (mk_real_int64 146000L); (mk_real_int64 292125L); (mk_real_int64 146000L); (mk_real_int64 297000L); (mk_real_int64 87000L); (mk_real_int64 39000L); (mk_real_int64 310L); (mk_real_int64 332000L); (mk_real_int64 232L); (mk_real_int64 308L); (mk_real_int64 126904L); (mk_real_int64 117381L); (mk_real_int64 84000L); (mk_real_int64 250L); (mk_real_int64 24L); (mk_real_int64 149000L); (mk_real_int64 151000L); (mk_real_int64 146000L); (mk_real_int64 125L); (mk_real_int64 198000L); (mk_real_int64 375L); (mk_real_int64 52000L); (mk_real_int64 135000L); (mk_real_int64 312L); (mk_real_int64 26L); (mk_real_int64 157256L); (mk_real_int64 237000L); (mk_real_int64 653000L); (mk_real_int64 14154L); (mk_real_int64 408L); (mk_real_int64 288L); (mk_real_int64 161000L); (mk_real_int64 146000L); ]);\r
("y6_hi", [6; 8; 10; 20; 21; 26; 28; 29; 37; 38; 45; 52; 56; 58; 59; 66; 67; ], [(mk_real_int64 592L); (mk_real_int64 144L); (mk_real_int64 372L); (mk_real_int64 204L); (mk_real_int64 160L); (mk_real_int64 472L); (mk_real_int64 602L); (mk_real_int64 96L); (mk_real_int64 602L); (mk_real_int64 852L); (mk_real_int64 116L); (mk_real_int64 276L); (mk_real_int64 287L); (mk_real_int64 436L); (mk_real_int64 692L); (mk_real_int64 36L); (mk_real_int64 584L); ]);\r
("ye_hi", [11; 23; 30; 33; 58; 64; 65; ], [(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
("ye_lo", [4; 9; 28; 36; 57; 66; 67; ], [(mk_real_int64 61000L); (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", [0; 1; 2; 3; 4; 5; 6; 7; 8; 10; 12; 13; 14; ], [(mk_real_int64 1396L); (mk_real_int64 2036L); (mk_real_int64 1036L); (mk_real_int64 1036L); (mk_real_int64 1036L); (mk_real_int64 1036L); (mk_real_int64 2036L); (mk_real_int64 1036L); (mk_real_int64 1036L); (mk_real_int64 853L); (mk_real_int64 1036L); (mk_real_int64 1036L); (mk_real_int64 1036L); ]);\r
("yn_lo", [9; 11; ], [(mk_real_int64 80L); (mk_real_int64 147L); ]);\r
];;\r
let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
end;;\r
\r
concl (Test_case.result)\r