text: input = """
  c num blocks = 1
  c num vars = 100
  c minblockids[0] = 1
  c maxblockids[0] = 100
  p cnf 100 405
  15 -27 78 0
  97 -3 87 0
  -100 -13 60 0
  -25 -97 -83 0
  -92 -40 28 0
  71 -96 -30 0
  4 -61 36 0
  -44 100 7 0
  -91 43 -52 0
  89 -70 -97 0
  11 59 60 0
  82 -51 -16 0
  -94 55 42 0
  68 -86 -20 0
  79 -40 15 0
  71 -4 -54 0
  -33 -87 -61 0
  54 -64 -63 0
  -41 -47 -81 0
  -66 4 -70 0
  -32 -14 -61 0
  -28 -40 67 0
  2 -59 -57 0
  -68 -3 -18 0
  -93 49 -96 0
  24 49 -31 0
  -18 32 91 0
  62 65 -57 0
  -64 78 10 0
  66 -88 34 0
  53 -30 -64 0
  31 -22 -93 0
  -34 61 47 0
  -20 85 -64 0
  29 -39 -49 0
  15 -7 90 0
  71 -97 -42 0
  -32 71 1 0
  -24 -81 7 0
  -90 -62 -84 0
  -75 2 -49 0
  -4 92 91 0
  97 -29 -11 0
  12 -44 -29 0
  -38 60 11 0
  -56 -5 25 0
  -69 -13 -56 0
  -65 86 78 0
  -74 65 -35 0
  -22 -68 -55 0
  50 65 -14 0
  10 -5 -87 0
  -16 23 59 0
  -75 -70 64 0
  72 -44 28 0
  58 -86 33 0
  -96 -67 4 0
  55 1 -77 0
  -14 41 67 0
  -97 88 92 0
  97 77 -55 0
  -64 37 -98 0
  63 -64 -11 0
  -3 34 -8 0
  -49 5 -68 0
  -96 -51 24 0
  -100 47 -54 0
  68 -55 6 0
  -13 -17 -52 0
  -52 5 22 0
  -94 -73 -75 0
  4 -1 96 0
  -14 37 71 0
  86 43 -33 0
  -27 97 -9 0
  -3 4 12 0
  50 90 46 0
  46 97 -55 0
  88 97 77 0
  -79 -97 31 0
  -28 87 -56 0
  -99 -52 49 0
  -12 -65 33 0
  -29 -44 -38 0
  -52 -73 -75 0
  9 -44 46 0
  61 11 -57 0
  93 -23 17 0
  71 -44 73 0
  37 20 -24 0
  -81 -45 -57 0
  -81 52 33 0
  87 -19 -27 0
  64 -87 -51 0
  41 -12 -51 0
  29 4 14 0
  -14 -65 8 0
  -54 -6 12 0
  -9 23 -11 0
  -45 25 23 0
  -57 -9 30 0
  -44 -24 67 0
  -60 -76 30 0
  44 -26 51 0
  -18 -52 -15 0
  11 97 29 0
  -61 89 -28 0
  38 13 -64 0
  30 7 -84 0
  -36 -45 69 0
  -74 -89 -19 0
  -21 99 65 0
  97 80 22 0
  35 78 63 0
  -81 33 -8 0
  -27 -77 94 0
  -92 2 -11 0
  -24 86 97 0
  18 57 -25 0
  12 6 76 0
  -62 -70 83 0
  -7 -71 100 0
  -19 71 95 0
  -32 -71 -23 0
  11 -18 82 0
  -35 -92 -1 0
  -16 -78 -88 0
  -6 98 39 0
  -87 -74 -47 0
  30 16 86 0
  43 34 87 0
  24 100 -83 0
  13 44 -60 0
  100 -33 -94 0
  61 -32 -24 0
  55 -16 -51 0
  -70 22 95 0
  -1 -10 5 0
  75 3 35 0
  -38 11 81 0
  -39 64 -99 0
  -3 -50 49 0
  79 32 -26 0
  84 -44 -60 0
  94 -32 61 0
  -14 -81 46 0
  31 85 -42 0
  -37 14 82 0
  89 -18 -68 0
  80 -77 -39 0
  33 -27 -88 0
  -56 -67 -20 0
  -61 84 -60 0
  -62 14 -10 0
  -94 88 -65 0
  -80 61 -70 0
  37 -22 70 0
  25 29 -2 0
  -21 66 -26 0
  -42 -61 36 0
  83 -38 -56 0
  37 -18 9 0
  97 -79 -30 0
  -15 42 2 0
  -5 -90 -8 0
  -10 -81 79 0
  -74 -96 -60 0
  -22 18 47 0
  45 -5 84 0
  51 -87 53 0
  -60 -11 70 0
  45 64 18 0
  15 -78 56 0
  9 -85 -92 0
  43 -89 82 0
  -2 63 9 0
  58 45 -16 0
  78 53 87 0
  87 47 -89 0
  66 -43 94 0
  76 29 -34 0
  -24 -34 43 0
  66 -68 -12 0
  79 61 48 0
  -31 -72 75 0
  93 8 -73 0
  76 90 53 0
  65 -60 -63 0
  -78 51 -57 0
  -36 57 -76 0
  67 -83 15 0
  -36 94 67 0
  11 -68 -30 0
  -54 -40 -73 0
  30 50 94 0
  35 31 43 0
  -92 -50 97 0
  -1 -55 -4 0
  -5 -15 55 0
  19 46 -78 0
  89 -18 -19 0
  -21 -41 -62 0
  81 30 59 0
  -91 58 35 0
  -36 26 -55 0
  15 -80 -87 0
  89 -47 66 0
  60 38 47 0
  -39 -86 -34 0
  -23 43 -31 0
  24 -79 -98 0
  -86 91 -90 0
  -99 64 -100 0
  -22 -81 65 0
  13 -15 -51 0
  -80 -52 -1 0
  -22 72 -13 0
  87 -58 -19 0
  25 3 19 0
  -87 21 90 0
  53 -80 -14 0
  -30 -46 -3 0
  -81 51 -24 0
  10 65 44 0
  62 4 74 0
  -11 77 15 0
  67 17 -12 0
  49 -48 -20 0
  43 95 65 0
  30 -25 -8 0
  75 -34 89 0
  98 -90 -4 0
  77 31 74 0
  -66 -100 -87 0
  8 92 68 0
  63 -29 -5 0
  -93 45 71 0
  -13 -15 -52 0
  -29 76 1 0
  -71 50 -82 0
  -17 61 21 0
  -72 17 -85 0
  94 45 72 0
  18 1 -56 0
  -6 -1 69 0
  -26 -11 -96 0
  -72 -38 -94 0
  -1 -96 18 0
  29 100 -10 0
  26 -46 6 0
  -55 48 -90 0
  76 -75 9 0
  -24 84 -36 0
  19 29 -48 0
  52 45 -51 0
  -36 46 96 0
  -74 -85 -96 0
  50 -92 -31 0
  -38 48 -61 0
  81 -89 -49 0
  -87 93 48 0
  90 -46 87 0
  83 -59 -15 0
  -46 -78 69 0
  -47 82 -79 0
  -31 -62 -79 0
  55 53 10 0
  84 28 -68 0
  -33 -78 -14 0
  -94 -33 -67 0
  -2 7 -84 0
  -88 -93 -97 0
  -73 13 63 0
  -45 -6 4 0
  -38 18 45 0
  48 -47 -99 0
  -76 -92 -13 0
  -91 -99 100 0
  19 88 83 0
  -1 98 -24 0
  -77 72 40 0
  32 -41 -77 0
  -45 94 34 0
  98 28 29 0
  55 -75 93 0
  -4 29 -42 0
  73 -99 43 0
  87 -36 -90 0
  -45 -47 61 0
  52 86 7 0
  -1 13 9 0
  43 10 -93 0
  13 -37 26 0
  -41 47 -27 0
  9 69 68 0
  81 82 41 0
  18 -57 64 0
  -82 -73 30 0
  14 31 88 0
  30 -17 49 0
  27 4 22 0
  -61 -22 -10 0
  1 -62 20 0
  50 79 -29 0
  -62 32 -61 0
  -35 -74 41 0
  49 42 -81 0
  20 7 6 0
  33 80 -50 0
  14 25 41 0
  5 -56 -19 0
  -33 70 32 0
  -54 92 -33 0
  -57 -58 -66 0
  29 -50 -31 0
  -42 -35 -49 0
  45 36 -55 0
  25 -2 60 0
  76 -22 47 0
  -23 27 -85 0
  -32 -17 -2 0
  -40 69 -66 0
  77 -5 61 0
  17 46 -38 0
  -50 -75 -98 0
  70 -43 -81 0
  47 61 8 0
  -59 68 -75 0
  11 34 -69 0
  -18 -27 -54 0
  -9 -29 59 0
  51 30 88 0
  24 -61 60 0
  70 -11 36 0
  -69 57 63 0
  58 57 93 0
  22 -13 77 0
  42 79 -50 0
  26 82 -78 0
  91 57 15 0
  -97 44 16 0
  85 -3 -89 0
  -17 -59 84 0
  -60 34 97 0
  6 -73 41 0
  42 82 -66 0
  -86 -77 -16 0
  -58 71 56 0
  19 -61 39 0
  87 98 -26 0
  -3 16 96 0
  -93 86 77 0
  -84 74 52 0
  -78 8 -1 0
  -12 -87 -97 0
  -26 -99 95 0
  -47 -66 -95 0
  -1 -77 45 0
  74 27 15 0
  18 -4 -94 0
  26 11 43 0
  82 77 -7 0
  -53 93 32 0
  -64 -21 -26 0
  -15 -33 -41 0
  24 -34 -47 0
  15 -94 80 0
  76 3 28 0
  4 -95 90 0
  53 -68 62 0
  -85 97 22 0
  13 -87 79 0
  -51 -6 44 0
  -60 -16 -42 0
  -20 -80 -28 0
  57 -2 -52 0
  52 -38 12 0
  14 -29 -85 0
  -64 -80 35 0
  48 -24 32 0
  12 13 -49 0
  2 26 22 0
  92 -99 10 0
  75 7 25 0
  -87 44 -25 0
  18 -6 91 0
  15 -8 20 0
  98 -42 -13 0
  63 -64 -3 0
  84 -35 -88 0
  -51 -29 31 0
  14 11 -35 0
  34 99 7 0
  -71 25 -52 0
  -7 -13 -78 0
  45 -83 9 0
  94 2 84 0
  8 12 1 0
  -98 -26 -61 0
  67 -8 71 0
  72 -9 60 0
  -29 6 19 0
  99 -29 -81 0
  40 -24 -75 0
  -78 -46 -50 0
  """
  
  output = "SAT"
  