formal_lp/old/ineqs/tests2/74394196986_out.hl

   1 needs "nobranching_lp.hl";;
   2 \r
   3 module Test_case = struct\r
   4 let hypermap_string = "74394196986 22 4 0 1 2 3 4 0 3 4 5 3 4 3 6 3 6 3 2 4 6 2 7 8 3 7 2 1 3 7 1 9 3 9 1 10 3 10 1 0 3 10 0 5 3 10 5 11 3 11 5 12 3 12 5 4 3 12 4 13 3 13 4 6 3 13 6 8 3 8 7 14 3 14 7 9 3 14 9 11 3 9 10 11 4 14 11 12 13 3 13 8 14 ";;\r
   5 let precision = 4;;\r
   6 (***************)\r
   7 (* Constraints *)\r
   8 (***************)\r
   9 let constraints = [\r
  10 ("azim_sum", [1; 2; 5; 7; 10; ], [(mk_real_int64 317L); (mk_real_int64 4116L); (mk_real_int64 1351L); (mk_real_int64 937L); (mk_real_int64 3610L); ]);\r
  11 ("azim_sum_neg", [4; 6; 9; 13; ], [(mk_real_int64 508L); (mk_real_int64 350L); (mk_real_int64 375L); (mk_real_int64 1008L); ]);\r
  12 ("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 10357L); (mk_real_int64 10087L); (mk_real_int64 10357L); (mk_real_int64 10357L); (mk_real_int64 10865L); (mk_real_int64 11244L); (mk_real_int64 11325L); (mk_real_int64 10147L); (mk_real_int64 10091L); (mk_real_int64 10091L); (mk_real_int64 11293L); (mk_real_int64 10357L); (mk_real_int64 11293L); (mk_real_int64 10087L); (mk_real_int64 11293L); ]);\r
  13 ("sol_sum3", [12; 13; ], [(mk_real_int64 1008L); (mk_real_int64 1008L); ]);\r
  14 ("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; ], [(mk_real_int64 10357L); (mk_real_int64 10357L); (mk_real_int64 10147L); (mk_real_int64 10091L); (mk_real_int64 10091L); (mk_real_int64 10091L); (mk_real_int64 10091L); (mk_real_int64 10091L); (mk_real_int64 10357L); (mk_real_int64 10357L); (mk_real_int64 10357L); (mk_real_int64 10975L); (mk_real_int64 10087L); (mk_real_int64 10087L); (mk_real_int64 10091L); (mk_real_int64 10091L); (mk_real_int64 10091L); (mk_real_int64 10087L); ]);\r
  15 ("tau_sum4_neg", [0; 1; 2; 3; ], [(mk_real_int64 10357L); (mk_real_int64 10357L); (mk_real_int64 10087L); (mk_real_int64 11293L); ]);\r
  16 ("ln_def_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 1419L); (mk_real_int64 1122L); (mk_real_int64 1419L); (mk_real_int64 1419L); (mk_real_int64 1979L); (mk_real_int64 2397L); (mk_real_int64 2487L); (mk_real_int64 1187L); (mk_real_int64 1127L); (mk_real_int64 1127L); (mk_real_int64 2451L); (mk_real_int64 1419L); (mk_real_int64 2451L); (mk_real_int64 1122L); (mk_real_int64 2451L); ]);\r
  17 ("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 65075L); (mk_real_int64 63380L); (mk_real_int64 65075L); (mk_real_int64 65075L); (mk_real_int64 68264L); (mk_real_int64 70647L); (mk_real_int64 71158L); (mk_real_int64 63753L); (mk_real_int64 63407L); (mk_real_int64 63407L); (mk_real_int64 70955L); (mk_real_int64 65075L); (mk_real_int64 70955L); (mk_real_int64 63380L); (mk_real_int64 70955L); ]);\r
  18 ("edge_sym", [5; 15; 26; 34; ], [(mk_real_int64 724L); (mk_real_int64 127L); (mk_real_int64 2503L); (mk_real_int64 387L); ]);\r
  19 ("edge_sym_neg", [9; 10; 13; 20; 22; 23; 25; 29; 32; 35; 37; 41; 43; 47; 50; 52; 53; 58; ], [(mk_real_int64 724L); (mk_real_int64 724L); (mk_real_int64 127L); (mk_real_int64 387L); (mk_real_int64 120L); (mk_real_int64 1884L); (mk_real_int64 444L); (mk_real_int64 347L); (mk_real_int64 1447L); (mk_real_int64 41L); (mk_real_int64 387L); (mk_real_int64 848L); (mk_real_int64 661L); (mk_real_int64 933L); (mk_real_int64 114L); (mk_real_int64 89L); (mk_real_int64 89L); (mk_real_int64 388L); ]);\r
  20 ("y1_def_neg", [10; 11; 15; 19; 20; 21; 22; 26; 28; 29; 31; 34; 35; 38; 40; 44; 45; 47; 48; 50; 51; 52; 53; 54; 55; 56; 57; 59; 62; 67; ], [(mk_real_int64 1043L); (mk_real_int64 1686L); (mk_real_int64 100L); (mk_real_int64 58L); (mk_real_int64 313L); (mk_real_int64 88L); (mk_real_int64 1480L); (mk_real_int64 369L); (mk_real_int64 557L); (mk_real_int64 159L); (mk_real_int64 1899L); (mk_real_int64 46L); (mk_real_int64 1873L); (mk_real_int64 557L); (mk_real_int64 1221L); (mk_real_int64 952L); (mk_real_int64 191L); (mk_real_int64 1510L); (mk_real_int64 152L); (mk_real_int64 634L); (mk_real_int64 152L); (mk_real_int64 609L); (mk_real_int64 14L); (mk_real_int64 721L); (mk_real_int64 33L); (mk_real_int64 1547L); (mk_real_int64 222L); (mk_real_int64 194L); (mk_real_int64 2139L); (mk_real_int64 1122L); ]);\r
  21 ("y1_def", [27; 30; 33; 61; 68; ], [(mk_real_int64 188L); (mk_real_int64 188L); (mk_real_int64 188L); (mk_real_int64 188L); (mk_real_int64 504L); ]);\r
  22 ("y2_def_neg", [10; 11; 20; 22; 26; 27; 28; 30; 31; 33; 35; 38; 40; 44; 47; 48; 50; 51; 52; 56; 59; 61; 62; 67; 68; ], [(mk_real_int64 1043L); (mk_real_int64 1686L); (mk_real_int64 313L); (mk_real_int64 204L); (mk_real_int64 614L); (mk_real_int64 57L); (mk_real_int64 557L); (mk_real_int64 57L); (mk_real_int64 1643L); (mk_real_int64 57L); (mk_real_int64 224L); (mk_real_int64 557L); (mk_real_int64 1221L); (mk_real_int64 952L); (mk_real_int64 1510L); (mk_real_int64 152L); (mk_real_int64 634L); (mk_real_int64 152L); (mk_real_int64 609L); (mk_real_int64 1547L); (mk_real_int64 194L); (mk_real_int64 57L); (mk_real_int64 248L); (mk_real_int64 1122L); (mk_real_int64 153L); ]);\r
  23 ("y2_def", [15; 19; 21; 29; 34; 45; 53; 54; 55; 57; ], [(mk_real_int64 127L); (mk_real_int64 90L); (mk_real_int64 105L); (mk_real_int64 97L); (mk_real_int64 28L); (mk_real_int64 116L); (mk_real_int64 8L); (mk_real_int64 437L); (mk_real_int64 20L); (mk_real_int64 134L); ]);\r
  24 ("y3_def_neg", [10; 11; 20; 22; 26; 27; 28; 30; 31; 33; 35; 38; 40; 44; 47; 48; 50; 51; 52; 56; 59; 61; 62; 67; 68; ], [(mk_real_int64 1043L); (mk_real_int64 1686L); (mk_real_int64 313L); (mk_real_int64 204L); (mk_real_int64 614L); (mk_real_int64 57L); (mk_real_int64 557L); (mk_real_int64 57L); (mk_real_int64 1643L); (mk_real_int64 57L); (mk_real_int64 224L); (mk_real_int64 557L); (mk_real_int64 1221L); (mk_real_int64 952L); (mk_real_int64 1510L); (mk_real_int64 152L); (mk_real_int64 634L); (mk_real_int64 152L); (mk_real_int64 609L); (mk_real_int64 1547L); (mk_real_int64 194L); (mk_real_int64 57L); (mk_real_int64 248L); (mk_real_int64 1122L); (mk_real_int64 153L); ]);\r
  25 ("y3_def", [15; 19; 21; 29; 34; 45; 53; 54; 55; 57; ], [(mk_real_int64 127L); (mk_real_int64 90L); (mk_real_int64 105L); (mk_real_int64 97L); (mk_real_int64 28L); (mk_real_int64 116L); (mk_real_int64 8L); (mk_real_int64 437L); (mk_real_int64 20L); (mk_real_int64 134L); ]);\r
  26 ("y4_def_neg", [2; 3; 7; 8; 9; 10; 14; 16; 17; 19; 22; 23; 26; 28; 32; 33; 35; 38; 40; 41; 42; 43; 44; 45; 47; 50; ], [(mk_real_int64 724L); (mk_real_int64 1171L); (mk_real_int64 169L); (mk_real_int64 217L); (mk_real_int64 197L); (mk_real_int64 1988L); (mk_real_int64 97L); (mk_real_int64 387L); (mk_real_int64 182L); (mk_real_int64 1390L); (mk_real_int64 53L); (mk_real_int64 2050L); (mk_real_int64 387L); (mk_real_int64 848L); (mk_real_int64 661L); (mk_real_int64 218L); (mk_real_int64 1049L); (mk_real_int64 440L); (mk_real_int64 423L); (mk_real_int64 15L); (mk_real_int64 823L); (mk_real_int64 38L); (mk_real_int64 1074L); (mk_real_int64 253L); (mk_real_int64 134L); (mk_real_int64 2446L); ]);\r
  27 ("y4_def", [15; 18; 21; 36; 39; 49; 51; 52; ], [(mk_real_int64 290L); (mk_real_int64 290L); (mk_real_int64 290L); (mk_real_int64 326L); (mk_real_int64 326L); (mk_real_int64 290L); (mk_real_int64 242L); (mk_real_int64 779L); ]);\r
  28 ("y5_def_neg", [10; 11; 20; 26; 27; 28; 30; 31; 33; 38; 40; 44; 47; 50; 52; 56; 59; 61; 67; 68; ], [(mk_real_int64 724L); (mk_real_int64 1171L); (mk_real_int64 217L); (mk_real_int64 444L); (mk_real_int64 57L); (mk_real_int64 387L); (mk_real_int64 57L); (mk_real_int64 1112L); (mk_real_int64 57L); (mk_real_int64 387L); (mk_real_int64 848L); (mk_real_int64 661L); (mk_real_int64 1049L); (mk_real_int64 440L); (mk_real_int64 423L); (mk_real_int64 1074L); (mk_real_int64 134L); (mk_real_int64 57L); (mk_real_int64 779L); (mk_real_int64 153L); ]);\r
  29 ("y5_def", [15; 19; 21; 22; 29; 34; 35; 45; 48; 51; 53; 54; 55; 57; 62; ], [(mk_real_int64 127L); (mk_real_int64 90L); (mk_real_int64 105L); (mk_real_int64 77L); (mk_real_int64 97L); (mk_real_int64 28L); (mk_real_int64 69L); (mk_real_int64 116L); (mk_real_int64 326L); (mk_real_int64 326L); (mk_real_int64 8L); (mk_real_int64 437L); (mk_real_int64 20L); (mk_real_int64 134L); (mk_real_int64 98L); ]);\r
  30 ("y6_def_neg", [10; 20; 26; 28; 31; 47; 50; 52; 56; 59; 61; 68; ], [(mk_real_int64 724L); (mk_real_int64 217L); (mk_real_int64 444L); (mk_real_int64 387L); (mk_real_int64 290L); (mk_real_int64 1049L); (mk_real_int64 440L); (mk_real_int64 423L); (mk_real_int64 1074L); (mk_real_int64 134L); (mk_real_int64 57L); (mk_real_int64 153L); ]);\r
  31 ("y6_def", [11; 12; 13; 15; 19; 21; 22; 24; 27; 29; 30; 33; 34; 35; 39; 42; 45; 46; 48; 49; 51; 53; 54; 55; 57; 62; 67; ], [(mk_real_int64 724L); (mk_real_int64 1171L); (mk_real_int64 1044L); (mk_real_int64 127L); (mk_real_int64 217L); (mk_real_int64 309L); (mk_real_int64 77L); (mk_real_int64 216L); (mk_real_int64 1012L); (mk_real_int64 97L); (mk_real_int64 1459L); (mk_real_int64 3470L); (mk_real_int64 28L); (mk_real_int64 69L); (mk_real_int64 1235L); (mk_real_int64 1509L); (mk_real_int64 1709L); (mk_real_int64 1990L); (mk_real_int64 1373L); (mk_real_int64 114L); (mk_real_int64 438L); (mk_real_int64 8L); (mk_real_int64 1143L); (mk_real_int64 3781L); (mk_real_int64 134L); (mk_real_int64 98L); (mk_real_int64 268L); ]);\r
  32 ("RHA", [6; 7; 8; 10; 11; 14; 16; 20; 25; 28; 32; 34; 36; 37; 40; 41; 43; 44; 46; 47; 48; 49; 52; 53; 57; 59; 67; 69; ], [(mk_real_int64 887L); (mk_real_int64 508L); (mk_real_int64 887L); (mk_real_int64 968L); (mk_real_int64 968L); (mk_real_int64 1238L); (mk_real_int64 59L); (mk_real_int64 210L); (mk_real_int64 266L); (mk_real_int64 266L); (mk_real_int64 773L); (mk_real_int64 696L); (mk_real_int64 936L); (mk_real_int64 508L); (mk_real_int64 508L); (mk_real_int64 887L); (mk_real_int64 887L); (mk_real_int64 936L); (mk_real_int64 269L); (mk_real_int64 350L); (mk_real_int64 1206L); (mk_real_int64 1238L); (mk_real_int64 59L); (mk_real_int64 1183L); (mk_real_int64 832L); (mk_real_int64 1201L); (mk_real_int64 1206L); (mk_real_int64 1206L); ]);\r
  33 ("RHB", [2; 13; 19; 65; ], [(mk_real_int64 270L); (mk_real_int64 270L); (mk_real_int64 59L); (mk_real_int64 936L); ]);\r
  34 ("tau4", [0; 1; 2; 3; ], [(mk_real_int64 4922L); (mk_real_int64 7402L); (mk_real_int64 5373L); (mk_real_int64 4097L); ]);\r
  35 ("ineq105", [9; ], [(mk_real_int64 317L); ]);\r
  36 ("ineq106", [9; 10; 17; 19; 22; 23; 33; 41; 42; 43; 45; 50; ], [(mk_real_int64 55L); (mk_real_int64 266L); (mk_real_int64 266L); (mk_real_int64 266L); (mk_real_int64 77L); (mk_real_int64 1201L); (mk_real_int64 318L); (mk_real_int64 23L); (mk_real_int64 1201L); (mk_real_int64 55L); (mk_real_int64 370L); (mk_real_int64 1201L); ]);\r
  37 ("ineq107", [14; 15; 18; 21; 49; 52; ], [(mk_real_int64 375L); (mk_real_int64 375L); (mk_real_int64 375L); (mk_real_int64 375L); (mk_real_int64 375L); (mk_real_int64 1008L); ]);\r
  38 ("ineq108", [7; 9; 10; 23; 50; ], [(mk_real_int64 247L); (mk_real_int64 233L); (mk_real_int64 1704L); (mk_real_int64 819L); (mk_real_int64 1224L); ]);\r
  39 ("ineq109", [36; 39; ], [(mk_real_int64 1008L); (mk_real_int64 1008L); ]);\r
  40 ("ineq111", [2; 3; 8; 10; 14; 16; 19; 23; 26; 28; 32; 35; 38; 40; 44; 47; 50; 51; ], [(mk_real_int64 5795L); (mk_real_int64 9369L); (mk_real_int64 1740L); (mk_real_int64 5114L); (mk_real_int64 3093L); (mk_real_int64 3093L); (mk_real_int64 9667L); (mk_real_int64 5331L); (mk_real_int64 3094L); (mk_real_int64 6782L); (mk_real_int64 5287L); (mk_real_int64 8388L); (mk_real_int64 3521L); (mk_real_int64 3384L); (mk_real_int64 8595L); (mk_real_int64 1076L); (mk_real_int64 6279L); (mk_real_int64 6235L); ]);\r
  41 ("ineq114", [0; 2; 3; 6; 8; 9; 10; 13; 16; 20; 22; 23; 24; 29; 31; 32; 34; 36; 37; 40; 41; 43; 45; 47; 50; 51; 53; ], [(mk_real_int64 3575L); (mk_real_int64 988L); (mk_real_int64 988L); (mk_real_int64 1497L); (mk_real_int64 6911L); (mk_real_int64 1125L); (mk_real_int64 3852L); (mk_real_int64 6999L); (mk_real_int64 6999L); (mk_real_int64 424L); (mk_real_int64 302L); (mk_real_int64 4459L); (mk_real_int64 7263L); (mk_real_int64 3575L); (mk_real_int64 3575L); (mk_real_int64 1495L); (mk_real_int64 2587L); (mk_real_int64 3537L); (mk_real_int64 3029L); (mk_real_int64 3202L); (mk_real_int64 3501L); (mk_real_int64 1497L); (mk_real_int64 1329L); (mk_real_int64 7687L); (mk_real_int64 3812L); (mk_real_int64 1926L); (mk_real_int64 1926L); ]);\r
  42 ("ineq119", [11; 14; ], [(mk_real_int64 2226L); (mk_real_int64 2428L); ]);\r
  43 ("ineq120", [1; 6; 8; 10; 13; ], [(mk_real_int64 5435L); (mk_real_int64 2955L); (mk_real_int64 1173L); (mk_real_int64 1316L); (mk_real_int64 4768L); ]);\r
  44 ];;\r
  45 \r
  46 (***************)\r
  47 (* Variables   *)\r
  48 (***************)\r
  49 let target_variables = [\r
  50 ("ln_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; ], [(mk_real_int64 48450L); (mk_real_int64 51480L); (mk_real_int64 48450L); (mk_real_int64 48450L); (mk_real_int64 54944L); (mk_real_int64 55162L); (mk_real_int64 58868L); (mk_real_int64 47238L); (mk_real_int64 54122L); (mk_real_int64 54122L); (mk_real_int64 54930L); (mk_real_int64 48450L); (mk_real_int64 54930L); (mk_real_int64 51480L); (mk_real_int64 54930L); ]);\r
  51 ];;\r
  52 \r
  53 (*************************)\r
  54 \r
  55 let variable_bounds = [\r
  56 ("azim_hi", [2; 10; 11; 13; 14; 16; 18; 20; 21; 32; 34; 35; 36; 48; 49; 52; 53; 55; 59; 62; 64; 65; ], [(mk_real_int64 3850L); (mk_real_int64 4880L); (mk_real_int64 4880L); (mk_real_int64 3850L); (mk_real_int64 3129L); (mk_real_int64 6068L); (mk_real_int64 1220L); (mk_real_int64 2860L); (mk_real_int64 2500L); (mk_real_int64 4240L); (mk_real_int64 10520L); (mk_real_int64 3340L); (mk_real_int64 6380L); (mk_real_int64 1620L); (mk_real_int64 1540L); (mk_real_int64 4520L); (mk_real_int64 6260L); (mk_real_int64 1220L); (mk_real_int64 10620L); (mk_real_int64 3120L); (mk_real_int64 8064L); (mk_real_int64 3840L); ]);\r
  57 ("azim_lo", [1; 6; 8; 17; 19; 22; 25; 28; 41; 43; 44; 46; 57; 67; 69; ], [(mk_real_int64 745L); (mk_real_int64 1785L); (mk_real_int64 500L); (mk_real_int64 3780L); (mk_real_int64 6455L); (mk_real_int64 6480L); (mk_real_int64 6260L); (mk_real_int64 6260L); (mk_real_int64 500L); (mk_real_int64 500L); (mk_real_int64 1300L); (mk_real_int64 5380L); (mk_real_int64 460L); (mk_real_int64 3240L); (mk_real_int64 3240L); ]);\r
  58 ("rhazim_lo", [16; 21; 32; 34; 35; 52; 54; 55; 59; 62; ], [(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); ]);\r
  59 ("rhazim_hi", [19; ], [(mk_real_int64 10000L); ]);\r
  60 ("rho_hi", [0; 2; 3; 4; 5; 7; 10; 11; 12; 14; ], [(mk_real_int64 1024L); (mk_real_int64 1024L); (mk_real_int64 1024L); (mk_real_int64 29680L); (mk_real_int64 13008L); (mk_real_int64 26304L); (mk_real_int64 11776L); (mk_real_int64 1024L); (mk_real_int64 11776L); (mk_real_int64 11776L); ]);\r
  61 ("rho_lo", [1; 6; 8; 9; 13; ], [(mk_real_int64 13616L); (mk_real_int64 7600L); (mk_real_int64 32288L); (mk_real_int64 32288L); (mk_real_int64 13616L); ]);\r
  62 ("tau_hi", [2; 4; 5; 7; 8; 10; 17; 18; ], [(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); ]);\r
  63 ("y1_lo", [10; 11; 19; 20; 22; 26; 27; 29; 30; 31; 33; 34; 48; 51; 52; 56; 61; 67; ], [(mk_real_int64 1000L); (mk_real_int64 4200L); (mk_real_int64 450L); (mk_real_int64 2000L); (mk_real_int64 5600L); (mk_real_int64 2400L); (mk_real_int64 5000L); (mk_real_int64 6000L); (mk_real_int64 5000L); (mk_real_int64 6600L); (mk_real_int64 5000L); (mk_real_int64 2000L); (mk_real_int64 2080L); (mk_real_int64 2080L); (mk_real_int64 1200L); (mk_real_int64 1000L); (mk_real_int64 5000L); (mk_real_int64 3000L); ]);\r
  64 ("y1_hi", [15; 21; 28; 35; 38; 40; 44; 45; 47; 50; 53; 54; 59; 62; ], [(mk_real_int64 1450L); (mk_real_int64 2450L); (mk_real_int64 2600L); (mk_real_int64 3550L); (mk_real_int64 800L); (mk_real_int64 2400L); (mk_real_int64 3400L); (mk_real_int64 2000L); (mk_real_int64 1600L); (mk_real_int64 2200L); (mk_real_int64 2000L); (mk_real_int64 4000L); (mk_real_int64 3200L); (mk_real_int64 5400L); ]);\r
  65 ("y2_lo", [10; 11; 19; 20; 21; 29; 31; 35; 45; 48; 51; 52; 56; 67; 68; ], [(mk_real_int64 1000L); (mk_real_int64 4200L); (mk_real_int64 1167L); (mk_real_int64 2000L); (mk_real_int64 1968L); (mk_real_int64 2026L); (mk_real_int64 2626L); (mk_real_int64 5020L); (mk_real_int64 2798L); (mk_real_int64 2080L); (mk_real_int64 2080L); (mk_real_int64 1200L); (mk_real_int64 1000L); (mk_real_int64 3000L); (mk_real_int64 2160L); ]);\r
  66 ("y2_hi", [15; 22; 26; 28; 34; 38; 40; 44; 47; 50; 53; 54; 55; 57; 59; 62; ], [(mk_real_int64 4340L); (mk_real_int64 3630L); (mk_real_int64 2600L); (mk_real_int64 2600L); (mk_real_int64 203L); (mk_real_int64 800L); (mk_real_int64 2400L); (mk_real_int64 3400L); (mk_real_int64 1600L); (mk_real_int64 2200L); (mk_real_int64 3697L); (mk_real_int64 439L); (mk_real_int64 145L); (mk_real_int64 6430L); (mk_real_int64 3200L); (mk_real_int64 2375L); ]);\r
  67 ("y3_lo", [10; 11; 19; 20; 21; 29; 31; 35; 45; 48; 51; 52; 56; 67; 68; ], [(mk_real_int64 1000L); (mk_real_int64 4200L); (mk_real_int64 1167L); (mk_real_int64 2000L); (mk_real_int64 1968L); (mk_real_int64 2026L); (mk_real_int64 2626L); (mk_real_int64 5020L); (mk_real_int64 2798L); (mk_real_int64 2080L); (mk_real_int64 2080L); (mk_real_int64 1200L); (mk_real_int64 1000L); (mk_real_int64 3000L); (mk_real_int64 2160L); ]);\r
  68 ("y3_hi", [15; 22; 26; 28; 34; 38; 40; 44; 47; 50; 53; 54; 55; 57; 59; 62; ], [(mk_real_int64 4340L); (mk_real_int64 3630L); (mk_real_int64 2600L); (mk_real_int64 2600L); (mk_real_int64 203L); (mk_real_int64 800L); (mk_real_int64 2400L); (mk_real_int64 3400L); (mk_real_int64 1600L); (mk_real_int64 2200L); (mk_real_int64 3697L); (mk_real_int64 439L); (mk_real_int64 145L); (mk_real_int64 6430L); (mk_real_int64 3200L); (mk_real_int64 2375L); ]);\r
  69 ("y4_lo", [2; 3; 7; 8; 9; 10; 15; 17; 18; 19; 21; 23; 36; 38; 39; 41; 44; 45; 47; 49; 51; ], [(mk_real_int64 3750L); (mk_real_int64 1250L); (mk_real_int64 1950L); (mk_real_int64 5000L); (mk_real_int64 2800L); (mk_real_int64 7000L); (mk_real_int64 1250L); (mk_real_int64 2100L); (mk_real_int64 1250L); (mk_real_int64 5850L); (mk_real_int64 1250L); (mk_real_int64 750L); (mk_real_int64 2144L); (mk_real_int64 1250L); (mk_real_int64 2144L); (mk_real_int64 7550L); (mk_real_int64 3750L); (mk_real_int64 4500L); (mk_real_int64 5000L); (mk_real_int64 1250L); (mk_real_int64 10220000L); ]);\r
  70 ("y4_hi", [14; 16; 22; 26; 28; 32; 33; 35; 42; 43; 51; 52; ], [(mk_real_int64 2500L); (mk_real_int64 3750L); (mk_real_int64 2550L); (mk_real_int64 2500L); (mk_real_int64 2500L); (mk_real_int64 1250L); (mk_real_int64 1700L); (mk_real_int64 5000L); (mk_real_int64 3150L); (mk_real_int64 3250L); (mk_real_int64 6250L); (mk_real_int64 1840L); ]);\r
  71 ("y5_lo", [10; 11; 19; 20; 21; 29; 35; 45; 48; 50; 51; 56; 59; 62; 67; 68; ], [(mk_real_int64 3750L); (mk_real_int64 1250L); (mk_real_int64 1167L); (mk_real_int64 5000L); (mk_real_int64 1968L); (mk_real_int64 2026L); (mk_real_int64 2970L); (mk_real_int64 2798L); (mk_real_int64 2144L); (mk_real_int64 1250L); (mk_real_int64 2144L); (mk_real_int64 3750L); (mk_real_int64 5000L); (mk_real_int64 4175L); (mk_real_int64 3750L); (mk_real_int64 2160L); ]);\r
  72 ("y5_hi", [15; 22; 26; 28; 31; 34; 38; 40; 44; 47; 53; 54; 55; 57; ], [(mk_real_int64 4340L); (mk_real_int64 6330L); (mk_real_int64 3750L); (mk_real_int64 3750L); (mk_real_int64 4224L); (mk_real_int64 203L); (mk_real_int64 2500L); (mk_real_int64 2500L); (mk_real_int64 1250L); (mk_real_int64 5000L); (mk_real_int64 3697L); (mk_real_int64 439L); (mk_real_int64 145L); (mk_real_int64 6430L); ]);\r
  73 ("y6_lo", [10; 11; 12; 13; 19; 20; 21; 24; 27; 29; 30; 31; 33; 35; 38; 39; 40; 42; 44; 45; 46; 48; 49; 50; 51; 54; 55; 56; 59; 62; 67; 68; ], [(mk_real_int64 3750L); (mk_real_int64 18951250L); (mk_real_int64 11710000L); (mk_real_int64 10440000L); (mk_real_int64 1271167L); (mk_real_int64 5000L); (mk_real_int64 2050000L); (mk_real_int64 2160000L); (mk_real_int64 10690000L); (mk_real_int64 2026L); (mk_real_int64 15160000L); (mk_real_int64 8220000L); (mk_real_int64 35270000L); (mk_real_int64 2970L); (mk_real_int64 3870000L); (mk_real_int64 12350000L); (mk_real_int64 8480000L); (mk_real_int64 15090000L); (mk_real_int64 6610000L); (mk_real_int64 15940000L); (mk_real_int64 19900000L); (mk_real_int64 10472144L); (mk_real_int64 1140000L); (mk_real_int64 1250L); (mk_real_int64 1130000L); (mk_real_int64 7060000L); (mk_real_int64 37610000L); (mk_real_int64 3750L); (mk_real_int64 5000L); (mk_real_int64 4175L); (mk_real_int64 10473750L); (mk_real_int64 2160L); ]);\r
  74 ("y6_hi", [15; 21; 22; 26; 28; 31; 34; 38; 40; 44; 45; 47; 51; 53; 54; 55; 57; ], [(mk_real_int64 4340L); (mk_real_int64 8032L); (mk_real_int64 6330L); (mk_real_int64 3750L); (mk_real_int64 3750L); (mk_real_int64 4224L); (mk_real_int64 203L); (mk_real_int64 2500L); (mk_real_int64 2500L); (mk_real_int64 1250L); (mk_real_int64 7202L); (mk_real_int64 5000L); (mk_real_int64 7856L); (mk_real_int64 3697L); (mk_real_int64 439L); (mk_real_int64 145L); (mk_real_int64 6430L); ]);\r
  75 ("ye_hi", [20; 23; 33; 58; 67; ], [(mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); ]);\r
  76 ("ye_lo", [5; 21; 24; 26; 27; 45; 46; 56; ], [(mk_real_int64 7240000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 29470000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 10000L); (mk_real_int64 6750000L); ]);\r
  77 ("yn_lo", [0; 2; 3; 5; 7; 8; 10; 11; 12; 14; ], [(mk_real_int64 1211L); (mk_real_int64 1211L); (mk_real_int64 1211L); (mk_real_int64 3293L); (mk_real_int64 12803L); (mk_real_int64 6663L); (mk_real_int64 14819L); (mk_real_int64 11211L); (mk_real_int64 4819L); (mk_real_int64 4819L); ]);\r
  78 ("yn_hi", [1; 4; 6; 9; 13; ], [(mk_real_int64 7182L); (mk_real_int64 8149L); (mk_real_int64 7497L); (mk_real_int64 33337L); (mk_real_int64 7182L); ]);\r
  79 ];;\r
  80 let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
  81 end;;\r
  82 \r
  83 concl (Test_case.result)\r