needs "nobranching_lp.hl";; module Test_case = struct let hypermap_string = "168156828154 21 4 0 1 2 3 3 0 3 4 3 4 3 5 4 5 3 6 7 3 6 3 2 3 6 2 8 3 8 2 1 3 8 1 9 3 9 1 0 4 9 0 10 11 3 10 0 4 3 10 4 12 3 12 4 5 3 12 5 7 3 7 6 13 3 13 6 8 3 13 8 9 3 13 9 11 3 11 10 12 3 11 12 7 3 7 13 11 ";; let precision = 4;; (***************) (* Constraints *) (***************) let constraints = [ ("azim_sum", [0; 3; 6; 8; ], [(mk_real_int64 2872L); (mk_real_int64 2872L); (mk_real_int64 580L); (mk_real_int64 580L); ]); ("azim_sum_neg", [4; 5; 7; 9; 10; 12; ], [(mk_real_int64 1531L); (mk_real_int64 1450L); (mk_real_int64 1073L); (mk_real_int64 1450L); (mk_real_int64 2874L); (mk_real_int64 1747L); ]); ("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 11731L); (mk_real_int64 10592L); (mk_real_int64 10592L); (mk_real_int64 11731L); (mk_real_int64 11731L); (mk_real_int64 10200L); (mk_real_int64 11731L); (mk_real_int64 9649L); (mk_real_int64 11731L); (mk_real_int64 10200L); (mk_real_int64 11351L); (mk_real_int64 11731L); (mk_real_int64 11731L); (mk_real_int64 11731L); ]); ("sol_sum3_neg", [0; 2; 6; ], [(mk_real_int64 1055L); (mk_real_int64 10L); (mk_real_int64 10L); ]); ("sol_sum3", [8; 9; 10; 15; ], [(mk_real_int64 1450L); (mk_real_int64 1450L); (mk_real_int64 1450L); (mk_real_int64 1450L); ]); ("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; ], [(mk_real_int64 11731L); (mk_real_int64 10200L); (mk_real_int64 10592L); (mk_real_int64 9649L); (mk_real_int64 9649L); (mk_real_int64 9649L); (mk_real_int64 10592L); (mk_real_int64 10200L); (mk_real_int64 10200L); (mk_real_int64 10200L); (mk_real_int64 10200L); (mk_real_int64 11731L); (mk_real_int64 9649L); (mk_real_int64 9649L); (mk_real_int64 11731L); (mk_real_int64 10200L); (mk_real_int64 11351L); (mk_real_int64 11731L); ]); ("tau_sum4_neg", [0; 1; 2; ], [(mk_real_int64 10592L); (mk_real_int64 11731L); (mk_real_int64 11731L); ]); ("ln_def_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 2934L); (mk_real_int64 1678L); (mk_real_int64 1678L); (mk_real_int64 2934L); (mk_real_int64 2934L); (mk_real_int64 1246L); (mk_real_int64 2934L); (mk_real_int64 638L); (mk_real_int64 2934L); (mk_real_int64 1246L); (mk_real_int64 2515L); (mk_real_int64 2934L); (mk_real_int64 2934L); (mk_real_int64 2934L); ]); ("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 73705L); (mk_real_int64 66550L); (mk_real_int64 66550L); (mk_real_int64 73705L); (mk_real_int64 73705L); (mk_real_int64 64086L); (mk_real_int64 73705L); (mk_real_int64 60625L); (mk_real_int64 73705L); (mk_real_int64 64086L); (mk_real_int64 71320L); (mk_real_int64 73705L); (mk_real_int64 73705L); (mk_real_int64 73705L); ]); ("edge_sym_neg", [3; 5; 6; 9; 11; 16; 18; 19; 22; 25; 35; 38; 41; 44; 46; 47; 50; 56; ], [(mk_real_int64 1051L); (mk_real_int64 1341L); (mk_real_int64 1341L); (mk_real_int64 3935L); (mk_real_int64 9L); (mk_real_int64 1195L); (mk_real_int64 495L); (mk_real_int64 1484L); (mk_real_int64 993L); (mk_real_int64 1484L); (mk_real_int64 3935L); (mk_real_int64 1507L); (mk_real_int64 1507L); (mk_real_int64 253L); (mk_real_int64 1616L); (mk_real_int64 1616L); (mk_real_int64 2174L); (mk_real_int64 1616L); ]); ("edge_sym", [24; 28; 37; 53; 59; 62; ], [(mk_real_int64 498L); (mk_real_int64 9L); (mk_real_int64 383L); (mk_real_int64 545L); (mk_real_int64 38L); (mk_real_int64 192L); ]); ("y1_def", [5; 6; 9; 16; 19; 20; 23; 33; 39; 42; 47; 50; 52; 54; 61; 64; ], [(mk_real_int64 401L); (mk_real_int64 226L); (mk_real_int64 725L); (mk_real_int64 8L); (mk_real_int64 537L); (mk_real_int64 537L); (mk_real_int64 537L); (mk_real_int64 725L); (mk_real_int64 137L); (mk_real_int64 137L); (mk_real_int64 874L); (mk_real_int64 537L); (mk_real_int64 537L); (mk_real_int64 874L); (mk_real_int64 124L); (mk_real_int64 742L); ]); ("y1_def_neg", [7; 8; 14; 15; 18; 22; 24; 25; 27; 28; 34; 35; 37; 38; 40; 41; 44; 45; 48; 49; 51; 53; 56; 58; 59; 65; ], [(mk_real_int64 1649L); (mk_real_int64 1441L); (mk_real_int64 592L); (mk_real_int64 683L); (mk_real_int64 1537L); (mk_real_int64 1195L); (mk_real_int64 566L); (mk_real_int64 971L); (mk_real_int64 587L); (mk_real_int64 680L); (mk_real_int64 1441L); (mk_real_int64 1649L); (mk_real_int64 2370L); (mk_real_int64 82L); (mk_real_int64 862L); (mk_real_int64 1727L); (mk_real_int64 1198L); (mk_real_int64 1945L); (mk_real_int64 127L); (mk_real_int64 2379L); (mk_real_int64 201L); (mk_real_int64 2423L); (mk_real_int64 1945L); (mk_real_int64 979L); (mk_real_int64 82L); (mk_real_int64 1929L); ]); ("y2_def", [5; 8; 15; 16; 24; 28; 34; 40; 48; 51; ], [(mk_real_int64 401L); (mk_real_int64 1365L); (mk_real_int64 414L); (mk_real_int64 2L); (mk_real_int64 343L); (mk_real_int64 418L); (mk_real_int64 1365L); (mk_real_int64 171L); (mk_real_int64 77L); (mk_real_int64 122L); ]); ("y2_def_neg", [6; 7; 9; 14; 18; 19; 20; 22; 23; 25; 27; 33; 35; 37; 38; 39; 41; 42; 44; 45; 47; 49; 50; 52; 53; 54; 56; 58; 59; 61; 64; 65; ], [(mk_real_int64 1460L); (mk_real_int64 1649L); (mk_real_int64 220L); (mk_real_int64 592L); (mk_real_int64 628L); (mk_real_int64 163L); (mk_real_int64 163L); (mk_real_int64 1195L); (mk_real_int64 163L); (mk_real_int64 971L); (mk_real_int64 593L); (mk_real_int64 220L); (mk_real_int64 1649L); (mk_real_int64 1337L); (mk_real_int64 260L); (mk_real_int64 42L); (mk_real_int64 1727L); (mk_real_int64 42L); (mk_real_int64 1198L); (mk_real_int64 1945L); (mk_real_int64 266L); (mk_real_int64 812L); (mk_real_int64 163L); (mk_real_int64 163L); (mk_real_int64 846L); (mk_real_int64 266L); (mk_real_int64 1945L); (mk_real_int64 979L); (mk_real_int64 260L); (mk_real_int64 38L); (mk_real_int64 226L); (mk_real_int64 1929L); ]); ("y3_def", [5; 8; 15; 16; 24; 28; 34; 40; 48; 51; ], [(mk_real_int64 401L); (mk_real_int64 1365L); (mk_real_int64 414L); (mk_real_int64 2L); (mk_real_int64 343L); (mk_real_int64 418L); (mk_real_int64 1365L); (mk_real_int64 171L); (mk_real_int64 77L); (mk_real_int64 122L); ]); ("y3_def_neg", [6; 7; 9; 14; 18; 19; 20; 22; 23; 25; 27; 33; 35; 37; 38; 39; 41; 42; 44; 45; 47; 49; 50; 52; 53; 54; 56; 58; 59; 61; 64; 65; ], [(mk_real_int64 1460L); (mk_real_int64 1649L); (mk_real_int64 220L); (mk_real_int64 592L); (mk_real_int64 628L); (mk_real_int64 163L); (mk_real_int64 163L); (mk_real_int64 1195L); (mk_real_int64 163L); (mk_real_int64 971L); (mk_real_int64 593L); (mk_real_int64 220L); (mk_real_int64 1649L); (mk_real_int64 1337L); (mk_real_int64 260L); (mk_real_int64 42L); (mk_real_int64 1727L); (mk_real_int64 42L); (mk_real_int64 1198L); (mk_real_int64 1945L); (mk_real_int64 266L); (mk_real_int64 812L); (mk_real_int64 163L); (mk_real_int64 163L); (mk_real_int64 846L); (mk_real_int64 266L); (mk_real_int64 1945L); (mk_real_int64 979L); (mk_real_int64 260L); (mk_real_int64 38L); (mk_real_int64 226L); (mk_real_int64 1929L); ]); ("y4_def_neg", [1; 3; 4; 6; 7; 10; 14; 16; 17; 19; 20; 22; 23; 25; 28; 29; 32; 33; 36; 37; 39; 41; 44; 46; 53; ], [(mk_real_int64 207L); (mk_real_int64 1145L); (mk_real_int64 2570L); (mk_real_int64 411L); (mk_real_int64 780L); (mk_real_int64 1320L); (mk_real_int64 830L); (mk_real_int64 646L); (mk_real_int64 675L); (mk_real_int64 404L); (mk_real_int64 782L); (mk_real_int64 2570L); (mk_real_int64 1145L); (mk_real_int64 1934L); (mk_real_int64 266L); (mk_real_int64 1199L); (mk_real_int64 211L); (mk_real_int64 1351L); (mk_real_int64 145L); (mk_real_int64 2088L); (mk_real_int64 229L); (mk_real_int64 2122L); (mk_real_int64 1351L); (mk_real_int64 680L); (mk_real_int64 1340L); ]); ("y4_def", [2; 5; 8; 11; 12; 15; 21; 26; 27; 30; 35; 38; 40; 42; 47; 49; 52; ], [(mk_real_int64 1258L); (mk_real_int64 1121L); (mk_real_int64 5L); (mk_real_int64 830L); (mk_real_int64 830L); (mk_real_int64 830L); (mk_real_int64 1121L); (mk_real_int64 680L); (mk_real_int64 211L); (mk_real_int64 211L); (mk_real_int64 1351L); (mk_real_int64 830L); (mk_real_int64 830L); (mk_real_int64 1351L); (mk_real_int64 680L); (mk_real_int64 192L); (mk_real_int64 1147L); ]); ("y5_def_neg", [5; 6; 7; 9; 12; 14; 16; 18; 19; 20; 22; 23; 25; 27; 30; 33; 35; 37; 39; 41; 42; 44; 45; 47; 49; 50; 52; 53; 54; 56; 58; 61; 64; 65; ], [(mk_real_int64 207L); (mk_real_int64 1134L); (mk_real_int64 1145L); (mk_real_int64 220L); (mk_real_int64 9L); (mk_real_int64 411L); (mk_real_int64 3L); (mk_real_int64 331L); (mk_real_int64 163L); (mk_real_int64 163L); (mk_real_int64 830L); (mk_real_int64 163L); (mk_real_int64 675L); (mk_real_int64 413L); (mk_real_int64 9L); (mk_real_int64 220L); (mk_real_int64 1145L); (mk_real_int64 809L); (mk_real_int64 42L); (mk_real_int64 1199L); (mk_real_int64 42L); (mk_real_int64 211L); (mk_real_int64 1351L); (mk_real_int64 266L); (mk_real_int64 383L); (mk_real_int64 163L); (mk_real_int64 163L); (mk_real_int64 406L); (mk_real_int64 266L); (mk_real_int64 1351L); (mk_real_int64 680L); (mk_real_int64 38L); (mk_real_int64 226L); (mk_real_int64 1340L); ]); ("y5_def", [8; 15; 24; 28; 34; 38; 40; 48; 51; 59; ], [(mk_real_int64 1365L); (mk_real_int64 414L); (mk_real_int64 343L); (mk_real_int64 413L); (mk_real_int64 1365L); (mk_real_int64 427L); (mk_real_int64 859L); (mk_real_int64 77L); (mk_real_int64 122L); (mk_real_int64 427L); ]); ("y6_def_neg", [5; 6; 7; 9; 14; 16; 18; 19; 22; 25; 27; 33; 35; 37; 39; 41; 44; 45; 47; 50; 53; 56; 65; ], [(mk_real_int64 207L); (mk_real_int64 1134L); (mk_real_int64 1145L); (mk_real_int64 220L); (mk_real_int64 411L); (mk_real_int64 3L); (mk_real_int64 331L); (mk_real_int64 163L); (mk_real_int64 830L); (mk_real_int64 675L); (mk_real_int64 413L); (mk_real_int64 220L); (mk_real_int64 1145L); (mk_real_int64 44L); (mk_real_int64 42L); (mk_real_int64 1199L); (mk_real_int64 211L); (mk_real_int64 1351L); (mk_real_int64 266L); (mk_real_int64 163L); (mk_real_int64 406L); (mk_real_int64 1351L); (mk_real_int64 1340L); ]); ("y6_def", [8; 15; 20; 23; 24; 26; 28; 34; 36; 38; 40; 42; 48; 49; 51; 52; 54; 58; 59; 61; 63; 64; ], [(mk_real_int64 1365L); (mk_real_int64 414L); (mk_real_int64 1324L); (mk_real_int64 1324L); (mk_real_int64 343L); (mk_real_int64 696L); (mk_real_int64 413L); (mk_real_int64 1365L); (mk_real_int64 4065L); (mk_real_int64 427L); (mk_real_int64 4924L); (mk_real_int64 1718L); (mk_real_int64 1170L); (mk_real_int64 1792L); (mk_real_int64 4459L); (mk_real_int64 2119L); (mk_real_int64 805L); (mk_real_int64 1080L); (mk_real_int64 427L); (mk_real_int64 253L); (mk_real_int64 3181L); (mk_real_int64 2956L); ]); ("y8_def_neg", [7; 10; ], [(mk_real_int64 9L); (mk_real_int64 9L); ]); ("RHA", [0; 3; 7; 14; 17; 21; 22; 25; 26; 35; 37; 38; 39; 40; 42; 44; 48; 49; 51; 53; 57; 59; 60; 62; ], [(mk_real_int64 1139L); (mk_real_int64 1139L); (mk_real_int64 1531L); (mk_real_int64 1139L); (mk_real_int64 2082L); (mk_real_int64 943L); (mk_real_int64 943L); (mk_real_int64 2082L); (mk_real_int64 1139L); (mk_real_int64 1531L); (mk_real_int64 459L); (mk_real_int64 1151L); (mk_real_int64 1151L); (mk_real_int64 459L); (mk_real_int64 1151L); (mk_real_int64 1531L); (mk_real_int64 1870L); (mk_real_int64 456L); (mk_real_int64 1747L); (mk_real_int64 446L); (mk_real_int64 1531L); (mk_real_int64 1151L); (mk_real_int64 380L); (mk_real_int64 380L); ]); ("RHB", [10; 31; ], [(mk_real_int64 1531L); (mk_real_int64 1531L); ]); ("yy10", [3; ], [(mk_real_int64 1051L); ]); ("ineq106", [4; 7; 10; 16; 20; 22; 25; 28; 36; 37; 39; 41; ], [(mk_real_int64 1531L); (mk_real_int64 1139L); (mk_real_int64 943L); (mk_real_int64 943L); (mk_real_int64 1139L); (mk_real_int64 1531L); (mk_real_int64 1072L); (mk_real_int64 1072L); (mk_real_int64 212L); (mk_real_int64 1625L); (mk_real_int64 335L); (mk_real_int64 1636L); ]); ("ineq107", [2; 5; 8; 11; 12; 15; 19; 21; 26; 27; 30; 35; 38; 40; 42; 47; 49; 52; ], [(mk_real_int64 2586L); (mk_real_int64 1450L); (mk_real_int64 10L); (mk_real_int64 1073L); (mk_real_int64 1073L); (mk_real_int64 1073L); (mk_real_int64 10L); (mk_real_int64 1450L); (mk_real_int64 273L); (mk_real_int64 273L); (mk_real_int64 273L); (mk_real_int64 1747L); (mk_real_int64 1073L); (mk_real_int64 1073L); (mk_real_int64 1747L); (mk_real_int64 273L); (mk_real_int64 249L); (mk_real_int64 1484L); ]); ("ineq108", [4; 22; ], [(mk_real_int64 2221L); (mk_real_int64 2221L); ]); ("ineq109", [26; 28; 32; 47; ], [(mk_real_int64 1450L); (mk_real_int64 1450L); (mk_real_int64 1450L); (mk_real_int64 1450L); ]); ("ineq110", [1; 8; 20; ], [(mk_real_int64 1055L); (mk_real_int64 10L); (mk_real_int64 10L); ]); ("ineq111", [2; 3; 6; 10; 14; 17; 19; 23; 25; 29; 32; 33; 37; 41; 44; 46; 53; ], [(mk_real_int64 5927L); (mk_real_int64 9160L); (mk_real_int64 3289L); (mk_real_int64 5397L); (mk_real_int64 6636L); (mk_real_int64 5397L); (mk_real_int64 3289L); (mk_real_int64 9160L); (mk_real_int64 9596L); (mk_real_int64 9596L); (mk_real_int64 5438L); (mk_real_int64 10804L); (mk_real_int64 7798L); (mk_real_int64 8010L); (mk_real_int64 10804L); (mk_real_int64 5438L); (mk_real_int64 10716L); ]); ("ineq113", [49; 52; ], [(mk_real_int64 10138L); (mk_real_int64 1014L); ]); ("ineq114", [0; 1; 4; 6; 7; 9; 13; 14; 17; 18; 20; 22; 25; 28; 32; 34; 36; 37; 41; 43; 45; 48; 50; ], [(mk_real_int64 2902L); (mk_real_int64 2902L); (mk_real_int64 1039L); (mk_real_int64 2731L); (mk_real_int64 4572L); (mk_real_int64 4252L); (mk_real_int64 1506L); (mk_real_int64 1506L); (mk_real_int64 4252L); (mk_real_int64 2731L); (mk_real_int64 4572L); (mk_real_int64 1039L); (mk_real_int64 604L); (mk_real_int64 604L); (mk_real_int64 4761L); (mk_real_int64 926L); (mk_real_int64 196L); (mk_real_int64 1655L); (mk_real_int64 1639L); (mk_real_int64 926L); (mk_real_int64 4761L); (mk_real_int64 606L); (mk_real_int64 606L); ]); ("ineq119", [4; 10; ], [(mk_real_int64 7173L); (mk_real_int64 7173L); ]); ("ineq120", [0; 3; 5; 6; 8; 9; ], [(mk_real_int64 5296L); (mk_real_int64 5296L); (mk_real_int64 3792L); (mk_real_int64 766L); (mk_real_int64 766L); (mk_real_int64 3792L); ]); ];; (***************) (* Variables *) (***************) let target_variables = [ ("ln_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 61430L); (mk_real_int64 51300L); (mk_real_int64 51300L); (mk_real_int64 61430L); (mk_real_int64 61430L); (mk_real_int64 53156L); (mk_real_int64 61430L); (mk_real_int64 43750L); (mk_real_int64 61430L); (mk_real_int64 53156L); (mk_real_int64 54720L); (mk_real_int64 61430L); (mk_real_int64 61430L); (mk_real_int64 61430L); ]); ];; (*************************) let variable_bounds = [ ("azim_lo", [0; 3; 4; 5; 8; 11; 17; 21; 22; 25; 30; 34; 44; 46; 48; 55; 57; 60; 61; 62; ], [(mk_real_int64 3392L); (mk_real_int64 3392L); (mk_real_int64 3480L); (mk_real_int64 3480L); (mk_real_int64 5860L); (mk_real_int64 3184L); (mk_real_int64 2480L); (mk_real_int64 2440L); (mk_real_int64 2440L); (mk_real_int64 2480L); (mk_real_int64 3184L); (mk_real_int64 5860L); (mk_real_int64 6140L); (mk_real_int64 3240L); (mk_real_int64 3040L); (mk_real_int64 3240L); (mk_real_int64 6140L); (mk_real_int64 6440L); (mk_real_int64 7420L); (mk_real_int64 6440L); ]); ("azim_hi", [10; 12; 14; 15; 26; 28; 29; 31; 37; 40; 49; 53; 64; ], [(mk_real_int64 3215L); (mk_real_int64 918L); (mk_real_int64 6060L); (mk_real_int64 720L); (mk_real_int64 6060L); (mk_real_int64 720L); (mk_real_int64 918L); (mk_real_int64 3215L); (mk_real_int64 1040L); (mk_real_int64 1040L); (mk_real_int64 300L); (mk_real_int64 140L); (mk_real_int64 3740L); ]); ("rhazim_lo", [49; ], [(mk_real_int64 10000L); ]); ("rho_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 32192L); (mk_real_int64 16544L); (mk_real_int64 16544L); (mk_real_int64 32192L); (mk_real_int64 32192L); (mk_real_int64 26400L); (mk_real_int64 32192L); (mk_real_int64 15968L); (mk_real_int64 32192L); (mk_real_int64 26400L); (mk_real_int64 6032L); (mk_real_int64 32192L); (mk_real_int64 32192L); (mk_real_int64 32192L); ]); ("tau_lo", [2; 6; 10; 13; 14; 17; 18; 19; 20; ], [(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); ]); ("y1_hi", [6; 7; 8; 16; 22; 24; 28; 34; 35; 44; 45; 49; 56; 58; 61; 65; ], [(mk_real_int64 1400L); (mk_real_int64 2000L); (mk_real_int64 4650L); (mk_real_int64 8000L); (mk_real_int64 5200L); (mk_real_int64 2000L); (mk_real_int64 4000L); (mk_real_int64 4650L); (mk_real_int64 2000L); (mk_real_int64 2100L); (mk_real_int64 2800L); (mk_real_int64 3600L); (mk_real_int64 2800L); (mk_real_int64 1600L); (mk_real_int64 5000L); (mk_real_int64 1200L); ]); ("y1_lo", [5; 14; 15; 18; 19; 20; 23; 25; 27; 37; 38; 39; 40; 41; 42; 47; 48; 50; 52; 53; 54; 59; ], [(mk_real_int64 1000L); (mk_real_int64 200L); (mk_real_int64 4000L); (mk_real_int64 2600L); (mk_real_int64 5000L); (mk_real_int64 5000L); (mk_real_int64 5000L); (mk_real_int64 4600L); (mk_real_int64 200L); (mk_real_int64 4800L); (mk_real_int64 4500L); (mk_real_int64 5000L); (mk_real_int64 1500L); (mk_real_int64 2800L); (mk_real_int64 5000L); (mk_real_int64 5000L); (mk_real_int64 2000L); (mk_real_int64 5000L); (mk_real_int64 5000L); (mk_real_int64 4000L); (mk_real_int64 5000L); (mk_real_int64 4500L); ]); ("y2_hi", [6; 7; 8; 15; 16; 22; 24; 28; 34; 35; 39; 40; 42; 44; 45; 47; 48; 54; 56; 58; 61; 64; 65; ], [(mk_real_int64 680L); (mk_real_int64 2000L); (mk_real_int64 3528L); (mk_real_int64 4821L); (mk_real_int64 2800L); (mk_real_int64 5200L); (mk_real_int64 1577L); (mk_real_int64 2821L); (mk_real_int64 3528L); (mk_real_int64 2000L); (mk_real_int64 5040L); (mk_real_int64 1508L); (mk_real_int64 5040L); (mk_real_int64 2100L); (mk_real_int64 2800L); (mk_real_int64 4560L); (mk_real_int64 1468L); (mk_real_int64 4560L); (mk_real_int64 2800L); (mk_real_int64 1600L); (mk_real_int64 1520L); (mk_real_int64 4320L); (mk_real_int64 1200L); ]); ("y2_lo", [5; 9; 14; 18; 19; 20; 23; 25; 27; 33; 37; 38; 41; 49; 50; 51; 52; 53; 59; ], [(mk_real_int64 1000L); (mk_real_int64 4000L); (mk_real_int64 200L); (mk_real_int64 3023L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 4600L); (mk_real_int64 5400L); (mk_real_int64 4000L); (mk_real_int64 1792L); (mk_real_int64 4460L); (mk_real_int64 2800L); (mk_real_int64 3025L); (mk_real_int64 960L); (mk_real_int64 935L); (mk_real_int64 960L); (mk_real_int64 4596L); (mk_real_int64 4460L); ]); ("y3_hi", [6; 7; 8; 15; 16; 22; 24; 28; 34; 35; 39; 40; 42; 44; 45; 47; 48; 54; 56; 58; 61; 64; 65; ], [(mk_real_int64 680L); (mk_real_int64 2000L); (mk_real_int64 3528L); (mk_real_int64 4821L); (mk_real_int64 2800L); (mk_real_int64 5200L); (mk_real_int64 1577L); (mk_real_int64 2821L); (mk_real_int64 3528L); (mk_real_int64 2000L); (mk_real_int64 5040L); (mk_real_int64 1508L); (mk_real_int64 5040L); (mk_real_int64 2100L); (mk_real_int64 2800L); (mk_real_int64 4560L); (mk_real_int64 1468L); (mk_real_int64 4560L); (mk_real_int64 2800L); (mk_real_int64 1600L); (mk_real_int64 1520L); (mk_real_int64 4320L); (mk_real_int64 1200L); ]); ("y3_lo", [5; 9; 14; 18; 19; 20; 23; 25; 27; 33; 37; 38; 41; 49; 50; 51; 52; 53; 59; ], [(mk_real_int64 1000L); (mk_real_int64 4000L); (mk_real_int64 200L); (mk_real_int64 3023L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 4600L); (mk_real_int64 5400L); (mk_real_int64 4000L); (mk_real_int64 1792L); (mk_real_int64 4460L); (mk_real_int64 2800L); (mk_real_int64 3025L); (mk_real_int64 960L); (mk_real_int64 935L); (mk_real_int64 960L); (mk_real_int64 4596L); (mk_real_int64 4460L); ]); ("y4_lo", [4; 5; 6; 7; 10; 11; 12; 15; 20; 21; 22; 26; 29; 32; 35; 36; 38; 39; 40; 42; 47; ], [(mk_real_int64 1200L); (mk_real_int64 1500L); (mk_real_int64 1250L); (mk_real_int64 2150L); (mk_real_int64 5800L); (mk_real_int64 5710L); (mk_real_int64 5710L); (mk_real_int64 5710L); (mk_real_int64 1750L); (mk_real_int64 1500L); (mk_real_int64 1200L); (mk_real_int64 3310L); (mk_real_int64 5000L); (mk_real_int64 1100L); (mk_real_int64 5690L); (mk_real_int64 2200L); (mk_real_int64 5710L); (mk_real_int64 4750L); (mk_real_int64 5710L); (mk_real_int64 5690L); (mk_real_int64 3310L); ]); ("y4_hi", [1; 2; 8; 14; 16; 17; 19; 25; 27; 28; 30; 33; 37; 41; 44; 46; 49; 52; 53; ], [(mk_real_int64 2200L); (mk_real_int64 1030L); (mk_real_int64 7700L); (mk_real_int64 5000L); (mk_real_int64 450L); (mk_real_int64 3750L); (mk_real_int64 6050L); (mk_real_int64 1800L); (mk_real_int64 290L); (mk_real_int64 3200L); (mk_real_int64 290L); (mk_real_int64 5000L); (mk_real_int64 1250L); (mk_real_int64 900L); (mk_real_int64 5000L); (mk_real_int64 2500L); (mk_real_int64 4770L); (mk_real_int64 1320L); (mk_real_int64 5000L); ]); ("y5_hi", [5; 6; 8; 15; 22; 24; 25; 27; 34; 38; 39; 42; 45; 47; 48; 53; 54; 56; 58; 59; 61; 64; 65; ], [(mk_real_int64 2200L); (mk_real_int64 530L); (mk_real_int64 3528L); (mk_real_int64 4821L); (mk_real_int64 5000L); (mk_real_int64 1577L); (mk_real_int64 3750L); (mk_real_int64 3550L); (mk_real_int64 3528L); (mk_real_int64 1440L); (mk_real_int64 5040L); (mk_real_int64 5040L); (mk_real_int64 5000L); (mk_real_int64 4560L); (mk_real_int64 1468L); (mk_real_int64 904L); (mk_real_int64 4560L); (mk_real_int64 5000L); (mk_real_int64 2500L); (mk_real_int64 1440L); (mk_real_int64 1520L); (mk_real_int64 4320L); (mk_real_int64 5000L); ]); ("y5_lo", [9; 14; 16; 18; 19; 20; 23; 28; 33; 37; 40; 41; 44; 49; 50; 51; 52; ], [(mk_real_int64 4000L); (mk_real_int64 1250L); (mk_real_int64 4800L); (mk_real_int64 4673L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 960L); (mk_real_int64 4779L); (mk_real_int64 4000L); (mk_real_int64 3992L); (mk_real_int64 2592L); (mk_real_int64 5000L); (mk_real_int64 1100L); (mk_real_int64 4125L); (mk_real_int64 960L); (mk_real_int64 935L); (mk_real_int64 960L); ]); ("y6_hi", [5; 6; 8; 15; 22; 24; 25; 27; 34; 38; 39; 45; 47; 48; 53; 54; 56; 59; 61; 65; ], [(mk_real_int64 2200L); (mk_real_int64 530L); (mk_real_int64 3528L); (mk_real_int64 4821L); (mk_real_int64 5000L); (mk_real_int64 1577L); (mk_real_int64 3750L); (mk_real_int64 3550L); (mk_real_int64 3528L); (mk_real_int64 1440L); (mk_real_int64 5040L); (mk_real_int64 5000L); (mk_real_int64 4560L); (mk_real_int64 1468L); (mk_real_int64 904L); (mk_real_int64 4560L); (mk_real_int64 5000L); (mk_real_int64 1440L); (mk_real_int64 1520L); (mk_real_int64 5000L); ]); ("y6_lo", [9; 14; 16; 18; 19; 20; 23; 26; 28; 33; 36; 37; 40; 41; 42; 44; 48; 49; 50; 51; 52; 54; 58; 61; 63; 64; ], [(mk_real_int64 4000L); (mk_real_int64 1250L); (mk_real_int64 4800L); (mk_real_int64 4673L); (mk_real_int64 960L); (mk_real_int64 14870960L); (mk_real_int64 14870960L); (mk_real_int64 6960000L); (mk_real_int64 4779L); (mk_real_int64 4000L); (mk_real_int64 40650000L); (mk_real_int64 7653992L); (mk_real_int64 40652592L); (mk_real_int64 5000L); (mk_real_int64 17594960L); (mk_real_int64 1100L); (mk_real_int64 10930000L); (mk_real_int64 21754125L); (mk_real_int64 960L); (mk_real_int64 43370935L); (mk_real_int64 22820960L); (mk_real_int64 10710000L); (mk_real_int64 17597500L); (mk_real_int64 2910000L); (mk_real_int64 31810000L); (mk_real_int64 31815680L); ]); ("y8_hi", [7; 10; ], [(mk_real_int64 90000L); (mk_real_int64 90000L); ]); ("ye_hi", [16; 18; 19; 36; 39; 40; 48; 53; ], [(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", [14; 17; 20; 23; 26; 46; 47; 54; 56; 59; 63; 65; ], [(mk_real_int64 10000L); (mk_real_int64 6960000L); (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 2910000L); (mk_real_int64 10000L); (mk_real_int64 10000L); ]); ("yn_hi", [0; 3; 4; 7; 8; 9; 10; 12; ], [(mk_real_int64 3754L); (mk_real_int64 3754L); (mk_real_int64 3754L); (mk_real_int64 19378L); (mk_real_int64 13754L); (mk_real_int64 11826L); (mk_real_int64 5965L); (mk_real_int64 13754L); ]); ("yn_lo", [1; 2; 5; 6; 11; 13; ], [(mk_real_int64 10382L); (mk_real_int64 382L); (mk_real_int64 8174L); (mk_real_int64 6246L); (mk_real_int64 16246L); (mk_real_int64 6246L); ]); ];;end;; concl (Test_case.result)let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;