//#rIgnore
// Auto-generated by bound-scaled.py
// size = 200

procedure main() returns (y: int)
{
  var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64, x65, x66, x67, x68, x69, x70, x71, x72, x73, x74, x75, x76, x77, x78, x79, x80, x81, x82, x83, x84, x85, x86, x87, x88, x89, x90, x91, x92, x93, x94, x95, x96, x97, x98, x99, x100, x101, x102, x103, x104, x105, x106, x107, x108, x109, x110, x111, x112, x113, x114, x115, x116, x117, x118, x119, x120, x121, x122, x123, x124, x125, x126, x127, x128, x129, x130, x131, x132, x133, x134, x135, x136, x137, x138, x139, x140, x141, x142, x143, x144, x145, x146, x147, x148, x149, x150, x151, x152, x153, x154, x155, x156, x157, x158, x159, x160, x161, x162, x163, x164, x165, x166, x167, x168, x169, x170, x171, x172, x173, x174, x175, x176, x177, x178, x179, x180, x181, x182, x183, x184, x185, x186, x187, x188, x189, x190, x191, x192, x193, x194, x195, x196, x197, x198, x199: int;
  x0 := 1;
  x1 := 1;
  x2 := 1;
  x3 := 1;
  x4 := 1;
  x5 := 1;
  x6 := 1;
  x7 := 1;
  x8 := 1;
  x9 := 1;
  x10 := 1;
  x11 := 1;
  x12 := 1;
  x13 := 1;
  x14 := 1;
  x15 := 1;
  x16 := 1;
  x17 := 1;
  x18 := 1;
  x19 := 1;
  x20 := 1;
  x21 := 1;
  x22 := 1;
  x23 := 1;
  x24 := 1;
  x25 := 1;
  x26 := 1;
  x27 := 1;
  x28 := 1;
  x29 := 1;
  x30 := 1;
  x31 := 1;
  x32 := 1;
  x33 := 1;
  x34 := 1;
  x35 := 1;
  x36 := 1;
  x37 := 1;
  x38 := 1;
  x39 := 1;
  x40 := 1;
  x41 := 1;
  x42 := 1;
  x43 := 1;
  x44 := 1;
  x45 := 1;
  x46 := 1;
  x47 := 1;
  x48 := 1;
  x49 := 1;
  x50 := 1;
  x51 := 1;
  x52 := 1;
  x53 := 1;
  x54 := 1;
  x55 := 1;
  x56 := 1;
  x57 := 1;
  x58 := 1;
  x59 := 1;
  x60 := 1;
  x61 := 1;
  x62 := 1;
  x63 := 1;
  x64 := 1;
  x65 := 1;
  x66 := 1;
  x67 := 1;
  x68 := 1;
  x69 := 1;
  x70 := 1;
  x71 := 1;
  x72 := 1;
  x73 := 1;
  x74 := 1;
  x75 := 1;
  x76 := 1;
  x77 := 1;
  x78 := 1;
  x79 := 1;
  x80 := 1;
  x81 := 1;
  x82 := 1;
  x83 := 1;
  x84 := 1;
  x85 := 1;
  x86 := 1;
  x87 := 1;
  x88 := 1;
  x89 := 1;
  x90 := 1;
  x91 := 1;
  x92 := 1;
  x93 := 1;
  x94 := 1;
  x95 := 1;
  x96 := 1;
  x97 := 1;
  x98 := 1;
  x99 := 1;
  x100 := 1;
  x101 := 1;
  x102 := 1;
  x103 := 1;
  x104 := 1;
  x105 := 1;
  x106 := 1;
  x107 := 1;
  x108 := 1;
  x109 := 1;
  x110 := 1;
  x111 := 1;
  x112 := 1;
  x113 := 1;
  x114 := 1;
  x115 := 1;
  x116 := 1;
  x117 := 1;
  x118 := 1;
  x119 := 1;
  x120 := 1;
  x121 := 1;
  x122 := 1;
  x123 := 1;
  x124 := 1;
  x125 := 1;
  x126 := 1;
  x127 := 1;
  x128 := 1;
  x129 := 1;
  x130 := 1;
  x131 := 1;
  x132 := 1;
  x133 := 1;
  x134 := 1;
  x135 := 1;
  x136 := 1;
  x137 := 1;
  x138 := 1;
  x139 := 1;
  x140 := 1;
  x141 := 1;
  x142 := 1;
  x143 := 1;
  x144 := 1;
  x145 := 1;
  x146 := 1;
  x147 := 1;
  x148 := 1;
  x149 := 1;
  x150 := 1;
  x151 := 1;
  x152 := 1;
  x153 := 1;
  x154 := 1;
  x155 := 1;
  x156 := 1;
  x157 := 1;
  x158 := 1;
  x159 := 1;
  x160 := 1;
  x161 := 1;
  x162 := 1;
  x163 := 1;
  x164 := 1;
  x165 := 1;
  x166 := 1;
  x167 := 1;
  x168 := 1;
  x169 := 1;
  x170 := 1;
  x171 := 1;
  x172 := 1;
  x173 := 1;
  x174 := 1;
  x175 := 1;
  x176 := 1;
  x177 := 1;
  x178 := 1;
  x179 := 1;
  x180 := 1;
  x181 := 1;
  x182 := 1;
  x183 := 1;
  x184 := 1;
  x185 := 1;
  x186 := 1;
  x187 := 1;
  x188 := 1;
  x189 := 1;
  x190 := 1;
  x191 := 1;
  x192 := 1;
  x193 := 1;
  x194 := 1;
  x195 := 1;
  x196 := 1;
  x197 := 1;
  x198 := 1;
  x199 := 1;
  while (y >= x0 + x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 + x20 + x21 + x22 + x23 + x24 + x25 + x26 + x27 + x28 + x29 + x30 + x31 + x32 + x33 + x34 + x35 + x36 + x37 + x38 + x39 + x40 + x41 + x42 + x43 + x44 + x45 + x46 + x47 + x48 + x49 + x50 + x51 + x52 + x53 + x54 + x55 + x56 + x57 + x58 + x59 + x60 + x61 + x62 + x63 + x64 + x65 + x66 + x67 + x68 + x69 + x70 + x71 + x72 + x73 + x74 + x75 + x76 + x77 + x78 + x79 + x80 + x81 + x82 + x83 + x84 + x85 + x86 + x87 + x88 + x89 + x90 + x91 + x92 + x93 + x94 + x95 + x96 + x97 + x98 + x99 + x100 + x101 + x102 + x103 + x104 + x105 + x106 + x107 + x108 + x109 + x110 + x111 + x112 + x113 + x114 + x115 + x116 + x117 + x118 + x119 + x120 + x121 + x122 + x123 + x124 + x125 + x126 + x127 + x128 + x129 + x130 + x131 + x132 + x133 + x134 + x135 + x136 + x137 + x138 + x139 + x140 + x141 + x142 + x143 + x144 + x145 + x146 + x147 + x148 + x149 + x150 + x151 + x152 + x153 + x154 + x155 + x156 + x157 + x158 + x159 + x160 + x161 + x162 + x163 + x164 + x165 + x166 + x167 + x168 + x169 + x170 + x171 + x172 + x173 + x174 + x175 + x176 + x177 + x178 + x179 + x180 + x181 + x182 + x183 + x184 + x185 + x186 + x187 + x188 + x189 + x190 + x191 + x192 + x193 + x194 + x195 + x196 + x197 + x198 + x199) {
    y := y - 1;
  }
}