needs "nobranching_lp.hl";; module Test_case = struct let hypermap_string = "95170601659 18 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 1 3 10 1 0 4 10 0 11 12 3 11 0 6 3 11 6 7 3 11 7 8 3 12 11 8 3 12 8 9 3 9 10 12 ";; let precision = 3;; (***************) (* Constraints *) (***************) let constraints = [ ("azim_sum_neg", [0; 4; 6; 7; 9; 10; 12; ], [(mk_real_int64 476L); (mk_real_int64 362L); (mk_real_int64 181L); (mk_real_int64 52L); (mk_real_int64 234L); (mk_real_int64 18L); (mk_real_int64 408L); ]); ("azim_sum", [2; 8; ], [(mk_real_int64 83L); (mk_real_int64 13L); ]); ("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 885L); (mk_real_int64 885L); (mk_real_int64 1014L); (mk_real_int64 885L); (mk_real_int64 885L); (mk_real_int64 919L); (mk_real_int64 885L); (mk_real_int64 955L); (mk_real_int64 919L); (mk_real_int64 919L); (mk_real_int64 923L); (mk_real_int64 919L); (mk_real_int64 919L); ]); ("sol_sum3", [0; 1; 13; 14; 15; ], [(mk_real_int64 181L); (mk_real_int64 251L); (mk_real_int64 238L); (mk_real_int64 267L); (mk_real_int64 51L); ]); ("sol_sum3_neg", [2; 3; 6; 7; 10; 11; 12; ], [(mk_real_int64 256L); (mk_real_int64 70L); (mk_real_int64 48L); (mk_real_int64 576L); (mk_real_int64 337L); (mk_real_int64 19L); (mk_real_int64 278L); ]); ("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; ], [(mk_real_int64 885L); (mk_real_int64 885L); (mk_real_int64 448L); (mk_real_int64 815L); (mk_real_int64 742L); (mk_real_int64 906L); (mk_real_int64 837L); (mk_real_int64 309L); (mk_real_int64 885L); (mk_real_int64 885L); (mk_real_int64 370L); (mk_real_int64 885L); (mk_real_int64 499L); (mk_real_int64 919L); (mk_real_int64 919L); (mk_real_int64 919L); ]); ("tau_sum4_neg", [0; ], [(mk_real_int64 919L); ]); ("tau_sum6_neg", [0; ], [(mk_real_int64 885L); ]); ("ln_def_neg", [2; 5; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 118L); (mk_real_int64 13L); (mk_real_int64 53L); (mk_real_int64 13L); (mk_real_int64 13L); (mk_real_int64 18L); (mk_real_int64 13L); (mk_real_int64 13L); ]); ("ln_def", [0; 1; 3; 4; 6; ], [(mk_real_int64 25L); (mk_real_int64 25L); (mk_real_int64 25L); (mk_real_int64 25L); (mk_real_int64 25L); ]); ("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 5558L); (mk_real_int64 5558L); (mk_real_int64 6374L); (mk_real_int64 5558L); (mk_real_int64 5558L); (mk_real_int64 5773L); (mk_real_int64 5558L); (mk_real_int64 6003L); (mk_real_int64 5773L); (mk_real_int64 5773L); (mk_real_int64 5802L); (mk_real_int64 5773L); (mk_real_int64 5773L); ]); ("edge_sym", [0; 2; 3; 5; 8; 11; 13; 14; 20; 22; 39; 42; 54; ], [(mk_real_int64 14L); (mk_real_int64 86L); (mk_real_int64 86L); (mk_real_int64 14L); (mk_real_int64 225L); (mk_real_int64 209L); (mk_real_int64 12L); (mk_real_int64 12L); (mk_real_int64 13L); (mk_real_int64 64L); (mk_real_int64 7L); (mk_real_int64 12L); (mk_real_int64 7L); ]); ("edge_sym_neg", [17; 19; 23; 26; 28; 29; 32; 37; 45; 48; 51; ], [(mk_real_int64 66L); (mk_real_int64 60L); (mk_real_int64 138L); (mk_real_int64 64L); (mk_real_int64 159L); (mk_real_int64 137L); (mk_real_int64 122L); (mk_real_int64 14L); (mk_real_int64 12L); (mk_real_int64 145L); (mk_real_int64 13L); ]); ("y1_def_neg", [0; 3; 6; 8; 14; 17; 18; 19; 22; 23; 24; 27; 31; 35; 40; 41; 45; 50; 51; 53; 54; 56; ], [(mk_real_int64 11L); (mk_real_int64 67L); (mk_real_int64 128L); (mk_real_int64 27L); (mk_real_int64 147L); (mk_real_int64 85L); (mk_real_int64 42L); (mk_real_int64 5L); (mk_real_int64 44L); (mk_real_int64 11L); (mk_real_int64 76L); (mk_real_int64 13L); (mk_real_int64 109L); (mk_real_int64 16L); (mk_real_int64 8L); (mk_real_int64 5L); (mk_real_int64 12L); (mk_real_int64 92L); (mk_real_int64 36L); (mk_real_int64 40L); (mk_real_int64 83L); (mk_real_int64 8L); ]); ("y1_def", [7; 10; 13; 15; 20; 21; 29; 32; 34; 42; 43; 47; 48; 49; 52; 57; ], [(mk_real_int64 148L); (mk_real_int64 8L); (mk_real_int64 97L); (mk_real_int64 22L); (mk_real_int64 29L); (mk_real_int64 2L); (mk_real_int64 173L); (mk_real_int64 152L); (mk_real_int64 7L); (mk_real_int64 1L); (mk_real_int64 7L); (mk_real_int64 76L); (mk_real_int64 14L); (mk_real_int64 85L); (mk_real_int64 71L); (mk_real_int64 78L); ]); ("y2_def", [0; 3; 13; 14; 15; 18; 22; 27; 29; 40; 43; 47; ], [(mk_real_int64 14L); (mk_real_int64 86L); (mk_real_int64 97L); (mk_real_int64 56L); (mk_real_int64 33L); (mk_real_int64 25L); (mk_real_int64 69L); (mk_real_int64 8L); (mk_real_int64 173L); (mk_real_int64 210L); (mk_real_int64 7L); (mk_real_int64 151L); ]); ("y2_def_neg", [6; 7; 8; 10; 17; 19; 20; 21; 23; 24; 31; 32; 34; 35; 41; 45; 48; 49; 50; 51; 52; 53; 54; 56; 57; ], [(mk_real_int64 95L); (mk_real_int64 45L); (mk_real_int64 27L); (mk_real_int64 139L); (mk_real_int64 85L); (mk_real_int64 5L); (mk_real_int64 9L); (mk_real_int64 1L); (mk_real_int64 11L); (mk_real_int64 64L); (mk_real_int64 109L); (mk_real_int64 46L); (mk_real_int64 2L); (mk_real_int64 16L); (mk_real_int64 5L); (mk_real_int64 12L); (mk_real_int64 4L); (mk_real_int64 26L); (mk_real_int64 92L); (mk_real_int64 36L); (mk_real_int64 21L); (mk_real_int64 40L); (mk_real_int64 83L); (mk_real_int64 8L); (mk_real_int64 24L); ]); ("y3_def", [0; 3; 13; 14; 15; 18; 22; 27; 29; 40; 43; 47; ], [(mk_real_int64 14L); (mk_real_int64 86L); (mk_real_int64 97L); (mk_real_int64 56L); (mk_real_int64 33L); (mk_real_int64 25L); (mk_real_int64 69L); (mk_real_int64 8L); (mk_real_int64 173L); (mk_real_int64 210L); (mk_real_int64 7L); (mk_real_int64 151L); ]); ("y3_def_neg", [6; 7; 8; 10; 17; 19; 20; 21; 23; 24; 31; 32; 34; 35; 41; 45; 48; 49; 50; 51; 52; 53; 54; 56; 57; ], [(mk_real_int64 95L); (mk_real_int64 45L); (mk_real_int64 27L); (mk_real_int64 139L); (mk_real_int64 85L); (mk_real_int64 5L); (mk_real_int64 9L); (mk_real_int64 1L); (mk_real_int64 11L); (mk_real_int64 64L); (mk_real_int64 109L); (mk_real_int64 46L); (mk_real_int64 2L); (mk_real_int64 16L); (mk_real_int64 5L); (mk_real_int64 12L); (mk_real_int64 4L); (mk_real_int64 26L); (mk_real_int64 92L); (mk_real_int64 36L); (mk_real_int64 21L); (mk_real_int64 40L); (mk_real_int64 83L); (mk_real_int64 8L); (mk_real_int64 24L); ]); ("y4_def", [1; 2; 4; 14; 15; 26; 28; 32; 38; 39; 41; 42; 43; 46; 47; ], [(mk_real_int64 228L); (mk_real_int64 58L); (mk_real_int64 209L); (mk_real_int64 44L); (mk_real_int64 3L); (mk_real_int64 235L); (mk_real_int64 11L); (mk_real_int64 2L); (mk_real_int64 21L); (mk_real_int64 131L); (mk_real_int64 77L); (mk_real_int64 109L); (mk_real_int64 86L); (mk_real_int64 16L); (mk_real_int64 121L); ]); ("y4_def_neg", [0; 7; 8; 9; 11; 12; 13; 16; 17; 18; 21; 23; 25; 29; 30; 31; 33; 35; 37; 40; 44; ], [(mk_real_int64 98L); (mk_real_int64 50L); (mk_real_int64 159L); (mk_real_int64 26L); (mk_real_int64 59L); (mk_real_int64 48L); (mk_real_int64 4L); (mk_real_int64 129L); (mk_real_int64 8L); (mk_real_int64 86L); (mk_real_int64 14L); (mk_real_int64 145L); (mk_real_int64 76L); (mk_real_int64 11L); (mk_real_int64 221L); (mk_real_int64 4L); (mk_real_int64 4L); (mk_real_int64 9L); (mk_real_int64 141L); (mk_real_int64 64L); (mk_real_int64 58L); ]); ("y5_def", [0; 3; 8; 14; 18; 22; 27; 36; 40; 51; 53; 56; ], [(mk_real_int64 14L); (mk_real_int64 86L); (mk_real_int64 58L); (mk_real_int64 62L); (mk_real_int64 25L); (mk_real_int64 69L); (mk_real_int64 8L); (mk_real_int64 7L); (mk_real_int64 16L); (mk_real_int64 77L); (mk_real_int64 86L); (mk_real_int64 16L); ]); ("y5_def_neg", [6; 7; 13; 15; 17; 19; 20; 21; 23; 24; 29; 31; 32; 34; 35; 41; 43; 45; 47; 48; 49; 50; 52; 54; 57; ], [(mk_real_int64 62L); (mk_real_int64 45L); (mk_real_int64 50L); (mk_real_int64 7L); (mk_real_int64 59L); (mk_real_int64 4L); (mk_real_int64 9L); (mk_real_int64 1L); (mk_real_int64 8L); (mk_real_int64 64L); (mk_real_int64 145L); (mk_real_int64 76L); (mk_real_int64 46L); (mk_real_int64 2L); (mk_real_int64 11L); (mk_real_int64 4L); (mk_real_int64 4L); (mk_real_int64 9L); (mk_real_int64 9L); (mk_real_int64 4L); (mk_real_int64 26L); (mk_real_int64 64L); (mk_real_int64 21L); (mk_real_int64 58L); (mk_real_int64 24L); ]); ("y6_def", [0; 3; 8; 14; 15; 18; 22; 27; 31; 33; 40; 51; 53; 56; ], [(mk_real_int64 14L); (mk_real_int64 86L); (mk_real_int64 58L); (mk_real_int64 62L); (mk_real_int64 47L); (mk_real_int64 25L); (mk_real_int64 69L); (mk_real_int64 208L); (mk_real_int64 46L); (mk_real_int64 136L); (mk_real_int64 16L); (mk_real_int64 77L); (mk_real_int64 86L); (mk_real_int64 16L); ]); ("y6_def_neg", [6; 7; 13; 17; 19; 20; 21; 23; 24; 29; 32; 34; 35; 41; 43; 45; 47; 48; 49; 50; 52; 54; 57; ], [(mk_real_int64 27L); (mk_real_int64 45L); (mk_real_int64 50L); (mk_real_int64 59L); (mk_real_int64 4L); (mk_real_int64 9L); (mk_real_int64 1L); (mk_real_int64 8L); (mk_real_int64 64L); (mk_real_int64 145L); (mk_real_int64 46L); (mk_real_int64 2L); (mk_real_int64 11L); (mk_real_int64 4L); (mk_real_int64 4L); (mk_real_int64 9L); (mk_real_int64 9L); (mk_real_int64 4L); (mk_real_int64 13L); (mk_real_int64 64L); (mk_real_int64 16L); (mk_real_int64 58L); (mk_real_int64 24L); ]); ("RHA", [0; 3; 12; 13; 14; 15; 16; 17; 18; 19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 33; 35; 40; 41; 42; 43; 45; 46; 47; 48; 54; 55; ], [(mk_real_int64 34L); (mk_real_int64 130L); (mk_real_int64 436L); (mk_real_int64 436L); (mk_real_int64 296L); (mk_real_int64 140L); (mk_real_int64 70L); (mk_real_int64 199L); (mk_real_int64 143L); (mk_real_int64 272L); (mk_real_int64 176L); (mk_real_int64 13L); (mk_real_int64 109L); (mk_real_int64 18L); (mk_real_int64 87L); (mk_real_int64 178L); (mk_real_int64 48L); (mk_real_int64 593L); (mk_real_int64 576L); (mk_real_int64 610L); (mk_real_int64 34L); (mk_real_int64 34L); (mk_real_int64 34L); (mk_real_int64 323L); (mk_real_int64 549L); (mk_real_int64 515L); (mk_real_int64 34L); (mk_real_int64 71L); (mk_real_int64 419L); (mk_real_int64 456L); (mk_real_int64 419L); (mk_real_int64 5L); (mk_real_int64 5L); ]); ("yy10", [37; ], [(mk_real_int64 14L); ]); ("tau6", [0; ], [(mk_real_int64 885L); ]); ("ineq105", [0; 3; ], [(mk_real_int64 34L); (mk_real_int64 213L); ]); ("ineq106", [0; 8; 12; 21; 30; ], [(mk_real_int64 34L); (mk_real_int64 211L); (mk_real_int64 70L); (mk_real_int64 21L); (mk_real_int64 226L); ]); ("ineq107", [1; 4; 14; 15; 26; 28; 32; 38; 39; 42; 47; ], [(mk_real_int64 296L); (mk_real_int64 226L); (mk_real_int64 57L); (mk_real_int64 4L); (mk_real_int64 304L); (mk_real_int64 15L); (mk_real_int64 2L); (mk_real_int64 27L); (mk_real_int64 170L); (mk_real_int64 141L); (mk_real_int64 156L); ]); ("ineq108", [9; 16; 18; 37; ], [(mk_real_int64 19L); (mk_real_int64 189L); (mk_real_int64 21L); (mk_real_int64 125L); ]); ("ineq109", [2; 4; 41; 43; 46; ], [(mk_real_int64 181L); (mk_real_int64 251L); (mk_real_int64 238L); (mk_real_int64 267L); (mk_real_int64 51L); ]); ("ineq110", [7; 9; 18; 23; 30; 33; 37; ], [(mk_real_int64 256L); (mk_real_int64 70L); (mk_real_int64 48L); (mk_real_int64 576L); (mk_real_int64 337L); (mk_real_int64 19L); (mk_real_int64 278L); ]); ("ineq111", [0; 4; 8; 11; 13; 17; 18; 23; 25; 29; 31; 35; 40; 44; ], [(mk_real_int64 596L); (mk_real_int64 373L); (mk_real_int64 115L); (mk_real_int64 474L); (mk_real_int64 29L); (mk_real_int64 63L); (mk_real_int64 496L); (mk_real_int64 255L); (mk_real_int64 606L); (mk_real_int64 92L); (mk_real_int64 30L); (mk_real_int64 69L); (mk_real_int64 510L); (mk_real_int64 460L); ]); ("ineq112", [28; ], [(mk_real_int64 684L); ]); ("ineq113", [8; 15; 26; 34; 38; 47; ], [(mk_real_int64 44L); (mk_real_int64 837L); (mk_real_int64 224L); (mk_real_int64 770L); (mk_real_int64 253L); (mk_real_int64 777L); ]); ("ineq114", [0; 3; 5; 7; 11; 12; 13; 16; 19; 23; 24; 27; 29; 31; 33; 36; 40; 41; 43; 44; 45; 46; ], [(mk_real_int64 289L); (mk_real_int64 111L); (mk_real_int64 400L); (mk_real_int64 289L); (mk_real_int64 341L); (mk_real_int64 145L); (mk_real_int64 568L); (mk_real_int64 5L); (mk_real_int64 341L); (mk_real_int64 54L); (mk_real_int64 54L); (mk_real_int64 54L); (mk_real_int64 54L); (mk_real_int64 340L); (mk_real_int64 46L); (mk_real_int64 247L); (mk_real_int64 402L); (mk_real_int64 7L); (mk_real_int64 53L); (mk_real_int64 405L); (mk_real_int64 60L); (mk_real_int64 81L); ]); ("ineq119", [3; ], [(mk_real_int64 901L); ]); ("ineq120", [2; ], [(mk_real_int64 18L); ]); ];; (***************) (* Variables *) (***************) let target_variables = [ ("ln_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 2350L); (mk_real_int64 2350L); (mk_real_int64 2550L); (mk_real_int64 2350L); (mk_real_int64 2350L); (mk_real_int64 2725L); (mk_real_int64 2350L); (mk_real_int64 2475L); (mk_real_int64 2725L); (mk_real_int64 2725L); (mk_real_int64 2650L); (mk_real_int64 2725L); (mk_real_int64 2725L); ]); ];; (*************************) let variable_bounds = [ ("azim_lo", [6; 7; 9; 10; 11; 18; 29; 30; 32; 33; 35; 39; 47; 54; 55; 56; 57; ], [(mk_real_int64 86L); (mk_real_int64 1000L); (mk_real_int64 514L); (mk_real_int64 1000L); (mk_real_int64 600L); (mk_real_int64 230L); (mk_real_int64 196L); (mk_real_int64 196L); (mk_real_int64 16L); (mk_real_int64 196L); (mk_real_int64 196L); (mk_real_int64 153L); (mk_real_int64 1000L); (mk_real_int64 470L); (mk_real_int64 440L); (mk_real_int64 294L); (mk_real_int64 243L); ]); ("azim_hi", [1; 5; 12; 13; 14; 15; 17; 19; 20; 21; 22; 25; 27; 34; 38; 40; 41; 42; 43; 44; 46; 48; 50; 51; 53; ], [(mk_real_int64 362000L); (mk_real_int64 476000L); (mk_real_int64 1000L); (mk_real_int64 914L); (mk_real_int64 604L); (mk_real_int64 1000L); (mk_real_int64 1466L); (mk_real_int64 568L); (mk_real_int64 1000L); (mk_real_int64 217L); (mk_real_int64 130L); (mk_real_int64 466L); (mk_real_int64 1000L); (mk_real_int64 212L); (mk_real_int64 644L); (mk_real_int64 1000L); (mk_real_int64 840L); (mk_real_int64 1000L); (mk_real_int64 796L); (mk_real_int64 570L); (mk_real_int64 622L); (mk_real_int64 473L); (mk_real_int64 652L); (mk_real_int64 382L); (mk_real_int64 178L); ]); ("rhazim_lo", [12; 13; 20; 46; 48; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]); ("rhazim_hi", [3; 22; 23; 24; 25; 45; 54; 55; ], [(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); ]); ("rho_hi", [0; 1; 3; 4; 5; 6; 8; 9; 11; 12; ], [(mk_real_int64 3340L); (mk_real_int64 3340L); (mk_real_int64 3340L); (mk_real_int64 3340L); (mk_real_int64 1996L); (mk_real_int64 3340L); (mk_real_int64 1996L); (mk_real_int64 1996L); (mk_real_int64 1996L); (mk_real_int64 1996L); ]); ("rho_lo", [2; 7; 10; ], [(mk_real_int64 2024L); (mk_real_int64 1780L); (mk_real_int64 1868L); ]); ("tau_lo", [2; 6; 9; 10; 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); ]); ("tau_hi", [14; ], [(mk_real_int64 1000L); ]); ("y1_hi", [0; 6; 13; 15; 24; 27; 34; 40; 43; 47; 50; 51; 54; 56; ], [(mk_real_int64 290L); (mk_real_int64 320L); (mk_real_int64 280L); (mk_real_int64 135L); (mk_real_int64 25L); (mk_real_int64 400L); (mk_real_int64 500L); (mk_real_int64 460L); (mk_real_int64 220L); (mk_real_int64 265L); (mk_real_int64 200L); (mk_real_int64 62L); (mk_real_int64 200L); (mk_real_int64 299L); ]); ("y1_lo", [3; 8; 10; 14; 17; 19; 20; 22; 23; 29; 31; 35; 41; 45; 48; 52; 53; ], [(mk_real_int64 95L); (mk_real_int64 331L); (mk_real_int64 41L); (mk_real_int64 300L); (mk_real_int64 320L); (mk_real_int64 220L); (mk_real_int64 500L); (mk_real_int64 415L); (mk_real_int64 340L); (mk_real_int64 20L); (mk_real_int64 80L); (mk_real_int64 560L); (mk_real_int64 400L); (mk_real_int64 420L); (mk_real_int64 500L); (mk_real_int64 500L); (mk_real_int64 317L); ]); ("y2_lo", [0; 3; 8; 10; 17; 19; 22; 23; 27; 29; 31; 32; 34; 35; 41; 42; 45; 48; 52; 53; ], [(mk_real_int64 332L); (mk_real_int64 374L); (mk_real_int64 331L); (mk_real_int64 393L); (mk_real_int64 320L); (mk_real_int64 220L); (mk_real_int64 204L); (mk_real_int64 340L); (mk_real_int64 356L); (mk_real_int64 20L); (mk_real_int64 80L); (mk_real_int64 208L); (mk_real_int64 280L); (mk_real_int64 560L); (mk_real_int64 400L); (mk_real_int64 304L); (mk_real_int64 420L); (mk_real_int64 104L); (mk_real_int64 432L); (mk_real_int64 317L); ]); ("y2_hi", [6; 7; 13; 14; 15; 18; 20; 21; 24; 40; 43; 47; 49; 50; 51; 54; 56; 57; ], [(mk_real_int64 96L); (mk_real_int64 8L); (mk_real_int64 280L); (mk_real_int64 104L); (mk_real_int64 516L); (mk_real_int64 480L); (mk_real_int64 336L); (mk_real_int64 392L); (mk_real_int64 604L); (mk_real_int64 324L); (mk_real_int64 220L); (mk_real_int64 140L); (mk_real_int64 160L); (mk_real_int64 200L); (mk_real_int64 62L); (mk_real_int64 200L); (mk_real_int64 299L); (mk_real_int64 288L); ]); ("y3_lo", [0; 3; 8; 10; 17; 19; 22; 23; 27; 29; 31; 32; 34; 35; 41; 42; 45; 48; 52; 53; ], [(mk_real_int64 332L); (mk_real_int64 374L); (mk_real_int64 331L); (mk_real_int64 393L); (mk_real_int64 320L); (mk_real_int64 220L); (mk_real_int64 204L); (mk_real_int64 340L); (mk_real_int64 356L); (mk_real_int64 20L); (mk_real_int64 80L); (mk_real_int64 208L); (mk_real_int64 280L); (mk_real_int64 560L); (mk_real_int64 400L); (mk_real_int64 304L); (mk_real_int64 420L); (mk_real_int64 104L); (mk_real_int64 432L); (mk_real_int64 317L); ]); ("y3_hi", [6; 7; 13; 14; 15; 18; 20; 21; 24; 40; 43; 47; 49; 50; 51; 54; 56; 57; ], [(mk_real_int64 96L); (mk_real_int64 8L); (mk_real_int64 280L); (mk_real_int64 104L); (mk_real_int64 516L); (mk_real_int64 480L); (mk_real_int64 336L); (mk_real_int64 392L); (mk_real_int64 604L); (mk_real_int64 324L); (mk_real_int64 220L); (mk_real_int64 140L); (mk_real_int64 160L); (mk_real_int64 200L); (mk_real_int64 62L); (mk_real_int64 200L); (mk_real_int64 299L); (mk_real_int64 288L); ]); ("y4_lo", [7; 9; 11; 16; 21; 26; 29; 32; 38; 42; 47; ], [(mk_real_int64 176L); (mk_real_int64 735L); (mk_real_int64 250L); (mk_real_int64 465L); (mk_real_int64 385L); (mk_real_int64 8L); (mk_real_int64 500L); (mk_real_int64 454L); (mk_real_int64 129L); (mk_real_int64 7L); (mk_real_int64 412L); ]); ("y4_hi", [0; 1; 2; 4; 8; 12; 13; 14; 15; 17; 18; 23; 25; 28; 30; 31; 33; 35; 37; 39; 40; 41; 43; 44; 46; ], [(mk_real_int64 210L); (mk_real_int64 808L); (mk_real_int64 644L); (mk_real_int64 397L); (mk_real_int64 90L); (mk_real_int64 50L); (mk_real_int64 375L); (mk_real_int64 61L); (mk_real_int64 92L); (mk_real_int64 125L); (mk_real_int64 207L); (mk_real_int64 229L); (mk_real_int64 250L); (mk_real_int64 595L); (mk_real_int64 138L); (mk_real_int64 250L); (mk_real_int64 276L); (mk_real_int64 375L); (mk_real_int64 887L); (mk_real_int64 410L); (mk_real_int64 250L); (mk_real_int64 112L); (mk_real_int64 508L); (mk_real_int64 500L); (mk_real_int64 524L); ]); ("y5_lo", [0; 3; 6; 13; 17; 22; 27; 32; 34; 35; 36; 42; 48; 52; ], [(mk_real_int64 332L); (mk_real_int64 374L); (mk_real_int64 124L); (mk_real_int64 176L); (mk_real_int64 250L); (mk_real_int64 204L); (mk_real_int64 356L); (mk_real_int64 208L); (mk_real_int64 280L); (mk_real_int64 500L); (mk_real_int64 7000L); (mk_real_int64 304L); (mk_real_int64 104L); (mk_real_int64 432L); ]); ("y5_hi", [7; 8; 10; 14; 15; 18; 19; 20; 21; 23; 24; 29; 31; 40; 41; 43; 45; 47; 49; 50; 51; 53; 54; 56; 57; ], [(mk_real_int64 8L); (mk_real_int64 644L); (mk_real_int64 347L); (mk_real_int64 429L); (mk_real_int64 196L); (mk_real_int64 480L); (mk_real_int64 375L); (mk_real_int64 336L); (mk_real_int64 392L); (mk_real_int64 125L); (mk_real_int64 236L); (mk_real_int64 229L); (mk_real_int64 250L); (mk_real_int64 212L); (mk_real_int64 250L); (mk_real_int64 276L); (mk_real_int64 375L); (mk_real_int64 12L); (mk_real_int64 160L); (mk_real_int64 250L); (mk_real_int64 112L); (mk_real_int64 508L); (mk_real_int64 500L); (mk_real_int64 524L); (mk_real_int64 288L); ]); ("y6_lo", [0; 3; 6; 13; 15; 17; 22; 27; 31; 32; 33; 34; 35; 42; 48; 49; 52; ], [(mk_real_int64 332L); (mk_real_int64 374L); (mk_real_int64 35124L); (mk_real_int64 176L); (mk_real_int64 54000L); (mk_real_int64 250L); (mk_real_int64 204L); (mk_real_int64 201000L); (mk_real_int64 122000L); (mk_real_int64 208L); (mk_real_int64 136000L); (mk_real_int64 280L); (mk_real_int64 500L); (mk_real_int64 304L); (mk_real_int64 104L); (mk_real_int64 13000L); (mk_real_int64 5432L); ]); ("y6_hi", [7; 8; 10; 14; 15; 18; 19; 20; 21; 23; 24; 27; 29; 31; 40; 41; 43; 45; 47; 49; 50; 51; 53; 54; 56; 57; ], [(mk_real_int64 8L); (mk_real_int64 644L); (mk_real_int64 347L); (mk_real_int64 429L); (mk_real_int64 196L); (mk_real_int64 480L); (mk_real_int64 375L); (mk_real_int64 336L); (mk_real_int64 392L); (mk_real_int64 125L); (mk_real_int64 236L); (mk_real_int64 644L); (mk_real_int64 229L); (mk_real_int64 250L); (mk_real_int64 212L); (mk_real_int64 250L); (mk_real_int64 276L); (mk_real_int64 375L); (mk_real_int64 12L); (mk_real_int64 160L); (mk_real_int64 250L); (mk_real_int64 112L); (mk_real_int64 508L); (mk_real_int64 500L); (mk_real_int64 524L); (mk_real_int64 288L); ]); ("ye_hi", [16; 33; 34; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]); ("ye_lo", [7; 8; 18; 19; 20; 27; 43; 44; 45; 50; 52; 53; 56; 57; ], [(mk_real_int64 85000L); (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); (mk_real_int64 1000L); ]); ("yn_hi", [5; 8; 9; 11; 12; ], [(mk_real_int64 1012L); (mk_real_int64 12L); (mk_real_int64 1012L); (mk_real_int64 1012L); (mk_real_int64 12L); ]); ("yn_lo", [0; 1; 2; 3; 4; 6; 7; 10; ], [(mk_real_int64 75L); (mk_real_int64 75L); (mk_real_int64 968L); (mk_real_int64 75L); (mk_real_int64 75L); (mk_real_int64 75L); (mk_real_int64 28L); (mk_real_int64 368L); ]); ];;end;; concl (Test_case.result)let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;