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

   1 needs "nobranching_lp.hl";;
   2 \r
   3 module Test_case = struct\r
   4 let hypermap_string = "17272290668 20 4 0 1 2 3 3 0 3 4 3 4 3 5 3 5 3 2 3 5 2 6 3 6 2 7 3 7 2 1 3 7 1 8 3 8 1 9 3 9 1 0 3 9 0 10 3 10 0 4 4 10 4 5 11 3 11 5 6 3 11 6 8 3 6 7 8 3 11 8 12 3 12 8 9 3 12 9 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", [3; 5; 6; 8; 9; ], [(mk_real_int64 59L); (mk_real_int64 59L); (mk_real_int64 128L); (mk_real_int64 205L); (mk_real_int64 128L); ]);\r
  11 ("azim_sum_neg", [0; 4; 7; 12; ], [(mk_real_int64 294L); (mk_real_int64 294L); (mk_real_int64 246L); (mk_real_int64 246L); ]);\r
  12 ("rhazim_sum", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 890L); (mk_real_int64 890L); (mk_real_int64 890L); (mk_real_int64 910L); (mk_real_int64 890L); (mk_real_int64 910L); (mk_real_int64 731L); (mk_real_int64 654L); (mk_real_int64 654L); (mk_real_int64 731L); (mk_real_int64 890L); (mk_real_int64 890L); (mk_real_int64 654L); ]);\r
  13 ("sol_sum3", [2; 10; ], [(mk_real_int64 51L); (mk_real_int64 51L); ]);\r
  14 ("sol_sum3_neg", [3; 6; 7; 9; 12; 14; ], [(mk_real_int64 349L); (mk_real_int64 13L); (mk_real_int64 859L); (mk_real_int64 349L); (mk_real_int64 859L); (mk_real_int64 13L); ]);\r
  15 ("tau_sum3_neg", [0; 1; 2; 3; 4; 5; 6; 8; 9; 10; 11; 13; 14; 15; 16; 17; ], [(mk_real_int64 596L); (mk_real_int64 596L); (mk_real_int64 890L); (mk_real_int64 509L); (mk_real_int64 654L); (mk_real_int64 654L); (mk_real_int64 654L); (mk_real_int64 731L); (mk_real_int64 509L); (mk_real_int64 890L); (mk_real_int64 731L); (mk_real_int64 654L); (mk_real_int64 654L); (mk_real_int64 654L); (mk_real_int64 654L); (mk_real_int64 654L); ]);\r
  16 ("tau_sum4_neg", [0; 1; ], [(mk_real_int64 890L); (mk_real_int64 890L); ]);\r
  17 ("ln_def_neg", [3; 5; ], [(mk_real_int64 3L); (mk_real_int64 3L); ]);\r
  18 ("ln_def", [0; 1; 2; 4; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 18L); (mk_real_int64 18L); (mk_real_int64 18L); (mk_real_int64 18L); (mk_real_int64 194L); (mk_real_int64 279L); (mk_real_int64 279L); (mk_real_int64 194L); (mk_real_int64 18L); (mk_real_int64 18L); (mk_real_int64 279L); ]);\r
  19 ("rho_def", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 5594L); (mk_real_int64 5594L); (mk_real_int64 5594L); (mk_real_int64 5717L); (mk_real_int64 5594L); (mk_real_int64 5717L); (mk_real_int64 4592L); (mk_real_int64 4109L); (mk_real_int64 4109L); (mk_real_int64 4592L); (mk_real_int64 5594L); (mk_real_int64 5594L); (mk_real_int64 4109L); ]);\r
  20 ("edge_sym_neg", [1; 14; 15; 17; 18; 24; 26; 27; 30; 32; 33; 40; 45; 46; 51; 52; 58; ], [(mk_real_int64 191L); (mk_real_int64 202L); (mk_real_int64 85L); (mk_real_int64 26L); (mk_real_int64 59L); (mk_real_int64 46L); (mk_real_int64 47L); (mk_real_int64 190L); (mk_real_int64 120L); (mk_real_int64 85L); (mk_real_int64 202L); (mk_real_int64 191L); (mk_real_int64 190L); (mk_real_int64 200L); (mk_real_int64 46L); (mk_real_int64 39L); (mk_real_int64 26L); ]);\r
  21 ("edge_sym", [12; 21; 23; 43; 55; ], [(mk_real_int64 85L); (mk_real_int64 26L); (mk_real_int64 157L); (mk_real_int64 47L); (mk_real_int64 59L); ]);\r
  22 ("y1_def", [11; 15; 18; 19; 22; 24; 25; 33; 36; 46; 48; 52; 53; 56; 61; ], [(mk_real_int64 35L); (mk_real_int64 133L); (mk_real_int64 123L); (mk_real_int64 89L); (mk_real_int64 129L); (mk_real_int64 5L); (mk_real_int64 326L); (mk_real_int64 133L); (mk_real_int64 39L); (mk_real_int64 326L); (mk_real_int64 123L); (mk_real_int64 134L); (mk_real_int64 123L); (mk_real_int64 123L); (mk_real_int64 89L); ]);\r
  23 ("y1_def_neg", [13; 17; 21; 23; 26; 28; 29; 32; 35; 41; 42; 43; 44; 50; 58; 60; ], [(mk_real_int64 149L); (mk_real_int64 19L); (mk_real_int64 88L); (mk_real_int64 4L); (mk_real_int64 19L); (mk_real_int64 50L); (mk_real_int64 96L); (mk_real_int64 149L); (mk_real_int64 3L); (mk_real_int64 96L); (mk_real_int64 39L); (mk_real_int64 11L); (mk_real_int64 19L); (mk_real_int64 4L); (mk_real_int64 19L); (mk_real_int64 88L); ]);\r
  24 ("y2_def_neg", [11; 13; 18; 19; 22; 28; 32; 35; 36; 42; 48; 52; 53; 56; 61; ], [(mk_real_int64 25L); (mk_real_int64 42L); (mk_real_int64 37L); (mk_real_int64 27L); (mk_real_int64 39L); (mk_real_int64 23L); (mk_real_int64 42L); (mk_real_int64 3L); (mk_real_int64 22L); (mk_real_int64 39L); (mk_real_int64 37L); (mk_real_int64 34L); (mk_real_int64 37L); (mk_real_int64 37L); (mk_real_int64 27L); ]);\r
  25 ("y2_def", [15; 17; 21; 23; 24; 25; 26; 29; 33; 41; 43; 44; 46; 50; 58; 60; ], [(mk_real_int64 133L); (mk_real_int64 12L); (mk_real_int64 53L); (mk_real_int64 2L); (mk_real_int64 5L); (mk_real_int64 326L); (mk_real_int64 12L); (mk_real_int64 58L); (mk_real_int64 133L); (mk_real_int64 58L); (mk_real_int64 16L); (mk_real_int64 12L); (mk_real_int64 326L); (mk_real_int64 2L); (mk_real_int64 12L); (mk_real_int64 53L); ]);\r
  26 ("y3_def_neg", [11; 13; 18; 19; 22; 28; 32; 35; 36; 42; 48; 52; 53; 56; 61; ], [(mk_real_int64 25L); (mk_real_int64 42L); (mk_real_int64 37L); (mk_real_int64 27L); (mk_real_int64 39L); (mk_real_int64 23L); (mk_real_int64 42L); (mk_real_int64 3L); (mk_real_int64 22L); (mk_real_int64 39L); (mk_real_int64 37L); (mk_real_int64 34L); (mk_real_int64 37L); (mk_real_int64 37L); (mk_real_int64 27L); ]);\r
  27 ("y3_def", [15; 17; 21; 23; 24; 25; 26; 29; 33; 41; 43; 44; 46; 50; 58; 60; ], [(mk_real_int64 133L); (mk_real_int64 12L); (mk_real_int64 53L); (mk_real_int64 2L); (mk_real_int64 5L); (mk_real_int64 326L); (mk_real_int64 12L); (mk_real_int64 58L); (mk_real_int64 133L); (mk_real_int64 58L); (mk_real_int64 16L); (mk_real_int64 12L); (mk_real_int64 326L); (mk_real_int64 2L); (mk_real_int64 12L); (mk_real_int64 53L); ]);\r
  28 ("y4_def", [7; 14; 15; 18; 32; 40; 44; 45; 48; 53; ], [(mk_real_int64 85L); (mk_real_int64 190L); (mk_real_int64 138L); (mk_real_int64 200L); (mk_real_int64 88L); (mk_real_int64 190L); (mk_real_int64 197L); (mk_real_int64 190L); (mk_real_int64 190L); (mk_real_int64 138L); ]);\r
  29 ("y4_def_neg", [9; 11; 13; 17; 19; 20; 21; 22; 24; 25; 28; 29; 31; 33; 34; 35; 36; 38; 42; 50; 52; ], [(mk_real_int64 133L); (mk_real_int64 68L); (mk_real_int64 22L); (mk_real_int64 100L); (mk_real_int64 4L); (mk_real_int64 2L); (mk_real_int64 168L); (mk_real_int64 22L); (mk_real_int64 58L); (mk_real_int64 109L); (mk_real_int64 133L); (mk_real_int64 68L); (mk_real_int64 2L); (mk_real_int64 109L); (mk_real_int64 27L); (mk_real_int64 31L); (mk_real_int64 22L); (mk_real_int64 168L); (mk_real_int64 4L); (mk_real_int64 22L); (mk_real_int64 100L); ]);\r
  30 ("y5_def_neg", [13; 15; 18; 19; 22; 24; 25; 28; 32; 33; 35; 37; 42; 46; 48; 52; 53; 56; 61; ], [(mk_real_int64 17L); (mk_real_int64 68L); (mk_real_int64 37L); (mk_real_int64 27L); (mk_real_int64 39L); (mk_real_int64 2L); (mk_real_int64 168L); (mk_real_int64 11L); (mk_real_int64 17L); (mk_real_int64 68L); (mk_real_int64 2L); (mk_real_int64 191L); (mk_real_int64 27L); (mk_real_int64 168L); (mk_real_int64 37L); (mk_real_int64 42L); (mk_real_int64 37L); (mk_real_int64 37L); (mk_real_int64 27L); ]);\r
  31 ("y5_def", [17; 21; 23; 26; 29; 36; 41; 43; 44; 50; 58; 60; ], [(mk_real_int64 12L); (mk_real_int64 53L); (mk_real_int64 2L); (mk_real_int64 12L); (mk_real_int64 58L); (mk_real_int64 2L); (mk_real_int64 58L); (mk_real_int64 16L); (mk_real_int64 12L); (mk_real_int64 2L); (mk_real_int64 12L); (mk_real_int64 53L); ]);\r
  32 ("y6_def_neg", [13; 15; 18; 22; 24; 25; 28; 32; 33; 35; 46; 52; 56; ], [(mk_real_int64 17L); (mk_real_int64 68L); (mk_real_int64 37L); (mk_real_int64 26L); (mk_real_int64 2L); (mk_real_int64 168L); (mk_real_int64 11L); (mk_real_int64 17L); (mk_real_int64 68L); (mk_real_int64 2L); (mk_real_int64 168L); (mk_real_int64 42L); (mk_real_int64 37L); ]);\r
  33 ("y6_def", [17; 19; 21; 23; 26; 29; 31; 36; 41; 42; 43; 44; 48; 50; 53; 58; 60; 61; ], [(mk_real_int64 12L); (mk_real_int64 126L); (mk_real_int64 53L); (mk_real_int64 2L); (mk_real_int64 121L); (mk_real_int64 58L); (mk_real_int64 206L); (mk_real_int64 2L); (mk_real_int64 58L); (mk_real_int64 178L); (mk_real_int64 16L); (mk_real_int64 121L); (mk_real_int64 46L); (mk_real_int64 2L); (mk_real_int64 46L); (mk_real_int64 12L); (mk_real_int64 67L); (mk_real_int64 126L); ]);\r
  34 ("y8_def_neg", [5; ], [(mk_real_int64 191L); ]);\r
  35 ("RHA", [0; 4; 5; 6; 7; 8; 9; 10; 13; 14; 15; 16; 17; 20; 21; 23; 25; 26; 27; 30; 31; 32; 33; 35; 39; 42; 44; 45; 46; 47; 50; 55; 57; 58; 59; 60; ], [(mk_real_int64 19L); (mk_real_int64 314L); (mk_real_int64 294L); (mk_real_int64 294L); (mk_real_int64 294L); (mk_real_int64 294L); (mk_real_int64 314L); (mk_real_int64 19L); (mk_real_int64 290L); (mk_real_int64 381L); (mk_real_int64 221L); (mk_real_int64 77L); (mk_real_int64 205L); (mk_real_int64 236L); (mk_real_int64 90L); (mk_real_int64 230L); (mk_real_int64 654L); (mk_real_int64 859L); (mk_real_int64 731L); (mk_real_int64 179L); (mk_real_int64 221L); (mk_real_int64 290L); (mk_real_int64 381L); (mk_real_int64 19L); (mk_real_int64 19L); (mk_real_int64 179L); (mk_real_int64 859L); (mk_real_int64 731L); (mk_real_int64 654L); (mk_real_int64 77L); (mk_real_int64 230L); (mk_real_int64 77L); (mk_real_int64 77L); (mk_real_int64 205L); (mk_real_int64 236L); (mk_real_int64 90L); ]);\r
  36 ("yy10", [1; 23; 46; ], [(mk_real_int64 191L); (mk_real_int64 43L); (mk_real_int64 43L); ]);\r
  37 ("tau4", [0; 1; ], [(mk_real_int64 137L); (mk_real_int64 137L); ]);\r
  38 ("ineq106", [9; 13; 17; 19; 22; 25; 28; 33; 36; 42; 50; 52; ], [(mk_real_int64 111L); (mk_real_int64 32L); (mk_real_int64 147L); (mk_real_int64 6L); (mk_real_int64 32L); (mk_real_int64 160L); (mk_real_int64 111L); (mk_real_int64 160L); (mk_real_int64 32L); (mk_real_int64 6L); (mk_real_int64 32L); (mk_real_int64 147L); ]);\r
  39 ("ineq107", [7; 14; 15; 18; 32; 40; 44; 45; 48; 53; ], [(mk_real_int64 92L); (mk_real_int64 246L); (mk_real_int64 179L); (mk_real_int64 259L); (mk_real_int64 92L); (mk_real_int64 246L); (mk_real_int64 259L); (mk_real_int64 246L); (mk_real_int64 246L); (mk_real_int64 179L); ]);\r
  40 ("ineq108", [24; 35; ], [(mk_real_int64 45L); (mk_real_int64 45L); ]);\r
  41 ("ineq109", [7; 32; ], [(mk_real_int64 51L); (mk_real_int64 51L); ]);\r
  42 ("ineq110", [11; 20; 21; 29; 38; 44; ], [(mk_real_int64 349L); (mk_real_int64 13L); (mk_real_int64 859L); (mk_real_int64 349L); (mk_real_int64 859L); (mk_real_int64 13L); ]);\r
  43 ("ineq111", [7; 9; 24; 28; 31; 34; ], [(mk_real_int64 19L); (mk_real_int64 459L); (mk_real_int64 218L); (mk_real_int64 459L); (mk_real_int64 19L); (mk_real_int64 218L); ]);\r
  44 ("ineq112", [15; 53; ], [(mk_real_int64 133L); (mk_real_int64 133L); ]);\r
  45 ("ineq113", [7; 32; ], [(mk_real_int64 584L); (mk_real_int64 584L); ]);\r
  46 ("ineq114", [0; 5; 6; 8; 10; 12; 13; 16; 17; 19; 20; 24; 26; 29; 30; 31; 34; 35; 39; 41; 42; 43; 46; 47; 49; 50; 51; 52; ], [(mk_real_int64 596L); (mk_real_int64 596L); (mk_real_int64 207L); (mk_real_int64 81L); (mk_real_int64 51L); (mk_real_int64 327L); (mk_real_int64 327L); (mk_real_int64 378L); (mk_real_int64 143L); (mk_real_int64 347L); (mk_real_int64 307L); (mk_real_int64 132L); (mk_real_int64 381L); (mk_real_int64 51L); (mk_real_int64 81L); (mk_real_int64 207L); (mk_real_int64 381L); (mk_real_int64 132L); (mk_real_int64 327L); (mk_real_int64 327L); (mk_real_int64 347L); (mk_real_int64 307L); (mk_real_int64 327L); (mk_real_int64 327L); (mk_real_int64 327L); (mk_real_int64 327L); (mk_real_int64 378L); (mk_real_int64 143L); ]);\r
  47 ("ineq119", [3; 5; ], [(mk_real_int64 650L); (mk_real_int64 650L); ]);\r
  48 ("ineq120", [0; 6; ], [(mk_real_int64 104L); (mk_real_int64 104L); ]);\r
  49 ];;\r
  50 \r
  51 (***************)\r
  52 (* Variables   *)\r
  53 (***************)\r
  54 let target_variables = [\r
  55 ("ln_hi", [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ], [(mk_real_int64 3050L); (mk_real_int64 3050L); (mk_real_int64 3050L); (mk_real_int64 2525L); (mk_real_int64 3050L); (mk_real_int64 2525L); (mk_real_int64 2400L); (mk_real_int64 1925L); (mk_real_int64 1925L); (mk_real_int64 2400L); (mk_real_int64 3050L); (mk_real_int64 3050L); (mk_real_int64 1925L); ]);\r
  56 ];;\r
  57 \r
  58 (*************************)\r
  59 \r
  60 let variable_bounds = [\r
  61 ("azim_hi", [0; 4; 9; 10; 20; 23; 24; 30; 35; 39; 42; 50; 51; 59; ], [(mk_real_int64 832L); (mk_real_int64 96L); (mk_real_int64 96L); (mk_real_int64 582L); (mk_real_int64 628L); (mk_real_int64 222L); (mk_real_int64 182L); (mk_real_int64 506L); (mk_real_int64 582L); (mk_real_int64 832L); (mk_real_int64 506L); (mk_real_int64 222L); (mk_real_int64 182L); (mk_real_int64 628L); ]);\r
  62 ("azim_lo", [3; 11; 12; 14; 16; 17; 19; 21; 28; 33; 34; 36; 38; 43; 47; 49; 54; 55; 57; 58; 60; 61; ], [(mk_real_int64 450L); (mk_real_int64 256L); (mk_real_int64 294L); (mk_real_int64 74L); (mk_real_int64 298L); (mk_real_int64 298L); (mk_real_int64 431L); (mk_real_int64 482L); (mk_real_int64 368L); (mk_real_int64 74L); (mk_real_int64 294L); (mk_real_int64 256L); (mk_real_int64 450L); (mk_real_int64 368L); (mk_real_int64 298L); (mk_real_int64 298L); (mk_real_int64 298L); (mk_real_int64 298L); (mk_real_int64 298L); (mk_real_int64 298L); (mk_real_int64 482L); (mk_real_int64 431L); ]);\r
  63 ("rhazim_lo", [0; 10; 15; 31; 35; 39; ], [(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
  64 ("rhazim_hi", [17; 21; 26; 29; 41; 44; 58; 60; ], [(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
  65 ("rho_hi", [3; 5; 6; 7; 8; 9; 12; ], [(mk_real_int64 1440L); (mk_real_int64 1440L); (mk_real_int64 1604L); (mk_real_int64 736L); (mk_real_int64 736L); (mk_real_int64 1604L); (mk_real_int64 736L); ]);\r
  66 ("rho_lo", [0; 1; 2; 4; 10; 11; ], [(mk_real_int64 1240L); (mk_real_int64 1240L); (mk_real_int64 1240L); (mk_real_int64 1240L); (mk_real_int64 1240L); (mk_real_int64 1240L); ]);\r
  67 ("tau_hi", [0; 3; 4; 10; 11; 12; ], [(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
  68 ("y1_lo", [11; 13; 15; 17; 21; 24; 26; 32; 33; 35; 36; 42; 44; 58; 60; ], [(mk_real_int64 121L); (mk_real_int64 220L); (mk_real_int64 380L); (mk_real_int64 200L); (mk_real_int64 200L); (mk_real_int64 60L); (mk_real_int64 200L); (mk_real_int64 220L); (mk_real_int64 380L); (mk_real_int64 420L); (mk_real_int64 701L); (mk_real_int64 240L); (mk_real_int64 200L); (mk_real_int64 200L); (mk_real_int64 200L); ]);\r
  69 ("y1_hi", [19; 22; 23; 25; 28; 43; 46; 50; 52; 61; ], [(mk_real_int64 500L); (mk_real_int64 500L); (mk_real_int64 400L); (mk_real_int64 420L); (mk_real_int64 185L); (mk_real_int64 425L); (mk_real_int64 420L); (mk_real_int64 400L); (mk_real_int64 440L); (mk_real_int64 500L); ]);\r
  70 ("y2_lo", [11; 13; 15; 17; 18; 19; 22; 24; 26; 32; 33; 35; 42; 44; 48; 52; 53; 56; 58; 61; ], [(mk_real_int64 105L); (mk_real_int64 216L); (mk_real_int64 380L); (mk_real_int64 352L); (mk_real_int64 392L); (mk_real_int64 208L); (mk_real_int64 368L); (mk_real_int64 60L); (mk_real_int64 352L); (mk_real_int64 216L); (mk_real_int64 380L); (mk_real_int64 420L); (mk_real_int64 240L); (mk_real_int64 352L); (mk_real_int64 392L); (mk_real_int64 428L); (mk_real_int64 392L); (mk_real_int64 392L); (mk_real_int64 352L); (mk_real_int64 208L); ]);\r
  71 ("y2_hi", [21; 23; 25; 28; 29; 36; 41; 43; 46; 50; 60; ], [(mk_real_int64 508L); (mk_real_int64 184L); (mk_real_int64 420L); (mk_real_int64 140L); (mk_real_int64 240L); (mk_real_int64 315L); (mk_real_int64 240L); (mk_real_int64 380L); (mk_real_int64 420L); (mk_real_int64 184L); (mk_real_int64 508L); ]);\r
  72 ("y3_lo", [11; 13; 15; 17; 18; 19; 22; 24; 26; 32; 33; 35; 42; 44; 48; 52; 53; 56; 58; 61; ], [(mk_real_int64 105L); (mk_real_int64 216L); (mk_real_int64 380L); (mk_real_int64 352L); (mk_real_int64 392L); (mk_real_int64 208L); (mk_real_int64 368L); (mk_real_int64 60L); (mk_real_int64 352L); (mk_real_int64 216L); (mk_real_int64 380L); (mk_real_int64 420L); (mk_real_int64 240L); (mk_real_int64 352L); (mk_real_int64 392L); (mk_real_int64 428L); (mk_real_int64 392L); (mk_real_int64 392L); (mk_real_int64 352L); (mk_real_int64 208L); ]);\r
  73 ("y3_hi", [21; 23; 25; 28; 29; 36; 41; 43; 46; 50; 60; ], [(mk_real_int64 508L); (mk_real_int64 184L); (mk_real_int64 420L); (mk_real_int64 140L); (mk_real_int64 240L); (mk_real_int64 315L); (mk_real_int64 240L); (mk_real_int64 380L); (mk_real_int64 420L); (mk_real_int64 184L); (mk_real_int64 508L); ]);\r
  74 ("y4_lo", [9; 11; 17; 19; 20; 21; 24; 25; 28; 29; 31; 32; 33; 34; 38; 42; 52; ], [(mk_real_int64 410L); (mk_real_int64 404L); (mk_real_int64 695L); (mk_real_int64 110L); (mk_real_int64 548L); (mk_real_int64 364L); (mk_real_int64 75L); (mk_real_int64 600L); (mk_real_int64 410L); (mk_real_int64 404L); (mk_real_int64 375L); (mk_real_int64 360L); (mk_real_int64 600L); (mk_real_int64 250L); (mk_real_int64 364L); (mk_real_int64 110L); (mk_real_int64 695L); ]);\r
  75 ("y4_hi", [7; 13; 14; 15; 18; 22; 35; 36; 40; 44; 45; 48; 50; 53; ], [(mk_real_int64 265L); (mk_real_int64 80L); (mk_real_int64 158L); (mk_real_int64 367L); (mk_real_int64 207L); (mk_real_int64 80L); (mk_real_int64 175L); (mk_real_int64 80L); (mk_real_int64 158L); (mk_real_int64 659L); (mk_real_int64 158L); (mk_real_int64 158L); (mk_real_int64 80L); (mk_real_int64 367L); ]);\r
  76 ("y5_hi", [11; 13; 21; 23; 28; 29; 32; 36; 41; 43; 50; 52; 60; ], [(mk_real_int64 165L); (mk_real_int64 29L); (mk_real_int64 508L); (mk_real_int64 184L); (mk_real_int64 130L); (mk_real_int64 240L); (mk_real_int64 29L); (mk_real_int64 540L); (mk_real_int64 240L); (mk_real_int64 380L); (mk_real_int64 184L); (mk_real_int64 84L); (mk_real_int64 508L); ]);\r
  77 ("y5_lo", [15; 17; 18; 19; 22; 24; 25; 26; 33; 35; 42; 44; 46; 48; 53; 56; 58; 61; ], [(mk_real_int64 404L); (mk_real_int64 352L); (mk_real_int64 392L); (mk_real_int64 208L); (mk_real_int64 368L); (mk_real_int64 548L); (mk_real_int64 364L); (mk_real_int64 352L); (mk_real_int64 404L); (mk_real_int64 375L); (mk_real_int64 250L); (mk_real_int64 352L); (mk_real_int64 364L); (mk_real_int64 392L); (mk_real_int64 392L); (mk_real_int64 392L); (mk_real_int64 352L); (mk_real_int64 208L); ]);\r
  78 ("y6_hi", [11; 13; 21; 23; 26; 28; 29; 32; 36; 41; 42; 43; 44; 48; 50; 52; 53; ], [(mk_real_int64 165L); (mk_real_int64 29L); (mk_real_int64 508L); (mk_real_int64 184L); (mk_real_int64 648L); (mk_real_int64 130L); (mk_real_int64 240L); (mk_real_int64 29L); (mk_real_int64 540L); (mk_real_int64 240L); (mk_real_int64 750L); (mk_real_int64 380L); (mk_real_int64 648L); (mk_real_int64 608L); (mk_real_int64 184L); (mk_real_int64 84L); (mk_real_int64 608L); ]);\r
  79 ("y6_lo", [15; 17; 18; 19; 22; 24; 25; 26; 31; 33; 35; 42; 44; 46; 48; 53; 56; 58; 60; 61; ], [(mk_real_int64 404L); (mk_real_int64 352L); (mk_real_int64 392L); (mk_real_int64 153208L); (mk_real_int64 13368L); (mk_real_int64 548L); (mk_real_int64 364L); (mk_real_int64 110000L); (mk_real_int64 206000L); (mk_real_int64 404L); (mk_real_int64 375L); (mk_real_int64 206000L); (mk_real_int64 110000L); (mk_real_int64 364L); (mk_real_int64 84000L); (mk_real_int64 84000L); (mk_real_int64 392L); (mk_real_int64 352L); (mk_real_int64 13492L); (mk_real_int64 153208L); ]);\r
  80 ("y8_hi", [5; ], [(mk_real_int64 191000L); ]);\r
  81 ("ye_hi", [14; 17; 24; 25; 31; 33; 34; 46; 47; 55; 58; 60; ], [(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); ]);\r
  82 ("ye_lo", [47; 50; 52; 55; ], [(mk_real_int64 97000L); (mk_real_int64 1000L); (mk_real_int64 1000L); (mk_real_int64 97000L); ]);\r
  83 ("yn_lo", [3; 5; 7; 12; ], [(mk_real_int64 228L); (mk_real_int64 228L); (mk_real_int64 517L); (mk_real_int64 517L); ]);\r
  84 ("yn_hi", [0; 1; 2; 4; 6; 8; 9; 10; 11; ], [(mk_real_int64 386L); (mk_real_int64 1386L); (mk_real_int64 386L); (mk_real_int64 1386L); (mk_real_int64 1938L); (mk_real_int64 1483L); (mk_real_int64 1938L); (mk_real_int64 1386L); (mk_real_int64 386L); ]);\r
  85 ];;\r
  86 let result = prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;\r
  87 end;;\r
  88 \r
  89 concl (Test_case.result)\r