//#rIgnore
// Auto-generated by yPositive-SIscaled.py
// size = 100

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: int;
  assume(x0 >= 1);
  assume(x1 >= 1);
  assume(x2 >= 1);
  assume(x3 >= 1);
  assume(x4 >= 1);
  assume(x5 >= 1);
  assume(x6 >= 1);
  assume(x7 >= 1);
  assume(x8 >= 1);
  assume(x9 >= 1);
  assume(x10 >= 1);
  assume(x11 >= 1);
  assume(x12 >= 1);
  assume(x13 >= 1);
  assume(x14 >= 1);
  assume(x15 >= 1);
  assume(x16 >= 1);
  assume(x17 >= 1);
  assume(x18 >= 1);
  assume(x19 >= 1);
  assume(x20 >= 1);
  assume(x21 >= 1);
  assume(x22 >= 1);
  assume(x23 >= 1);
  assume(x24 >= 1);
  assume(x25 >= 1);
  assume(x26 >= 1);
  assume(x27 >= 1);
  assume(x28 >= 1);
  assume(x29 >= 1);
  assume(x30 >= 1);
  assume(x31 >= 1);
  assume(x32 >= 1);
  assume(x33 >= 1);
  assume(x34 >= 1);
  assume(x35 >= 1);
  assume(x36 >= 1);
  assume(x37 >= 1);
  assume(x38 >= 1);
  assume(x39 >= 1);
  assume(x40 >= 1);
  assume(x41 >= 1);
  assume(x42 >= 1);
  assume(x43 >= 1);
  assume(x44 >= 1);
  assume(x45 >= 1);
  assume(x46 >= 1);
  assume(x47 >= 1);
  assume(x48 >= 1);
  assume(x49 >= 1);
  assume(x50 >= 1);
  assume(x51 >= 1);
  assume(x52 >= 1);
  assume(x53 >= 1);
  assume(x54 >= 1);
  assume(x55 >= 1);
  assume(x56 >= 1);
  assume(x57 >= 1);
  assume(x58 >= 1);
  assume(x59 >= 1);
  assume(x60 >= 1);
  assume(x61 >= 1);
  assume(x62 >= 1);
  assume(x63 >= 1);
  assume(x64 >= 1);
  assume(x65 >= 1);
  assume(x66 >= 1);
  assume(x67 >= 1);
  assume(x68 >= 1);
  assume(x69 >= 1);
  assume(x70 >= 1);
  assume(x71 >= 1);
  assume(x72 >= 1);
  assume(x73 >= 1);
  assume(x74 >= 1);
  assume(x75 >= 1);
  assume(x76 >= 1);
  assume(x77 >= 1);
  assume(x78 >= 1);
  assume(x79 >= 1);
  assume(x80 >= 1);
  assume(x81 >= 1);
  assume(x82 >= 1);
  assume(x83 >= 1);
  assume(x84 >= 1);
  assume(x85 >= 1);
  assume(x86 >= 1);
  assume(x87 >= 1);
  assume(x88 >= 1);
  assume(x89 >= 1);
  assume(x90 >= 1);
  assume(x91 >= 1);
  assume(x92 >= 1);
  assume(x93 >= 1);
  assume(x94 >= 1);
  assume(x95 >= 1);
  assume(x96 >= 1);
  assume(x97 >= 1);
  assume(x98 >= 1);
  assume(x99 >= 1);
  while (y >= 0) {
    y := 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);
    x0 := x0 + 1;
    x1 := x1 + 1;
    x2 := x2 + 1;
    x3 := x3 + 1;
    x4 := x4 + 1;
    x5 := x5 + 1;
    x6 := x6 + 1;
    x7 := x7 + 1;
    x8 := x8 + 1;
    x9 := x9 + 1;
    x10 := x10 + 1;
    x11 := x11 + 1;
    x12 := x12 + 1;
    x13 := x13 + 1;
    x14 := x14 + 1;
    x15 := x15 + 1;
    x16 := x16 + 1;
    x17 := x17 + 1;
    x18 := x18 + 1;
    x19 := x19 + 1;
    x20 := x20 + 1;
    x21 := x21 + 1;
    x22 := x22 + 1;
    x23 := x23 + 1;
    x24 := x24 + 1;
    x25 := x25 + 1;
    x26 := x26 + 1;
    x27 := x27 + 1;
    x28 := x28 + 1;
    x29 := x29 + 1;
    x30 := x30 + 1;
    x31 := x31 + 1;
    x32 := x32 + 1;
    x33 := x33 + 1;
    x34 := x34 + 1;
    x35 := x35 + 1;
    x36 := x36 + 1;
    x37 := x37 + 1;
    x38 := x38 + 1;
    x39 := x39 + 1;
    x40 := x40 + 1;
    x41 := x41 + 1;
    x42 := x42 + 1;
    x43 := x43 + 1;
    x44 := x44 + 1;
    x45 := x45 + 1;
    x46 := x46 + 1;
    x47 := x47 + 1;
    x48 := x48 + 1;
    x49 := x49 + 1;
    x50 := x50 + 1;
    x51 := x51 + 1;
    x52 := x52 + 1;
    x53 := x53 + 1;
    x54 := x54 + 1;
    x55 := x55 + 1;
    x56 := x56 + 1;
    x57 := x57 + 1;
    x58 := x58 + 1;
    x59 := x59 + 1;
    x60 := x60 + 1;
    x61 := x61 + 1;
    x62 := x62 + 1;
    x63 := x63 + 1;
    x64 := x64 + 1;
    x65 := x65 + 1;
    x66 := x66 + 1;
    x67 := x67 + 1;
    x68 := x68 + 1;
    x69 := x69 + 1;
    x70 := x70 + 1;
    x71 := x71 + 1;
    x72 := x72 + 1;
    x73 := x73 + 1;
    x74 := x74 + 1;
    x75 := x75 + 1;
    x76 := x76 + 1;
    x77 := x77 + 1;
    x78 := x78 + 1;
    x79 := x79 + 1;
    x80 := x80 + 1;
    x81 := x81 + 1;
    x82 := x82 + 1;
    x83 := x83 + 1;
    x84 := x84 + 1;
    x85 := x85 + 1;
    x86 := x86 + 1;
    x87 := x87 + 1;
    x88 := x88 + 1;
    x89 := x89 + 1;
    x90 := x90 + 1;
    x91 := x91 + 1;
    x92 := x92 + 1;
    x93 := x93 + 1;
    x94 := x94 + 1;
    x95 := x95 + 1;
    x96 := x96 + 1;
    x97 := x97 + 1;
    x98 := x98 + 1;
    x99 := x99 + 1;
  }
}