needs "nobranching_lp.hl";; module Test_case = struct let hypermap_string = "219955817888 20 4 0 1 2 3 4 0 3 4 5 3 4 3 6 3 6 3 2 3 6 2 7 3 7 2 1 4 7 1 8 9 3 8 1 0 3 8 0 10 3 10 0 5 3 10 5 11 3 11 5 4 3 11 4 12 3 12 4 6 4 12 6 7 9 3 9 8 13 3 13 8 10 3 13 10 11 3 13 11 12 3 12 9 13 ";; let precision = 4;; (***************) (* Constraints *) (***************) let constraints = [ ("azim_sum", [3; 5; 6; 8; 9; 11; ], [(mk_real_int64 5039L); (mk_real_int64 1787L); (mk_real_int64 1787L); (mk_real_int64 1319L); (mk_real_int64 347L); (mk_real_int64 4720L); ]); ("azim_sum_neg", [1; 4; 7; 10; 13; ], [(mk_real_int64 1520L); (mk_real_int64 896L); (mk_real_int64 8L); (mk_real_int64 971L); (mk_real_int64 448L); ]); ("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 10019L); (mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 9921L); (mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 10011L); ]); ("sol_sum3", [2; 7; 8; 13; ], [(mk_real_int64 979L); (mk_real_int64 896L); (mk_real_int64 896L); (mk_real_int64 448L); ]); ("sol_sum3_neg", [4; 5; 6; 9; 10; ], [(mk_real_int64 31L); (mk_real_int64 347L); (mk_real_int64 237L); (mk_real_int64 193L); (mk_real_int64 2548L); ]); ("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; ], [(mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 9548L); (mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 9921L); (mk_real_int64 9921L); (mk_real_int64 9921L); (mk_real_int64 9249L); (mk_real_int64 10011L); (mk_real_int64 9562L); (mk_real_int64 9480L); (mk_real_int64 9261L); (mk_real_int64 9562L); ]); ("tau_sum4_neg", [0; 1; 2; 3; ], [(mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 10011L); (mk_real_int64 10011L); ]); ("ln_def_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 1037L); (mk_real_int64 1037L); (mk_real_int64 1037L); (mk_real_int64 1037L); (mk_real_int64 1037L); (mk_real_int64 1037L); (mk_real_int64 1063L); (mk_real_int64 1047L); (mk_real_int64 1115L); (mk_real_int64 1037L); (mk_real_int64 939L); (mk_real_int64 1037L); (mk_real_int64 1037L); (mk_real_int64 1037L); ]); ("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 62898L); (mk_real_int64 62898L); (mk_real_int64 62898L); (mk_real_int64 62898L); (mk_real_int64 62898L); (mk_real_int64 62898L); (mk_real_int64 62898L); (mk_real_int64 62951L); (mk_real_int64 62898L); (mk_real_int64 62898L); (mk_real_int64 62336L); (mk_real_int64 62898L); (mk_real_int64 62898L); (mk_real_int64 62898L); ]); ("edge_sym", [5; 6; 15; 22; 26; 40; 57; 60; ], [(mk_real_int64 299L); (mk_real_int64 299L); (mk_real_int64 485L); (mk_real_int64 641L); (mk_real_int64 29L); (mk_real_int64 895L); (mk_real_int64 49L); (mk_real_int64 470L); ]); ("edge_sym_neg", [9; 10; 13; 28; 29; 32; 34; 35; 38; 41; 50; 51; 54; ], [(mk_real_int64 281L); (mk_real_int64 538L); (mk_real_int64 1126L); (mk_real_int64 1048L); (mk_real_int64 29L); (mk_real_int64 3124L); (mk_real_int64 663L); (mk_real_int64 757L); (mk_real_int64 462L); (mk_real_int64 182L); (mk_real_int64 1056L); (mk_real_int64 1056L); (mk_real_int64 125L); ]); ("y1_def_neg", [6; 10; 12; 14; 15; 19; 26; 27; 29; 31; 32; 33; 34; 35; 37; 38; 41; 42; 43; 50; 53; 55; 56; 57; 60; 62; 63; ], [(mk_real_int64 234L); (mk_real_int64 774L); (mk_real_int64 1288L); (mk_real_int64 148L); (mk_real_int64 277L); (mk_real_int64 1802L); (mk_real_int64 7L); (mk_real_int64 228L); (mk_real_int64 321L); (mk_real_int64 700L); (mk_real_int64 589L); (mk_real_int64 1403L); (mk_real_int64 54L); (mk_real_int64 98L); (mk_real_int64 54L); (mk_real_int64 1165L); (mk_real_int64 54L); (mk_real_int64 529L); (mk_real_int64 1128L); (mk_real_int64 1423L); (mk_real_int64 123L); (mk_real_int64 319L); (mk_real_int64 398L); (mk_real_int64 27L); (mk_real_int64 1030L); (mk_real_int64 269L); (mk_real_int64 235L); ]); ("y1_def", [13; 18; 24; 25; 36; 39; 40; 44; 51; 59; ], [(mk_real_int64 760L); (mk_real_int64 760L); (mk_real_int64 12L); (mk_real_int64 16L); (mk_real_int64 37L); (mk_real_int64 582L); (mk_real_int64 73L); (mk_real_int64 968L); (mk_real_int64 224L); (mk_real_int64 156L); ]); ("y2_def", [6; 15; 24; 26; 27; 31; 34; 37; 40; 41; 42; 44; 53; 55; 60; 62; ], [(mk_real_int64 299L); (mk_real_int64 168L); (mk_real_int64 12L); (mk_real_int64 11L); (mk_real_int64 354L); (mk_real_int64 1084L); (mk_real_int64 33L); (mk_real_int64 33L); (mk_real_int64 73L); (mk_real_int64 33L); (mk_real_int64 388L); (mk_real_int64 968L); (mk_real_int64 18L); (mk_real_int64 193L); (mk_real_int64 101L); (mk_real_int64 163L); ]); ("y2_def_neg", [10; 12; 13; 14; 18; 19; 25; 29; 32; 33; 35; 36; 38; 39; 43; 50; 51; 56; 57; 59; 63; ], [(mk_real_int64 774L); (mk_real_int64 1288L); (mk_real_int64 231L); (mk_real_int64 148L); (mk_real_int64 231L); (mk_real_int64 1802L); (mk_real_int64 5L); (mk_real_int64 321L); (mk_real_int64 1328L); (mk_real_int64 1403L); (mk_real_int64 147L); (mk_real_int64 11L); (mk_real_int64 1120L); (mk_real_int64 177L); (mk_real_int64 1128L); (mk_real_int64 1423L); (mk_real_int64 68L); (mk_real_int64 398L); (mk_real_int64 80L); (mk_real_int64 47L); (mk_real_int64 235L); ]); ("y3_def", [6; 15; 24; 26; 27; 31; 34; 37; 40; 41; 42; 44; 53; 55; 60; 62; ], [(mk_real_int64 299L); (mk_real_int64 168L); (mk_real_int64 12L); (mk_real_int64 11L); (mk_real_int64 354L); (mk_real_int64 1084L); (mk_real_int64 33L); (mk_real_int64 33L); (mk_real_int64 73L); (mk_real_int64 33L); (mk_real_int64 388L); (mk_real_int64 968L); (mk_real_int64 18L); (mk_real_int64 193L); (mk_real_int64 101L); (mk_real_int64 163L); ]); ("y3_def_neg", [10; 12; 13; 14; 18; 19; 25; 29; 32; 33; 35; 36; 38; 39; 43; 50; 51; 56; 57; 59; 63; ], [(mk_real_int64 774L); (mk_real_int64 1288L); (mk_real_int64 231L); (mk_real_int64 148L); (mk_real_int64 231L); (mk_real_int64 1802L); (mk_real_int64 5L); (mk_real_int64 321L); (mk_real_int64 1328L); (mk_real_int64 1403L); (mk_real_int64 147L); (mk_real_int64 11L); (mk_real_int64 1120L); (mk_real_int64 177L); (mk_real_int64 1128L); (mk_real_int64 1423L); (mk_real_int64 68L); (mk_real_int64 398L); (mk_real_int64 80L); (mk_real_int64 47L); (mk_real_int64 235L); ]); ("y4_def_neg", [2; 4; 7; 11; 12; 14; 15; 17; 19; 20; 21; 22; 25; 26; 28; 29; 30; 31; 32; 34; 37; 39; 40; 44; 46; 47; ], [(mk_real_int64 538L); (mk_real_int64 895L); (mk_real_int64 317L); (mk_real_int64 1251L); (mk_real_int64 6L); (mk_real_int64 20L); (mk_real_int64 666L); (mk_real_int64 382L); (mk_real_int64 2040L); (mk_real_int64 36L); (mk_real_int64 974L); (mk_real_int64 61L); (mk_real_int64 61L); (mk_real_int64 438L); (mk_real_int64 38L); (mk_real_int64 61L); (mk_real_int64 731L); (mk_real_int64 784L); (mk_real_int64 499L); (mk_real_int64 988L); (mk_real_int64 125L); (mk_real_int64 364L); (mk_real_int64 276L); (mk_real_int64 1272L); (mk_real_int64 307L); (mk_real_int64 163L); ]); ("y4_def", [5; 6; 10; 13; 23; 24; 27; 35; 41; 43; ], [(mk_real_int64 1175L); (mk_real_int64 317L); (mk_real_int64 1175L); (mk_real_int64 24L); (mk_real_int64 348L); (mk_real_int64 58L); (mk_real_int64 900L); (mk_real_int64 347L); (mk_real_int64 208L); (mk_real_int64 241L); ]); ("y5_def", [6; 14; 15; 26; 27; 31; 34; 35; 37; 41; 42; 53; 55; 57; 60; 62; ], [(mk_real_int64 299L); (mk_real_int64 317L); (mk_real_int64 168L); (mk_real_int64 11L); (mk_real_int64 354L); (mk_real_int64 1084L); (mk_real_int64 33L); (mk_real_int64 278L); (mk_real_int64 33L); (mk_real_int64 33L); (mk_real_int64 388L); (mk_real_int64 29L); (mk_real_int64 193L); (mk_real_int64 133L); (mk_real_int64 230L); (mk_real_int64 163L); ]); ("y5_def_neg", [10; 12; 13; 18; 19; 24; 25; 29; 32; 33; 36; 38; 39; 40; 43; 44; 50; 51; 56; 59; 63; ], [(mk_real_int64 538L); (mk_real_int64 895L); (mk_real_int64 231L); (mk_real_int64 231L); (mk_real_int64 1251L); (mk_real_int64 6L); (mk_real_int64 5L); (mk_real_int64 382L); (mk_real_int64 1084L); (mk_real_int64 974L); (mk_real_int64 11L); (mk_real_int64 389L); (mk_real_int64 177L); (mk_real_int64 38L); (mk_real_int64 784L); (mk_real_int64 499L); (mk_real_int64 988L); (mk_real_int64 68L); (mk_real_int64 276L); (mk_real_int64 47L); (mk_real_int64 163L); ]); ("y6_def", [6; 8; 12; 14; 15; 17; 18; 24; 26; 27; 31; 33; 34; 35; 36; 37; 39; 41; 42; 43; 44; 52; 53; 55; 56; 57; 58; 60; 62; ], [(mk_real_int64 299L); (mk_real_int64 239L); (mk_real_int64 231L); (mk_real_int64 957L); (mk_real_int64 168L); (mk_real_int64 998L); (mk_real_int64 1251L); (mk_real_int64 25L); (mk_real_int64 11L); (mk_real_int64 354L); (mk_real_int64 1084L); (mk_real_int64 2744L); (mk_real_int64 33L); (mk_real_int64 278L); (mk_real_int64 1068L); (mk_real_int64 33L); (mk_real_int64 561L); (mk_real_int64 33L); (mk_real_int64 388L); (mk_real_int64 1768L); (mk_real_int64 395L); (mk_real_int64 1027L); (mk_real_int64 29L); (mk_real_int64 193L); (mk_real_int64 988L); (mk_real_int64 133L); (mk_real_int64 1270L); (mk_real_int64 230L); (mk_real_int64 1219L); ]); ("y6_def_neg", [10; 13; 19; 25; 29; 32; 38; 40; 50; 51; 59; 63; ], [(mk_real_int64 538L); (mk_real_int64 231L); (mk_real_int64 1175L); (mk_real_int64 5L); (mk_real_int64 382L); (mk_real_int64 1084L); (mk_real_int64 389L); (mk_real_int64 38L); (mk_real_int64 988L); (mk_real_int64 68L); (mk_real_int64 47L); (mk_real_int64 163L); ]); ("RHA", [14; 16; 17; 20; 33; 38; 40; 43; 44; 47; 52; 53; 54; 56; 57; 58; 59; 61; 63; ], [(mk_real_int64 462L); (mk_real_int64 471L); (mk_real_int64 8L); (mk_real_int64 8L); (mk_real_int64 89L); (mk_real_int64 43L); (mk_real_int64 89L); (mk_real_int64 762L); (mk_real_int64 762L); (mk_real_int64 8L); (mk_real_int64 448L); (mk_real_int64 302L); (mk_real_int64 448L); (mk_real_int64 531L); (mk_real_int64 442L); (mk_real_int64 749L); (mk_real_int64 660L); (mk_real_int64 448L); (mk_real_int64 448L); ]); ("tau4", [2; 3; ], [(mk_real_int64 8269L); (mk_real_int64 1418L); ]); ("ineq105", [6; ], [(mk_real_int64 743L); ]); ("ineq106", [7; 22; 25; 26; 29; 30; 37; 39; 44; 46; ], [(mk_real_int64 462L); (mk_real_int64 89L); (mk_real_int64 89L); (mk_real_int64 46L); (mk_real_int64 89L); (mk_real_int64 762L); (mk_real_int64 146L); (mk_real_int64 531L); (mk_real_int64 749L); (mk_real_int64 448L); ]); ("ineq107", [5; 10; 13; 20; 23; 24; 27; 35; 41; 43; ], [(mk_real_int64 1520L); (mk_real_int64 1520L); (mk_real_int64 31L); (mk_real_int64 1133L); (mk_real_int64 75L); (mk_real_int64 75L); (mk_real_int64 1164L); (mk_real_int64 448L); (mk_real_int64 81L); (mk_real_int64 312L); ]); ("ineq108", [14; 15; 19; 30; 44; ], [(mk_real_int64 30L); (mk_real_int64 972L); (mk_real_int64 2978L); (mk_real_int64 306L); (mk_real_int64 683L); ]); ("ineq109", [6; 23; 26; 41; ], [(mk_real_int64 979L); (mk_real_int64 896L); (mk_real_int64 896L); (mk_real_int64 448L); ]); ("ineq110", [12; 17; 20; 28; 32; ], [(mk_real_int64 31L); (mk_real_int64 347L); (mk_real_int64 237L); (mk_real_int64 193L); (mk_real_int64 2548L); ]); ("ineq111", [2; 4; 11; 17; 20; 21; 26; 31; 34; 37; 40; 44; 47; ], [(mk_real_int64 4302L); (mk_real_int64 7156L); (mk_real_int64 10011L); (mk_real_int64 2515L); (mk_real_int64 6921L); (mk_real_int64 7792L); (mk_real_int64 5566L); (mk_real_int64 6268L); (mk_real_int64 7903L); (mk_real_int64 196L); (mk_real_int64 2211L); (mk_real_int64 2332L); (mk_real_int64 1306L); ]); ("ineq113", [7; ], [(mk_real_int64 2089L); ]); ("ineq114", [0; 2; 3; 6; 8; 12; 14; 16; 18; 19; 21; 26; 28; 29; 30; 34; 37; 38; 40; 42; 44; 45; ], [(mk_real_int64 2854L); (mk_real_int64 2854L); (mk_real_int64 2854L); (mk_real_int64 5157L); (mk_real_int64 2303L); (mk_real_int64 2058L); (mk_real_int64 7953L); (mk_real_int64 7495L); (mk_real_int64 176L); (mk_real_int64 2914L); (mk_real_int64 2129L); (mk_real_int64 4355L); (mk_real_int64 2689L); (mk_real_int64 7232L); (mk_real_int64 2981L); (mk_real_int64 2107L); (mk_real_int64 2590L); (mk_real_int64 1271L); (mk_real_int64 2119L); (mk_real_int64 480L); (mk_real_int64 6450L); (mk_real_int64 8256L); ]); ("ineq119", [2; 7; ], [(mk_real_int64 3356L); (mk_real_int64 1979L); ]); ("ineq120", [0; 4; 6; 10; 12; 13; ], [(mk_real_int64 6654L); (mk_real_int64 6654L); (mk_real_int64 1378L); (mk_real_int64 1742L); (mk_real_int64 6233L); (mk_real_int64 2359L); ]); ];; (***************) (* Variables *) (***************) let target_variables = [ ("ln_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 46908L); (mk_real_int64 46908L); (mk_real_int64 46908L); (mk_real_int64 46908L); (mk_real_int64 46908L); (mk_real_int64 46908L); (mk_real_int64 306908L); (mk_real_int64 53946L); (mk_real_int64 826908L); (mk_real_int64 46908L); (mk_real_int64 52656L); (mk_real_int64 46908L); (mk_real_int64 46908L); (mk_real_int64 46908L); ]); ];; (*************************) let variable_bounds = [ ("azim_hi", [0; 4; 14; 22; 24; 26; 30; 31; 33; 38; 40; 41; 42; 45; 53; 54; 56; 60; 61; ], [(mk_real_int64 742L); (mk_real_int64 742L); (mk_real_int64 2820L); (mk_real_int64 2166L); (mk_real_int64 3080L); (mk_real_int64 5780L); (mk_real_int64 1760L); (mk_real_int64 1640L); (mk_real_int64 7540L); (mk_real_int64 2300L); (mk_real_int64 3140L); (mk_real_int64 2320L); (mk_real_int64 1060L); (mk_real_int64 2509L); (mk_real_int64 3400L); (mk_real_int64 6460L); (mk_real_int64 4940L); (mk_real_int64 7000L); (mk_real_int64 2560L); ]); ("azim_lo", [2; 6; 7; 8; 10; 11; 15; 16; 28; 43; 44; 46; 50; 58; 59; ], [(mk_real_int64 2680L); (mk_real_int64 4406L); (mk_real_int64 4870L); (mk_real_int64 3960L); (mk_real_int64 3960L); (mk_real_int64 3960L); (mk_real_int64 510L); (mk_real_int64 3220L); (mk_real_int64 1300L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 5293L); (mk_real_int64 180L); (mk_real_int64 5200L); (mk_real_int64 10000L); ]); ("rhazim_lo", [14; 15; 33; 34; 37; 38; 40; 41; 52; 53; 54; 58; 60; 61; 62; 63; ], [(mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); ]); ("rhazim_hi", [57; ], [(mk_real_int64 10000L); ]); ("rho_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 11; 12; 13; ], [(mk_real_int64 31152L); (mk_real_int64 31152L); (mk_real_int64 31152L); (mk_real_int64 31152L); (mk_real_int64 31152L); (mk_real_int64 31152L); (mk_real_int64 31152L); (mk_real_int64 3808L); (mk_real_int64 31152L); (mk_real_int64 31152L); (mk_real_int64 31152L); (mk_real_int64 31152L); (mk_real_int64 31152L); ]); ("rho_lo", [10; ], [(mk_real_int64 3728L); ]); ("tau_lo", [0; 2; 3; 8; 14; 15; 16; 17; ], [(mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 55050000L); (mk_real_int64 51500000L); ]); ("tau_hi", [4; 18; ], [(mk_real_int64 10000L); (mk_real_int64 10000L); ]); ("y1_lo", [6; 10; 12; 15; 24; 25; 26; 27; 32; 42; 43; 57; 63; ], [(mk_real_int64 450L); (mk_real_int64 3600L); (mk_real_int64 800L); (mk_real_int64 2000L); (mk_real_int64 2200L); (mk_real_int64 5000L); (mk_real_int64 500L); (mk_real_int64 4200L); (mk_real_int64 2200L); (mk_real_int64 1100L); (mk_real_int64 2400L); (mk_real_int64 1480L); (mk_real_int64 800L); ]); ("y1_hi", [14; 19; 29; 31; 33; 34; 35; 36; 37; 38; 40; 41; 44; 50; 53; 55; 56; 60; 62; ], [(mk_real_int64 1710L); (mk_real_int64 200L); (mk_real_int64 1600L); (mk_real_int64 1700L); (mk_real_int64 4400L); (mk_real_int64 6000L); (mk_real_int64 2040L); (mk_real_int64 5000L); (mk_real_int64 6000L); (mk_real_int64 2240L); (mk_real_int64 3400L); (mk_real_int64 6000L); (mk_real_int64 2400L); (mk_real_int64 4600L); (mk_real_int64 1200L); (mk_real_int64 4000L); (mk_real_int64 200L); (mk_real_int64 3350L); (mk_real_int64 2000L); ]); ("y2_lo", [6; 10; 12; 13; 18; 24; 26; 27; 31; 34; 36; 37; 38; 41; 43; 51; 53; 59; 63; ], [(mk_real_int64 3140L); (mk_real_int64 3600L); (mk_real_int64 800L); (mk_real_int64 400L); (mk_real_int64 400L); (mk_real_int64 2200L); (mk_real_int64 830L); (mk_real_int64 2892L); (mk_real_int64 3058L); (mk_real_int64 6129L); (mk_real_int64 4000L); (mk_real_int64 6129L); (mk_real_int64 4366L); (mk_real_int64 6129L); (mk_real_int64 2400L); (mk_real_int64 960L); (mk_real_int64 1506L); (mk_real_int64 4240L); (mk_real_int64 800L); ]); ("y2_hi", [14; 15; 19; 25; 29; 32; 33; 35; 39; 40; 42; 44; 50; 55; 56; 57; 60; 62; ], [(mk_real_int64 1710L); (mk_real_int64 1218L); (mk_real_int64 200L); (mk_real_int64 2880L); (mk_real_int64 1600L); (mk_real_int64 640L); (mk_real_int64 4400L); (mk_real_int64 3040L); (mk_real_int64 720L); (mk_real_int64 3400L); (mk_real_int64 6452L); (mk_real_int64 2400L); (mk_real_int64 4600L); (mk_real_int64 2309L); (mk_real_int64 200L); (mk_real_int64 400L); (mk_real_int64 3448L); (mk_real_int64 272L); ]); ("y3_lo", [6; 10; 12; 13; 18; 24; 26; 27; 31; 34; 36; 37; 38; 41; 43; 51; 53; 59; 63; ], [(mk_real_int64 3140L); (mk_real_int64 3600L); (mk_real_int64 800L); (mk_real_int64 400L); (mk_real_int64 400L); (mk_real_int64 2200L); (mk_real_int64 830L); (mk_real_int64 2892L); (mk_real_int64 3058L); (mk_real_int64 6129L); (mk_real_int64 4000L); (mk_real_int64 6129L); (mk_real_int64 4366L); (mk_real_int64 6129L); (mk_real_int64 2400L); (mk_real_int64 960L); (mk_real_int64 1506L); (mk_real_int64 4240L); (mk_real_int64 800L); ]); ("y3_hi", [14; 15; 19; 25; 29; 32; 33; 35; 39; 40; 42; 44; 50; 55; 56; 57; 60; 62; ], [(mk_real_int64 1710L); (mk_real_int64 1218L); (mk_real_int64 200L); (mk_real_int64 2880L); (mk_real_int64 1600L); (mk_real_int64 640L); (mk_real_int64 4400L); (mk_real_int64 3040L); (mk_real_int64 720L); (mk_real_int64 3400L); (mk_real_int64 6452L); (mk_real_int64 2400L); (mk_real_int64 4600L); (mk_real_int64 2309L); (mk_real_int64 200L); (mk_real_int64 400L); (mk_real_int64 3448L); (mk_real_int64 272L); ]); ("y4_lo", [5; 6; 10; 11; 12; 13; 14; 17; 23; 24; 27; 30; 32; 35; 40; 41; 44; 47; ], [(mk_real_int64 400L); (mk_real_int64 5872L); (mk_real_int64 400L); (mk_real_int64 3750L); (mk_real_int64 760L); (mk_real_int64 370L); (mk_real_int64 5500L); (mk_real_int64 3870L); (mk_real_int64 4378L); (mk_real_int64 250L); (mk_real_int64 2280L); (mk_real_int64 5800L); (mk_real_int64 4080L); (mk_real_int64 6960L); (mk_real_int64 3750L); (mk_real_int64 5934L); (mk_real_int64 4200L); (mk_real_int64 2500L); ]); ("y4_hi", [2; 4; 7; 15; 19; 20; 22; 25; 26; 28; 29; 31; 34; 37; 39; 43; 46; ], [(mk_real_int64 2500L); (mk_real_int64 5000L); (mk_real_int64 5300L); (mk_real_int64 1800L); (mk_real_int64 700L); (mk_real_int64 2320L); (mk_real_int64 350L); (mk_real_int64 350L); (mk_real_int64 3272L); (mk_real_int64 1720L); (mk_real_int64 350L); (mk_real_int64 5000L); (mk_real_int64 1250L); (mk_real_int64 4900L); (mk_real_int64 2650L); (mk_real_int64 1760L); (mk_real_int64 1200L); ]); ("y5_lo", [6; 13; 14; 18; 19; 24; 26; 27; 29; 31; 34; 36; 37; 38; 41; 44; 51; 53; 56; 57; 59; 60; 63; ], [(mk_real_int64 3140L); (mk_real_int64 400L); (mk_real_int64 5872L); (mk_real_int64 400L); (mk_real_int64 3750L); (mk_real_int64 760L); (mk_real_int64 830L); (mk_real_int64 2892L); (mk_real_int64 3870L); (mk_real_int64 3058L); (mk_real_int64 6129L); (mk_real_int64 4000L); (mk_real_int64 6129L); (mk_real_int64 4234L); (mk_real_int64 6129L); (mk_real_int64 4080L); (mk_real_int64 960L); (mk_real_int64 3706L); (mk_real_int64 3750L); (mk_real_int64 5184L); (mk_real_int64 4240L); (mk_real_int64 3952L); (mk_real_int64 2500L); ]); ("y5_hi", [10; 12; 15; 25; 32; 35; 39; 40; 42; 43; 50; 55; 62; ], [(mk_real_int64 2500L); (mk_real_int64 5000L); (mk_real_int64 1218L); (mk_real_int64 2880L); (mk_real_int64 2070L); (mk_real_int64 1872L); (mk_real_int64 720L); (mk_real_int64 1720L); (mk_real_int64 6452L); (mk_real_int64 5000L); (mk_real_int64 1250L); (mk_real_int64 2309L); (mk_real_int64 272L); ]); ("y6_lo", [6; 8; 12; 13; 14; 17; 18; 19; 24; 26; 27; 29; 31; 33; 34; 36; 37; 38; 39; 41; 43; 44; 51; 52; 53; 56; 57; 58; 59; 60; 62; 63; ], [(mk_real_int64 3140L); (mk_real_int64 2390000L); (mk_real_int64 11260000L); (mk_real_int64 400L); (mk_real_int64 6410000L); (mk_real_int64 9980000L); (mk_real_int64 14820400L); (mk_real_int64 763750L); (mk_real_int64 310760L); (mk_real_int64 830L); (mk_real_int64 2892L); (mk_real_int64 3870L); (mk_real_int64 3058L); (mk_real_int64 37180000L); (mk_real_int64 6129L); (mk_real_int64 10800000L); (mk_real_int64 6129L); (mk_real_int64 4234L); (mk_real_int64 7380000L); (mk_real_int64 6129L); (mk_real_int64 25520000L); (mk_real_int64 8950000L); (mk_real_int64 960L); (mk_real_int64 10270000L); (mk_real_int64 3706L); (mk_real_int64 12643750L); (mk_real_int64 5184L); (mk_real_int64 12700000L); (mk_real_int64 4240L); (mk_real_int64 3952L); (mk_real_int64 10560000L); (mk_real_int64 2500L); ]); ("y6_hi", [10; 12; 14; 15; 25; 32; 35; 36; 39; 40; 42; 43; 44; 50; 55; 62; ], [(mk_real_int64 2500L); (mk_real_int64 5000L); (mk_real_int64 4128L); (mk_real_int64 1218L); (mk_real_int64 2880L); (mk_real_int64 2070L); (mk_real_int64 1872L); (mk_real_int64 6000L); (mk_real_int64 720L); (mk_real_int64 1720L); (mk_real_int64 6452L); (mk_real_int64 5000L); (mk_real_int64 5920L); (mk_real_int64 1250L); (mk_real_int64 2309L); (mk_real_int64 272L); ]); ("ye_hi", [17; 27; 29; 33; 37; 38; 57; 59; 60; ], [(mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); ]); ("ye_lo", [9; 11; 14; 22; 44; ], [(mk_real_int64 2570000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 6410000L); (mk_real_int64 10000L); ]); ("yn_lo", [1; 3; 4; 6; 8; 9; 11; 12; 13; ], [(mk_real_int64 7453L); (mk_real_int64 7453L); (mk_real_int64 7453L); (mk_real_int64 7447L); (mk_real_int64 7435L); (mk_real_int64 7453L); (mk_real_int64 17453L); (mk_real_int64 7453L); (mk_real_int64 17453L); ]); ("yn_hi", [0; 2; 5; 7; 10; ], [(mk_real_int64 2547L); (mk_real_int64 2547L); (mk_real_int64 2547L); (mk_real_int64 4857L); (mk_real_int64 7909L); ]); ];;end;; concl (Test_case.result)let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;