//#rIgnore
// Auto-generated by simple-scaled.py
// A scaled version of Bangalore.bpl with n different ranking functions
// size = 100

procedure main() returns (x0: int, x1: int, x2: int, x3: int, x4: int, x5: int, x6: int, x7: int, x8: int, x9: int, x10: int, x11: int, x12: int, x13: int, x14: int, x15: int, x16: int, x17: int, x18: int, x19: int, x20: int, x21: int, x22: int, x23: int, x24: int, x25: int, x26: int, x27: int, x28: int, x29: int, x30: int, x31: int, x32: int, x33: int, x34: int, x35: int, x36: int, x37: int, x38: int, x39: int, x40: int, x41: int, x42: int, x43: int, x44: int, x45: int, x46: int, x47: int, x48: int, x49: int, x50: int, x51: int, x52: int, x53: int, x54: int, x55: int, x56: int, x57: int, x58: int, x59: int, x60: int, x61: int, x62: int, x63: int, x64: int, x65: int, x66: int, x67: int, x68: int, x69: int, x70: int, x71: int, x72: int, x73: int, x74: int, x75: int, x76: int, x77: int, x78: int, x79: int, x80: int, x81: int, x82: int, x83: int, x84: int, x85: int, x86: int, x87: int, x88: int, x89: int, x90: int, x91: int, x92: int, x93: int, x94: int, x95: int, x96: int, x97: int, x98: int, x99: int)
{
  var y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15, y16, y17, y18, y19, y20, y21, y22, y23, y24, y25, y26, y27, y28, y29, y30, y31, y32, y33, y34, y35, y36, y37, y38, y39, y40, y41, y42, y43, y44, y45, y46, y47, y48, y49, y50, y51, y52, y53, y54, y55, y56, y57, y58, y59, y60, y61, y62, y63, y64, y65, y66, y67, y68, y69, y70, y71, y72, y73, y74, y75, y76, y77, y78, y79, y80, y81, y82, y83, y84, y85, y86, y87, y88, y89, y90, y91, y92, y93, y94, y95, y96, y97, y98, y99: int;
  y0 := 1;
  y1 := 1;
  y2 := 1;
  y3 := 1;
  y4 := 1;
  y5 := 1;
  y6 := 1;
  y7 := 1;
  y8 := 1;
  y9 := 1;
  y10 := 1;
  y11 := 1;
  y12 := 1;
  y13 := 1;
  y14 := 1;
  y15 := 1;
  y16 := 1;
  y17 := 1;
  y18 := 1;
  y19 := 1;
  y20 := 1;
  y21 := 1;
  y22 := 1;
  y23 := 1;
  y24 := 1;
  y25 := 1;
  y26 := 1;
  y27 := 1;
  y28 := 1;
  y29 := 1;
  y30 := 1;
  y31 := 1;
  y32 := 1;
  y33 := 1;
  y34 := 1;
  y35 := 1;
  y36 := 1;
  y37 := 1;
  y38 := 1;
  y39 := 1;
  y40 := 1;
  y41 := 1;
  y42 := 1;
  y43 := 1;
  y44 := 1;
  y45 := 1;
  y46 := 1;
  y47 := 1;
  y48 := 1;
  y49 := 1;
  y50 := 1;
  y51 := 1;
  y52 := 1;
  y53 := 1;
  y54 := 1;
  y55 := 1;
  y56 := 1;
  y57 := 1;
  y58 := 1;
  y59 := 1;
  y60 := 1;
  y61 := 1;
  y62 := 1;
  y63 := 1;
  y64 := 1;
  y65 := 1;
  y66 := 1;
  y67 := 1;
  y68 := 1;
  y69 := 1;
  y70 := 1;
  y71 := 1;
  y72 := 1;
  y73 := 1;
  y74 := 1;
  y75 := 1;
  y76 := 1;
  y77 := 1;
  y78 := 1;
  y79 := 1;
  y80 := 1;
  y81 := 1;
  y82 := 1;
  y83 := 1;
  y84 := 1;
  y85 := 1;
  y86 := 1;
  y87 := 1;
  y88 := 1;
  y89 := 1;
  y90 := 1;
  y91 := 1;
  y92 := 1;
  y93 := 1;
  y94 := 1;
  y95 := 1;
  y96 := 1;
  y97 := 1;
  y98 := 1;
  y99 := 1;
  while (x0 >= 0 && x1 >= 0 && x2 >= 0 && x3 >= 0 && x4 >= 0 && x5 >= 0 && x6 >= 0 && x7 >= 0 && x8 >= 0 && x9 >= 0 && x10 >= 0 && x11 >= 0 && x12 >= 0 && x13 >= 0 && x14 >= 0 && x15 >= 0 && x16 >= 0 && x17 >= 0 && x18 >= 0 && x19 >= 0 && x20 >= 0 && x21 >= 0 && x22 >= 0 && x23 >= 0 && x24 >= 0 && x25 >= 0 && x26 >= 0 && x27 >= 0 && x28 >= 0 && x29 >= 0 && x30 >= 0 && x31 >= 0 && x32 >= 0 && x33 >= 0 && x34 >= 0 && x35 >= 0 && x36 >= 0 && x37 >= 0 && x38 >= 0 && x39 >= 0 && x40 >= 0 && x41 >= 0 && x42 >= 0 && x43 >= 0 && x44 >= 0 && x45 >= 0 && x46 >= 0 && x47 >= 0 && x48 >= 0 && x49 >= 0 && x50 >= 0 && x51 >= 0 && x52 >= 0 && x53 >= 0 && x54 >= 0 && x55 >= 0 && x56 >= 0 && x57 >= 0 && x58 >= 0 && x59 >= 0 && x60 >= 0 && x61 >= 0 && x62 >= 0 && x63 >= 0 && x64 >= 0 && x65 >= 0 && x66 >= 0 && x67 >= 0 && x68 >= 0 && x69 >= 0 && x70 >= 0 && x71 >= 0 && x72 >= 0 && x73 >= 0 && x74 >= 0 && x75 >= 0 && x76 >= 0 && x77 >= 0 && x78 >= 0 && x79 >= 0 && x80 >= 0 && x81 >= 0 && x82 >= 0 && x83 >= 0 && x84 >= 0 && x85 >= 0 && x86 >= 0 && x87 >= 0 && x88 >= 0 && x89 >= 0 && x90 >= 0 && x91 >= 0 && x92 >= 0 && x93 >= 0 && x94 >= 0 && x95 >= 0 && x96 >= 0 && x97 >= 0 && x98 >= 0 && x99 >= 0) {
    x0 := x0 - y0;
    x1 := x1 - y1;
    x2 := x2 - y2;
    x3 := x3 - y3;
    x4 := x4 - y4;
    x5 := x5 - y5;
    x6 := x6 - y6;
    x7 := x7 - y7;
    x8 := x8 - y8;
    x9 := x9 - y9;
    x10 := x10 - y10;
    x11 := x11 - y11;
    x12 := x12 - y12;
    x13 := x13 - y13;
    x14 := x14 - y14;
    x15 := x15 - y15;
    x16 := x16 - y16;
    x17 := x17 - y17;
    x18 := x18 - y18;
    x19 := x19 - y19;
    x20 := x20 - y20;
    x21 := x21 - y21;
    x22 := x22 - y22;
    x23 := x23 - y23;
    x24 := x24 - y24;
    x25 := x25 - y25;
    x26 := x26 - y26;
    x27 := x27 - y27;
    x28 := x28 - y28;
    x29 := x29 - y29;
    x30 := x30 - y30;
    x31 := x31 - y31;
    x32 := x32 - y32;
    x33 := x33 - y33;
    x34 := x34 - y34;
    x35 := x35 - y35;
    x36 := x36 - y36;
    x37 := x37 - y37;
    x38 := x38 - y38;
    x39 := x39 - y39;
    x40 := x40 - y40;
    x41 := x41 - y41;
    x42 := x42 - y42;
    x43 := x43 - y43;
    x44 := x44 - y44;
    x45 := x45 - y45;
    x46 := x46 - y46;
    x47 := x47 - y47;
    x48 := x48 - y48;
    x49 := x49 - y49;
    x50 := x50 - y50;
    x51 := x51 - y51;
    x52 := x52 - y52;
    x53 := x53 - y53;
    x54 := x54 - y54;
    x55 := x55 - y55;
    x56 := x56 - y56;
    x57 := x57 - y57;
    x58 := x58 - y58;
    x59 := x59 - y59;
    x60 := x60 - y60;
    x61 := x61 - y61;
    x62 := x62 - y62;
    x63 := x63 - y63;
    x64 := x64 - y64;
    x65 := x65 - y65;
    x66 := x66 - y66;
    x67 := x67 - y67;
    x68 := x68 - y68;
    x69 := x69 - y69;
    x70 := x70 - y70;
    x71 := x71 - y71;
    x72 := x72 - y72;
    x73 := x73 - y73;
    x74 := x74 - y74;
    x75 := x75 - y75;
    x76 := x76 - y76;
    x77 := x77 - y77;
    x78 := x78 - y78;
    x79 := x79 - y79;
    x80 := x80 - y80;
    x81 := x81 - y81;
    x82 := x82 - y82;
    x83 := x83 - y83;
    x84 := x84 - y84;
    x85 := x85 - y85;
    x86 := x86 - y86;
    x87 := x87 - y87;
    x88 := x88 - y88;
    x89 := x89 - y89;
    x90 := x90 - y90;
    x91 := x91 - y91;
    x92 := x92 - y92;
    x93 := x93 - y93;
    x94 := x94 - y94;
    x95 := x95 - y95;
    x96 := x96 - y96;
    x97 := x97 - y97;
    x98 := x98 - y98;
    x99 := x99 - y99;
  }
}