formal_lp/old/ineqs/tests/72977109430_out.hl

   1 needs "nobranching_lp.hl";;
   2 \r
   3 module Test_case = struct\r
   4 let hypermap_string = "72977109430 19 6 0 1 2 3 4 5 3 0 5 6 3 6 5 7 3 7 5 4 3 7 4 8 3 8 4 3 3 8 3 2 3 8 2 9 3 9 2 1 3 9 1 10 3 10 1 11 3 11 1 0 4 11 0 6 12 3 12 6 13 3 13 6 7 4 13 7 8 9 3 13 9 10 3 12 13 10 3 10 11 12 ";;\r
   5 let precision = 3;;\r
   6 (***************)\r
   7 (* Constraints *)\r
   8 (***************)\r
   9 let constraints = [\r
  10 ("azim_sum_neg", [2; 8; 13; ], [(mk_real_int64 99L); (mk_real_int64 130L); (mk_real_int64 10L); ]);\r
  11 ("azim_sum", [6; 7; 9; 11; ], [(mk_real_int64 44L); (mk_real_int64 116L); (mk_real_int64 116L); (mk_real_int64 25L); ]);\r
  12 ("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 1082L); (mk_real_int64 1082L); (mk_real_int64 660L); (mk_real_int64 1082L); (mk_real_int64 1082L); (mk_real_int64 1082L); (mk_real_int64 1082L); (mk_real_int64 1279L); (mk_real_int64 1279L); (mk_real_int64 1279L); (mk_real_int64 1279L); (mk_real_int64 1032L); (mk_real_int64 699L); (mk_real_int64 699L); ]);\r
  13 ("sol_sum3_neg", [8; 10; 12; 13; ], [(mk_real_int64 7L); (mk_real_int64 271L); (mk_real_int64 44L); (mk_real_int64 247L); ]);\r
  14 ("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; ], [(mk_real_int64 1082L); (mk_real_int64 1082L); (mk_real_int64 1082L); (mk_real_int64 1082L); (mk_real_int64 660L); (mk_real_int64 660L); (mk_real_int64 1082L); (mk_real_int64 1082L); (mk_real_int64 1032L); (mk_real_int64 699L); (mk_real_int64 699L); (mk_real_int64 699L); (mk_real_int64 1082L); (mk_real_int64 1032L); (mk_real_int64 699L); (mk_real_int64 699L); ]);\r
  15 ("tau_sum4_neg", [0; 1; ], [(mk_real_int64 699L); (mk_real_int64 1279L); ]);\r
  16 ("tau_sum6_neg", [0; ], [(mk_real_int64 1082L); ]);\r
  17 ("ln_def_neg", [0; 1; 3; 4; 5; 6; 7; 8; 9; 10; 11; ], [(mk_real_int64 193L); (mk_real_int64 193L); (mk_real_int64 193L); (mk_real_int64 193L); (mk_real_int64 193L); (mk_real_int64 193L); (mk_real_int64 410L); (mk_real_int64 410L); (mk_real_int64 410L); (mk_real_int64 410L); (mk_real_int64 138L); ]);\r
  18 ("ln_def", [2; 12; 13; ], [(mk_real_int64 273L); (mk_real_int64 229L); (mk_real_int64 229L); ]);\r
  19 ("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 6798L); (mk_real_int64 6798L); (mk_real_int64 4146L); (mk_real_int64 6798L); (mk_real_int64 6798L); (mk_real_int64 6798L); (mk_real_int64 6798L); (mk_real_int64 8033L); (mk_real_int64 8033L); (mk_real_int64 8033L); (mk_real_int64 8033L); (mk_real_int64 6484L); (mk_real_int64 4395L); (mk_real_int64 4392L); ]);\r
  20 ("edge_sym", [1; 2; 23; 25; 29; 44; ], [(mk_real_int64 73L); (mk_real_int64 278L); (mk_real_int64 325L); (mk_real_int64 73L); (mk_real_int64 15L); (mk_real_int64 282L); ]);\r
  21 ("edge_sym_neg", [7; 8; 10; 11; 14; 16; 20; 31; 32; 34; 35; 38; 45; 55; 58; ], [(mk_real_int64 119L); (mk_real_int64 119L); (mk_real_int64 100L); (mk_real_int64 54L); (mk_real_int64 73L); (mk_real_int64 325L); (mk_real_int64 209L); (mk_real_int64 176L); (mk_real_int64 42L); (mk_real_int64 199L); (mk_real_int64 187L); (mk_real_int64 119L); (mk_real_int64 146L); (mk_real_int64 211L); (mk_real_int64 23L); ]);\r
  22 ("y1_def_neg", [6; 8; 9; 10; 11; 12; 15; 17; 18; 19; 20; 21; 23; 24; 25; 26; 27; 30; 31; 32; 33; 34; 37; 38; 40; 44; 45; 46; 48; 54; 56; 57; 58; 59; 60; ], [(mk_real_int64 195L); (mk_real_int64 10L); (mk_real_int64 10L); (mk_real_int64 110L); (mk_real_int64 11L); (mk_real_int64 105L); (mk_real_int64 340L); (mk_real_int64 40L); (mk_real_int64 293L); (mk_real_int64 253L); (mk_real_int64 69L); (mk_real_int64 293L); (mk_real_int64 372L); (mk_real_int64 40L); (mk_real_int64 195L); (mk_real_int64 145L); (mk_real_int64 105L); (mk_real_int64 148L); (mk_real_int64 23L); (mk_real_int64 159L); (mk_real_int64 321L); (mk_real_int64 208L); (mk_real_int64 94L); (mk_real_int64 67L); (mk_real_int64 93L); (mk_real_int64 352L); (mk_real_int64 348L); (mk_real_int64 57L); (mk_real_int64 296L); (mk_real_int64 70L); (mk_real_int64 33L); (mk_real_int64 348L); (mk_real_int64 32L); (mk_real_int64 149L); (mk_real_int64 94L); ]);\r
  23 ("y1_def", [22; 36; 43; 55; 61; ], [(mk_real_int64 49L); (mk_real_int64 239L); (mk_real_int64 5L); (mk_real_int64 43L); (mk_real_int64 5L); ]);\r
  24 ("y2_def", [8; 9; 11; 17; 18; 19; 21; 23; 24; 26; 30; 31; 33; 34; 36; 38; 40; 44; 45; 46; 54; 57; 58; 59; ], [(mk_real_int64 16L); (mk_real_int64 16L); (mk_real_int64 7L); (mk_real_int64 24L); (mk_real_int64 178L); (mk_real_int64 154L); (mk_real_int64 178L); (mk_real_int64 35L); (mk_real_int64 24L); (mk_real_int64 114L); (mk_real_int64 90L); (mk_real_int64 18L); (mk_real_int64 15L); (mk_real_int64 126L); (mk_real_int64 62L); (mk_real_int64 40L); (mk_real_int64 119L); (mk_real_int64 27L); (mk_real_int64 211L); (mk_real_int64 34L); (mk_real_int64 42L); (mk_real_int64 211L); (mk_real_int64 19L); (mk_real_int64 90L); ]);\r
  25 ("y2_def_neg", [6; 10; 12; 15; 20; 22; 25; 27; 32; 37; 43; 48; 55; 56; 60; 61; ], [(mk_real_int64 195L); (mk_real_int64 110L); (mk_real_int64 105L); (mk_real_int64 81L); (mk_real_int64 134L); (mk_real_int64 15L); (mk_real_int64 195L); (mk_real_int64 105L); (mk_real_int64 148L); (mk_real_int64 94L); (mk_real_int64 1L); (mk_real_int64 64L); (mk_real_int64 20L); (mk_real_int64 40L); (mk_real_int64 94L); (mk_real_int64 1L); ]);\r
  26 ("y3_def", [8; 9; 11; 17; 18; 19; 21; 23; 24; 26; 30; 31; 33; 34; 36; 38; 40; 44; 45; 46; 54; 57; 58; 59; ], [(mk_real_int64 16L); (mk_real_int64 16L); (mk_real_int64 7L); (mk_real_int64 24L); (mk_real_int64 178L); (mk_real_int64 154L); (mk_real_int64 178L); (mk_real_int64 35L); (mk_real_int64 24L); (mk_real_int64 114L); (mk_real_int64 90L); (mk_real_int64 18L); (mk_real_int64 15L); (mk_real_int64 126L); (mk_real_int64 62L); (mk_real_int64 40L); (mk_real_int64 119L); (mk_real_int64 27L); (mk_real_int64 211L); (mk_real_int64 34L); (mk_real_int64 42L); (mk_real_int64 211L); (mk_real_int64 19L); (mk_real_int64 90L); ]);\r
  27 ("y3_def_neg", [6; 10; 12; 15; 20; 22; 25; 27; 32; 37; 43; 48; 55; 56; 60; 61; ], [(mk_real_int64 195L); (mk_real_int64 110L); (mk_real_int64 105L); (mk_real_int64 81L); (mk_real_int64 134L); (mk_real_int64 15L); (mk_real_int64 195L); (mk_real_int64 105L); (mk_real_int64 148L); (mk_real_int64 94L); (mk_real_int64 1L); (mk_real_int64 64L); (mk_real_int64 20L); (mk_real_int64 40L); (mk_real_int64 94L); (mk_real_int64 1L); ]);\r
  28 ("y4_def_neg", [0; 2; 3; 4; 5; 6; 9; 11; 12; 13; 14; 15; 17; 18; 19; 20; 21; 24; 25; 26; 27; 28; 31; 32; 34; 35; 36; 38; 40; 41; 42; 43; 44; 45; 46; ], [(mk_real_int64 135L); (mk_real_int64 30L); (mk_real_int64 30L); (mk_real_int64 77L); (mk_real_int64 13L); (mk_real_int64 73L); (mk_real_int64 349L); (mk_real_int64 45L); (mk_real_int64 335L); (mk_real_int64 289L); (mk_real_int64 6L); (mk_real_int64 335L); (mk_real_int64 372L); (mk_real_int64 45L); (mk_real_int64 135L); (mk_real_int64 214L); (mk_real_int64 73L); (mk_real_int64 169L); (mk_real_int64 31L); (mk_real_int64 119L); (mk_real_int64 325L); (mk_real_int64 237L); (mk_real_int64 65L); (mk_real_int64 76L); (mk_real_int64 356L); (mk_real_int64 397L); (mk_real_int64 65L); (mk_real_int64 316L); (mk_real_int64 80L); (mk_real_int64 42L); (mk_real_int64 19L); (mk_real_int64 397L); (mk_real_int64 36L); (mk_real_int64 170L); (mk_real_int64 66L); ]);\r
  29 ("y4_def", [16; 30; 33; 47; ], [(mk_real_int64 76L); (mk_real_int64 157L); (mk_real_int64 8L); (mk_real_int64 7L); ]);\r
  30 ("y5_def", [8; 9; 11; 17; 18; 19; 21; 23; 24; 26; 30; 31; 33; 34; 37; 38; 40; 44; 45; 46; 54; 57; 58; 59; ], [(mk_real_int64 16L); (mk_real_int64 16L); (mk_real_int64 7L); (mk_real_int64 24L); (mk_real_int64 178L); (mk_real_int64 154L); (mk_real_int64 178L); (mk_real_int64 71L); (mk_real_int64 24L); (mk_real_int64 114L); (mk_real_int64 90L); (mk_real_int64 14L); (mk_real_int64 50L); (mk_real_int64 126L); (mk_real_int64 370L); (mk_real_int64 40L); (mk_real_int64 119L); (mk_real_int64 64L); (mk_real_int64 211L); (mk_real_int64 34L); (mk_real_int64 42L); (mk_real_int64 211L); (mk_real_int64 19L); (mk_real_int64 90L); ]);\r
  31 ("y5_def_neg", [6; 10; 12; 15; 20; 22; 25; 27; 32; 36; 43; 48; 55; 56; 60; 61; ], [(mk_real_int64 135L); (mk_real_int64 77L); (mk_real_int64 73L); (mk_real_int64 21L); (mk_real_int64 98L); (mk_real_int64 15L); (mk_real_int64 135L); (mk_real_int64 73L); (mk_real_int64 101L); (mk_real_int64 94L); (mk_real_int64 1L); (mk_real_int64 34L); (mk_real_int64 132L); (mk_real_int64 28L); (mk_real_int64 65L); (mk_real_int64 1L); ]);\r
  32 ("y6_def", [1; 6; 8; 9; 11; 12; 13; 15; 17; 18; 19; 21; 23; 24; 26; 30; 31; 33; 34; 38; 40; 43; 44; 45; 46; 47; 54; 57; 58; 59; 60; ], [(mk_real_int64 73L); (mk_real_int64 30L); (mk_real_int64 16L); (mk_real_int64 208L); (mk_real_int64 7L); (mk_real_int64 100L); (mk_real_int64 73L); (mk_real_int64 118L); (mk_real_int64 24L); (mk_real_int64 178L); (mk_real_int64 432L); (mk_real_int64 596L); (mk_real_int64 71L); (mk_real_int64 24L); (mk_real_int64 114L); (mk_real_int64 90L); (mk_real_int64 14L); (mk_real_int64 50L); (mk_real_int64 126L); (mk_real_int64 40L); (mk_real_int64 119L); (mk_real_int64 333L); (mk_real_int64 64L); (mk_real_int64 211L); (mk_real_int64 34L); (mk_real_int64 153L); (mk_real_int64 173L); (mk_real_int64 211L); (mk_real_int64 19L); (mk_real_int64 245L); (mk_real_int64 171L); ]);\r
  33 ("y6_def_neg", [10; 20; 22; 25; 27; 32; 36; 37; 48; 55; 56; 61; ], [(mk_real_int64 77L); (mk_real_int64 98L); (mk_real_int64 15L); (mk_real_int64 135L); (mk_real_int64 73L); (mk_real_int64 101L); (mk_real_int64 94L); (mk_real_int64 65L); (mk_real_int64 34L); (mk_real_int64 132L); (mk_real_int64 28L); (mk_real_int64 1L); ]);\r
  34 ("RHA", [11; 12; 17; 18; 21; 24; 27; 31; 34; 37; 38; 40; 41; 46; 53; 54; 58; 59; ], [(mk_real_int64 178L); (mk_real_int64 197L); (mk_real_int64 130L); (mk_real_int64 130L); (mk_real_int64 130L); (mk_real_int64 130L); (mk_real_int64 197L); (mk_real_int64 7L); (mk_real_int64 36L); (mk_real_int64 383L); (mk_real_int64 271L); (mk_real_int64 383L); (mk_real_int64 383L); (mk_real_int64 102L); (mk_real_int64 247L); (mk_real_int64 130L); (mk_real_int64 280L); (mk_real_int64 85L); ]);\r
  35 ("yy10", [17; 26; 37; ], [(mk_real_int64 3L); (mk_real_int64 3L); (mk_real_int64 132L); ]);\r
  36 ("tau4", [1; ], [(mk_real_int64 684L); ]);\r
  37 ("tau6", [0; ], [(mk_real_int64 1082L); ]);\r
  38 ("ineq105", [7; ], [(mk_real_int64 297L); ]);\r
  39 ("ineq106", [5; 9; 11; 12; 13; 15; 17; 18; 20; 24; 25; 27; 28; 32; 34; 35; 36; 38; 40; 43; 44; 45; ], [(mk_real_int64 18L); (mk_real_int64 197L); (mk_real_int64 66L); (mk_real_int64 488L); (mk_real_int64 422L); (mk_real_int64 488L); (mk_real_int64 422L); (mk_real_int64 66L); (mk_real_int64 197L); (mk_real_int64 247L); (mk_real_int64 43L); (mk_real_int64 332L); (mk_real_int64 346L); (mk_real_int64 111L); (mk_real_int64 383L); (mk_real_int64 580L); (mk_real_int64 95L); (mk_real_int64 197L); (mk_real_int64 116L); (mk_real_int64 580L); (mk_real_int64 53L); (mk_real_int64 248L); ]);\r
  40 ("ineq107", [14; 16; 30; 33; 41; 42; 47; ], [(mk_real_int64 99L); (mk_real_int64 99L); (mk_real_int64 272L); (mk_real_int64 10L); (mk_real_int64 97L); (mk_real_int64 10L); (mk_real_int64 9L); ]);\r
  41 ("ineq108", [2; 3; 9; 20; 26; 27; 34; 38; ], [(mk_real_int64 44L); (mk_real_int64 44L); (mk_real_int64 116L); (mk_real_int64 116L); (mk_real_int64 18L); (mk_real_int64 25L); (mk_real_int64 17L); (mk_real_int64 72L); ]);\r
  42 ("ineq110", [25; 30; 38; 41; ], [(mk_real_int64 7L); (mk_real_int64 271L); (mk_real_int64 44L); (mk_real_int64 247L); ]);\r
  43 ("ineq111", [0; 4; 6; 9; 14; 17; 19; 21; 26; 27; 31; 34; 38; 41; 42; 46; ], [(mk_real_int64 1082L); (mk_real_int64 612L); (mk_real_int64 582L); (mk_real_int64 1082L); (mk_real_int64 660L); (mk_real_int64 660L); (mk_real_int64 1082L); (mk_real_int64 582L); (mk_real_int64 858L); (mk_real_int64 642L); (mk_real_int64 522L); (mk_real_int64 656L); (mk_real_int64 990L); (mk_real_int64 549L); (mk_real_int64 212L); (mk_real_int64 523L); ]);\r
  44 ("ineq113", [41; ], [(mk_real_int64 483L); ]);\r
  45 ("ineq114", [5; 6; 21; 24; 28; 31; 34; 36; 44; 45; ], [(mk_real_int64 470L); (mk_real_int64 499L); (mk_real_int64 499L); (mk_real_int64 174L); (mk_real_int64 58L); (mk_real_int64 178L); (mk_real_int64 43L); (mk_real_int64 92L); (mk_real_int64 487L); (mk_real_int64 176L); ]);\r
  46 ("ineq119", [3; 6; ], [(mk_real_int64 21L); (mk_real_int64 288L); ]);\r
  47 ("ineq120", [1; 2; 5; 7; ], [(mk_real_int64 114L); (mk_real_int64 564L); (mk_real_int64 153L); (mk_real_int64 153L); ]);\r
  48 ];;\r
  49 \r
  50 (***************)\r
  51 (* Variables   *)\r
  52 (***************)\r
  53 let target_variables = [\r
  54 ("ln_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; ], [(mk_real_int64 3350L); (mk_real_int64 3350L); (mk_real_int64 1450L); (mk_real_int64 3350L); (mk_real_int64 3350L); (mk_real_int64 3350L); (mk_real_int64 3350L); (mk_real_int64 4225L); (mk_real_int64 4225L); (mk_real_int64 4225L); (mk_real_int64 4225L); (mk_real_int64 3300L); (mk_real_int64 1875L); (mk_real_int64 2400L); ]);\r
  55 ];;\r
  56 \r
  57 (*************************)\r
  58 \r
  59 let variable_bounds = [\r
  60 ("azim_hi", [3; 11; 34; 40; 41; 42; 54; 59; 61; ], [(mk_real_int64 99000L); (mk_real_int64 220L); (mk_real_int64 308L); (mk_real_int64 412L); (mk_real_int64 512L); (mk_real_int64 487L); (mk_real_int64 1000L); (mk_real_int64 176L); (mk_real_int64 1000L); ]);\r
  61 ("azim_lo", [12; 27; 30; 36; 37; 44; 46; 50; 51; 52; 55; 58; ], [(mk_real_int64 626L); (mk_real_int64 626L); (mk_real_int64 76L); (mk_real_int64 1000L); (mk_real_int64 572L); (mk_real_int64 82L); (mk_real_int64 408L); (mk_real_int64 26L); (mk_real_int64 464L); (mk_real_int64 26L); (mk_real_int64 97L); (mk_real_int64 138L); ]);\r
  62 ("rhazim_lo", [11; 17; 18; 21; 24; 33; 34; 38; 54; ], [(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); ]);\r
  63 ("rhazim_hi", [3; ], [(mk_real_int64 422000L); ]);\r
  64 ("rho_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 13; ], [(mk_real_int64 1288L); (mk_real_int64 1288L); (mk_real_int64 1440L); (mk_real_int64 1288L); (mk_real_int64 1288L); (mk_real_int64 1288L); (mk_real_int64 1288L); (mk_real_int64 4236L); (mk_real_int64 4236L); (mk_real_int64 4236L); (mk_real_int64 4236L); (mk_real_int64 1088L); (mk_real_int64 516L); ]);\r
  65 ("rho_lo", [12; ], [(mk_real_int64 2484L); ]);\r
  66 ("tau_hi", [10; 11; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
  67 ("tau_lo", [3; 8; 15; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
  68 ("y1_hi", [6; 11; 12; 17; 18; 21; 22; 24; 25; 27; 32; 33; 34; 37; 38; 44; 54; 55; 58; 59; ], [(mk_real_int64 240L); (mk_real_int64 200L); (mk_real_int64 240L); (mk_real_int64 400L); (mk_real_int64 200L); (mk_real_int64 200L); (mk_real_int64 500L); (mk_real_int64 400L); (mk_real_int64 240L); (mk_real_int64 240L); (mk_real_int64 330L); (mk_real_int64 365L); (mk_real_int64 400L); (mk_real_int64 40L); (mk_real_int64 400L); (mk_real_int64 125L); (mk_real_int64 400L); (mk_real_int64 540L); (mk_real_int64 200L); (mk_real_int64 200L); ]);\r
  69 ("y1_lo", [8; 9; 10; 15; 19; 20; 26; 30; 31; 36; 40; 48; 56; 60; 61; ], [(mk_real_int64 340L); (mk_real_int64 340L); (mk_real_int64 160L); (mk_real_int64 220L); (mk_real_int64 200L); (mk_real_int64 300L); (mk_real_int64 460L); (mk_real_int64 200L); (mk_real_int64 140L); (mk_real_int64 20L); (mk_real_int64 555L); (mk_real_int64 600L); (mk_real_int64 160L); (mk_real_int64 140L); (mk_real_int64 500L); ]);\r
  70 ("y2_hi", [6; 8; 9; 12; 15; 17; 20; 24; 25; 27; 31; 32; 37; 38; 40; 44; 45; 46; 48; 54; 55; 56; 57; 58; 59; ], [(mk_real_int64 240L); (mk_real_int64 16L); (mk_real_int64 16L); (mk_real_int64 240L); (mk_real_int64 172L); (mk_real_int64 24L); (mk_real_int64 152L); (mk_real_int64 24L); (mk_real_int64 240L); (mk_real_int64 240L); (mk_real_int64 312L); (mk_real_int64 112L); (mk_real_int64 40L); (mk_real_int64 404L); (mk_real_int64 394L); (mk_real_int64 520L); (mk_real_int64 120L); (mk_real_int64 580L); (mk_real_int64 436L); (mk_real_int64 224L); (mk_real_int64 296L); (mk_real_int64 320L); (mk_real_int64 120L); (mk_real_int64 292L); (mk_real_int64 272L); ]);\r
  71 ("y2_lo", [10; 11; 18; 19; 21; 22; 23; 26; 30; 33; 34; 36; 43; 60; 61; ], [(mk_real_int64 160L); (mk_real_int64 448L); (mk_real_int64 368L); (mk_real_int64 392L); (mk_real_int64 368L); (mk_real_int64 48L); (mk_real_int64 192L); (mk_real_int64 68L); (mk_real_int64 92L); (mk_real_int64 612L); (mk_real_int64 56L); (mk_real_int64 364L); (mk_real_int64 520L); (mk_real_int64 140L); (mk_real_int64 368L); ]);\r
  72 ("y3_hi", [6; 8; 9; 12; 15; 17; 20; 24; 25; 27; 31; 32; 37; 38; 40; 44; 45; 46; 48; 54; 55; 56; 57; 58; 59; ], [(mk_real_int64 240L); (mk_real_int64 16L); (mk_real_int64 16L); (mk_real_int64 240L); (mk_real_int64 172L); (mk_real_int64 24L); (mk_real_int64 152L); (mk_real_int64 24L); (mk_real_int64 240L); (mk_real_int64 240L); (mk_real_int64 312L); (mk_real_int64 112L); (mk_real_int64 40L); (mk_real_int64 404L); (mk_real_int64 394L); (mk_real_int64 520L); (mk_real_int64 120L); (mk_real_int64 580L); (mk_real_int64 436L); (mk_real_int64 224L); (mk_real_int64 296L); (mk_real_int64 320L); (mk_real_int64 120L); (mk_real_int64 292L); (mk_real_int64 272L); ]);\r
  73 ("y3_lo", [10; 11; 18; 19; 21; 22; 23; 26; 30; 33; 34; 36; 43; 60; 61; ], [(mk_real_int64 160L); (mk_real_int64 448L); (mk_real_int64 368L); (mk_real_int64 392L); (mk_real_int64 368L); (mk_real_int64 48L); (mk_real_int64 192L); (mk_real_int64 68L); (mk_real_int64 92L); (mk_real_int64 612L); (mk_real_int64 56L); (mk_real_int64 364L); (mk_real_int64 520L); (mk_real_int64 140L); (mk_real_int64 368L); ]);\r
  74 ("y4_lo", [0; 2; 3; 9; 11; 13; 18; 19; 20; 24; 26; 28; 31; 32; 33; 35; 36; 38; 41; 43; 44; 47; ], [(mk_real_int64 250L); (mk_real_int64 140L); (mk_real_int64 140L); (mk_real_int64 655L); (mk_real_int64 210L); (mk_real_int64 70L); (mk_real_int64 210L); (mk_real_int64 250L); (mk_real_int64 405L); (mk_real_int64 195L); (mk_real_int64 580L); (mk_real_int64 10L); (mk_real_int64 250L); (mk_real_int64 35L); (mk_real_int64 270L); (mk_real_int64 300L); (mk_real_int64 75L); (mk_real_int64 639L); (mk_real_int64 56L); (mk_real_int64 300L); (mk_real_int64 305L); (mk_real_int64 43L); ]);\r
  75 ("y4_hi", [4; 5; 6; 12; 14; 15; 16; 17; 21; 25; 27; 30; 40; 42; 45; 46; ], [(mk_real_int64 500L); (mk_real_int64 670L); (mk_real_int64 250L); (mk_real_int64 720L); (mk_real_int64 27L); (mk_real_int64 720L); (mk_real_int64 527L); (mk_real_int64 430L); (mk_real_int64 250L); (mk_real_int64 173L); (mk_real_int64 205L); (mk_real_int64 140L); (mk_real_int64 540L); (mk_real_int64 230L); (mk_real_int64 120L); (mk_real_int64 625L); ]);\r
  76 ("y5_hi", [8; 9; 10; 12; 17; 20; 23; 24; 27; 31; 32; 38; 40; 45; 46; 54; 55; 57; 58; 59; ], [(mk_real_int64 16L); (mk_real_int64 16L); (mk_real_int64 500L); (mk_real_int64 250L); (mk_real_int64 24L); (mk_real_int64 452L); (mk_real_int64 108L); (mk_real_int64 24L); (mk_real_int64 250L); (mk_real_int64 280L); (mk_real_int64 302L); (mk_real_int64 404L); (mk_real_int64 394L); (mk_real_int64 120L); (mk_real_int64 580L); (mk_real_int64 224L); (mk_real_int64 219L); (mk_real_int64 120L); (mk_real_int64 292L); (mk_real_int64 272L); ]);\r
  77 ("y5_lo", [6; 11; 15; 18; 19; 21; 22; 25; 26; 30; 33; 34; 36; 37; 43; 44; 48; 56; 60; 61; ], [(mk_real_int64 250L); (mk_real_int64 448L); (mk_real_int64 318L); (mk_real_int64 368L); (mk_real_int64 392L); (mk_real_int64 368L); (mk_real_int64 48L); (mk_real_int64 250L); (mk_real_int64 68L); (mk_real_int64 92L); (mk_real_int64 302L); (mk_real_int64 56L); (mk_real_int64 460L); (mk_real_int64 435250L); (mk_real_int64 520L); (mk_real_int64 400L); (mk_real_int64 458L); (mk_real_int64 20L); (mk_real_int64 375L); (mk_real_int64 368L); ]);\r
  78 ("y6_hi", [8; 9; 10; 12; 15; 17; 20; 23; 24; 27; 31; 32; 38; 40; 43; 45; 46; 54; 55; 57; 58; 59; ], [(mk_real_int64 16L); (mk_real_int64 16L); (mk_real_int64 500L); (mk_real_int64 250L); (mk_real_int64 682L); (mk_real_int64 24L); (mk_real_int64 452L); (mk_real_int64 108L); (mk_real_int64 24L); (mk_real_int64 250L); (mk_real_int64 280L); (mk_real_int64 302L); (mk_real_int64 404L); (mk_real_int64 394L); (mk_real_int64 480L); (mk_real_int64 120L); (mk_real_int64 580L); (mk_real_int64 224L); (mk_real_int64 219L); (mk_real_int64 120L); (mk_real_int64 292L); (mk_real_int64 272L); ]);\r
  79 ("y6_lo", [1; 6; 9; 11; 12; 13; 15; 18; 19; 21; 22; 25; 26; 30; 33; 34; 36; 37; 43; 44; 47; 48; 54; 56; 59; 60; 61; ], [(mk_real_int64 73000L); (mk_real_int64 165250L); (mk_real_int64 192000L); (mk_real_int64 448L); (mk_real_int64 173000L); (mk_real_int64 73000L); (mk_real_int64 140000L); (mk_real_int64 368L); (mk_real_int64 278392L); (mk_real_int64 418368L); (mk_real_int64 48L); (mk_real_int64 250L); (mk_real_int64 68L); (mk_real_int64 92L); (mk_real_int64 302L); (mk_real_int64 56L); (mk_real_int64 460L); (mk_real_int64 250L); (mk_real_int64 335000L); (mk_real_int64 400L); (mk_real_int64 153000L); (mk_real_int64 458L); (mk_real_int64 131000L); (mk_real_int64 20L); (mk_real_int64 155000L); (mk_real_int64 236375L); (mk_real_int64 368L); ]);\r
  80 ("ye_lo", [2; 9; 19; 22; 25; 29; 31; 54; 55; 58; ], [(mk_real_int64 278000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 140000L); (mk_real_int64 88000L); (mk_real_int64 80000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 383000L); ]);\r
  81 ("ye_hi", [18; 25; 36; 44; 56; ], [(mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 1000L); ]);\r
  82 ("yn_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 13; ], [(mk_real_int64 332L); (mk_real_int64 332L); (mk_real_int64 21L); (mk_real_int64 332L); (mk_real_int64 332L); (mk_real_int64 332L); (mk_real_int64 332L); (mk_real_int64 840L); (mk_real_int64 840L); (mk_real_int64 633L); ]);\r
  83 ("yn_lo", [9; 10; 11; 12; ], [(mk_real_int64 160L); (mk_real_int64 1160L); (mk_real_int64 488L); (mk_real_int64 367L); ]);\r
  84 ];;\r
  85 let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
  86 end;;\r
  87 \r
  88 concl (Test_case.result)\r