text: input = """
  c num blocks = 1
  c num vars = 160
  c minblockids[0] = 1
  c maxblockids[0] = 160
  p cnf 160 660
  -52 18 -42 0
  -5 -34 -128 0
  121 95 -82 0
  43 33 138 0
  145 66 116 0
  -68 62 -116 0
  64 68 -37 0
  32 -135 -130 0
  150 -138 -52 0
  90 -7 -3 0
  27 -35 139 0
  -13 134 111 0
  92 -78 50 0
  73 137 -24 0
  62 143 -36 0
  59 159 -83 0
  -52 -94 115 0
  -75 -61 28 0
  -95 -87 102 0
  145 13 76 0
  -75 139 95 0
  -6 71 -99 0
  116 -18 152 0
  -150 3 109 0
  41 -120 27 0
  -159 -87 -4 0
  90 -45 -73 0
  -107 -116 -39 0
  -33 103 -76 0
  -149 58 26 0
  138 -83 136 0
  -115 17 -32 0
  95 -70 69 0
  35 42 121 0
  -135 -132 -65 0
  -72 66 130 0
  37 -78 -160 0
  158 110 -23 0
  -113 63 -160 0
  117 15 129 0
  102 -49 -24 0
  -29 -8 -53 0
  132 -90 27 0
  26 74 145 0
  -12 -28 157 0
  -59 -125 35 0
  140 112 8 0
  119 -146 149 0
  -32 -153 66 0
  -92 -95 -56 0
  91 108 121 0
  -81 39 8 0
  -6 -142 -128 0
  154 16 -102 0
  -113 111 -86 0
  39 -123 -2 0
  -17 -146 -5 0
  -129 90 -15 0
  -5 82 -139 0
  -77 -1 -144 0
  76 110 -149 0
  -30 -155 -25 0
  66 18 155 0
  -15 -70 152 0
  100 -86 4 0
  97 -64 -45 0
  120 -95 -143 0
  -38 147 2 0
  154 -137 143 0
  -154 38 -95 0
  122 1 62 0
  -41 82 130 0
  157 -38 88 0
  -66 82 38 0
  -98 -114 102 0
  -62 -150 -25 0
  -118 -22 100 0
  -46 -12 -65 0
  -113 -81 62 0
  -122 134 126 0
  -145 79 -50 0
  46 -94 -69 0
  -156 1 34 0
  91 45 86 0
  108 96 43 0
  -60 160 59 0
  -78 -139 -144 0
  -111 -160 65 0
  -110 -91 -22 0
  -131 -93 68 0
  -56 -68 -109 0
  -81 -54 113 0
  47 -134 -79 0
  43 160 -28 0
  -130 85 39 0
  -92 29 -46 0
  96 145 -34 0
  33 -115 48 0
  -16 -62 150 0
  -46 131 43 0
  -70 159 -102 0
  -18 15 -141 0
  90 60 -130 0
  18 -55 -129 0
  153 91 -140 0
  -36 -153 79 0
  -137 -52 -78 0
  138 -131 29 0
  66 -73 128 0
  -16 -75 22 0
  -113 55 -65 0
  10 -113 -4 0
  58 96 -30 0
  -144 108 -16 0
  -84 -119 87 0
  -7 -23 -40 0
  -56 126 -36 0
  77 105 159 0
  -25 -86 1 0
  -82 51 119 0
  76 -122 120 0
  83 90 92 0
  76 -79 59 0
  106 83 -116 0
  76 142 42 0
  -74 95 -133 0
  44 -148 72 0
  -140 -158 -16 0
  -60 -147 -135 0
  -146 28 44 0
  -52 -31 -138 0
  120 22 58 0
  -67 -122 111 0
  -149 -155 -94 0
  -149 133 -46 0
  117 7 -113 0
  -157 -88 -47 0
  72 -62 89 0
  36 117 82 0
  -111 -125 -142 0
  130 12 94 0
  3 147 -62 0
  1 -9 -69 0
  -118 -28 116 0
  73 15 28 0
  137 156 -104 0
  -154 53 -3 0
  -113 72 20 0
  156 89 -58 0
  -78 -45 -148 0
  -61 51 -42 0
  44 -45 -100 0
  150 -68 -114 0
  -60 -30 7 0
  -114 50 154 0
  129 -56 -158 0
  70 45 35 0
  -139 106 157 0
  -113 123 -92 0
  -63 91 -6 0
  81 -79 -61 0
  90 113 -152 0
  -157 -81 -68 0
  -21 -60 -128 0
  -38 -105 73 0
  -107 96 109 0
  -119 14 135 0
  -14 43 105 0
  -156 56 -9 0
  -25 -51 113 0
  144 61 94 0
  112 133 -53 0
  64 154 -124 0
  -7 31 -63 0
  122 -82 -84 0
  -53 149 70 0
  -35 95 -26 0
  1 48 113 0
  56 125 -32 0
  -93 -124 104 0
  56 99 27 0
  -110 -87 -107 0
  -141 -160 45 0
  117 -135 59 0
  -45 -38 76 0
  -46 39 2 0
  121 87 91 0
  -80 -75 -40 0
  -109 75 -106 0
  138 -154 -132 0
  63 39 -50 0
  94 137 -48 0
  -128 -152 -117 0
  98 74 -144 0
  -63 -22 -109 0
  100 -78 -76 0
  57 130 83 0
  56 9 -137 0
  97 25 -140 0
  107 -84 152 0
  -59 -145 -113 0
  -42 -155 67 0
  -154 136 -112 0
  23 34 91 0
  -41 -67 136 0
  103 -156 -94 0
  66 -46 -13 0
  -138 44 159 0
  -140 -41 -153 0
  -86 -41 81 0
  150 99 -82 0
  133 56 -119 0
  -44 147 -55 0
  29 53 150 0
  68 116 -138 0
  -58 -32 -127 0
  -154 -10 -81 0
  -78 80 26 0
  77 14 94 0
  136 -130 69 0
  26 -155 69 0
  -92 23 62 0
  -160 50 112 0
  -78 109 -85 0
  -148 -144 35 0
  -98 32 -159 0
  153 133 -16 0
  85 -29 -88 0
  -121 97 66 0
  -64 -90 -42 0
  131 -105 116 0
  33 67 -118 0
  -22 -2 -159 0
  5 -34 137 0
  159 52 -43 0
  130 -91 55 0
  -40 74 66 0
  -143 -80 27 0
  75 -80 -2 0
  -9 102 -76 0
  117 -45 -135 0
  96 73 90 0
  1 151 -54 0
  45 -38 -131 0
  158 37 35 0
  -83 124 151 0
  130 -116 -18 0
  63 -98 -67 0
  148 -57 23 0
  54 111 -132 0
  20 -142 144 0
  -142 89 56 0
  10 -51 68 0
  69 148 -131 0
  -48 -158 17 0
  62 -9 -61 0
  -145 -34 143 0
  -100 -119 -107 0
  -88 -65 -101 0
  24 83 -87 0
  -127 -5 -48 0
  -43 44 -125 0
  3 -8 -85 0
  -63 4 -153 0
  -135 141 10 0
  -17 -100 82 0
  -7 27 63 0
  -103 8 90 0
  94 22 122 0
  25 40 -71 0
  -123 -139 -22 0
  -27 -132 111 0
  -32 -103 -82 0
  93 150 -146 0
  133 -6 91 0
  129 153 36 0
  45 -38 63 0
  44 92 -48 0
  127 -122 1 0
  93 -136 -62 0
  -104 -140 37 0
  9 -160 10 0
  120 -94 114 0
  -104 -78 131 0
  146 -64 -85 0
  -145 77 -32 0
  -50 29 -52 0
  -44 -43 130 0
  148 -106 -11 0
  139 39 14 0
  71 -50 60 0
  -21 -69 31 0
  54 4 30 0
  -136 99 17 0
  -128 61 -140 0
  -53 -38 25 0
  132 -46 150 0
  91 134 35 0
  -100 97 17 0
  -51 -11 138 0
  -150 -115 -73 0
  -52 -116 47 0
  -62 -87 89 0
  -148 120 -81 0
  -21 -54 -75 0
  2 151 124 0
  -78 -65 -7 0
  -69 120 -150 0
  -45 -46 129 0
  48 23 74 0
  75 -61 10 0
  -23 -107 -22 0
  -150 -8 146 0
  26 125 -47 0
  -1 36 -81 0
  152 88 5 0
  19 -31 23 0
  -73 -50 47 0
  29 62 89 0
  121 -86 -35 0
  63 -101 -25 0
  2 160 -87 0
  -25 -66 12 0
  -79 -3 -76 0
  69 29 -15 0
  98 157 75 0
  -53 37 -91 0
  119 140 42 0
  128 9 -117 0
  117 -97 -1 0
  99 12 -128 0
  120 72 141 0
  86 140 115 0
  -147 -9 -72 0
  98 152 -2 0
  49 26 3 0
  106 -85 145 0
  127 -131 39 0
  155 45 -124 0
  70 46 122 0
  -45 -65 31 0
  -66 71 147 0
  144 -78 23 0
  117 112 66 0
  -9 73 -23 0
  107 78 68 0
  -89 -76 123 0
  31 -143 147 0
  -121 52 -35 0
  29 -61 93 0
  -82 -110 -119 0
  -15 123 92 0
  -80 -40 -121 0
  -35 -52 -42 0
  137 113 79 0
  -106 -94 -49 0
  44 -69 157 0
  126 135 143 0
  101 1 104 0
  -148 -117 135 0
  -116 44 51 0
  45 67 -48 0
  -10 132 -143 0
  -74 4 93 0
  -68 103 108 0
  -90 -132 106 0
  100 101 27 0
  129 -9 59 0
  95 -88 89 0
  -17 48 -7 0
  39 -133 63 0
  148 93 -88 0
  126 22 89 0
  -16 30 135 0
  -63 90 88 0
  21 -18 -11 0
  -160 19 -12 0
  -106 -135 68 0
  79 93 -118 0
  29 -50 -116 0
  -124 137 16 0
  -60 146 -143 0
  13 -66 86 0
  -51 -27 76 0
  -144 -128 32 0
  40 138 123 0
  -64 84 138 0
  139 -65 -160 0
  48 -123 -69 0
  134 -18 146 0
  -150 69 92 0
  65 -124 84 0
  37 -61 14 0
  -85 -87 -134 0
  -1 126 21 0
  127 -120 48 0
  -55 -3 -2 0
  51 -111 -78 0
  135 107 -82 0
  155 5 -104 0
  2 -131 -41 0
  137 18 -26 0
  87 6 -103 0
  -131 -50 43 0
  158 113 -134 0
  -119 79 88 0
  17 46 -147 0
  108 -36 -24 0
  41 120 5 0
  -38 -72 140 0
  -3 -144 -145 0
  -44 -66 -2 0
  86 117 109 0
  -57 -159 -85 0
  -14 158 -135 0
  70 -15 -89 0
  47 21 -97 0
  -127 -52 -35 0
  -90 61 25 0
  26 59 -40 0
  18 70 -89 0
  1 -4 -67 0
  -69 -123 -53 0
  135 -100 -36 0
  16 37 -40 0
  -67 -125 -120 0
  125 -77 114 0
  57 -51 58 0
  155 -43 97 0
  -20 37 122 0
  101 114 43 0
  -22 -73 -132 0
  -77 52 -159 0
  63 17 -105 0
  -133 30 102 0
  113 57 -7 0
  92 107 -112 0
  96 45 -50 0
  110 13 -15 0
  -50 118 13 0
  71 49 95 0
  -134 21 -33 0
  88 -129 -141 0
  121 -110 -59 0
  -110 -9 -46 0
  8 60 -61 0
  -43 -17 134 0
  -145 -45 102 0
  38 59 -44 0
  -141 -143 -13 0
  -126 -103 -145 0
  -9 -12 41 0
  -155 -152 93 0
  133 -75 -126 0
  -47 -128 -156 0
  -70 150 -27 0
  -125 -31 59 0
  72 -15 65 0
  -56 -11 114 0
  41 54 -129 0
  -45 -24 75 0
  1 114 -108 0
  -145 -45 -52 0
  32 159 90 0
  154 -101 5 0
  140 159 4 0
  100 -125 40 0
  -92 -54 -59 0
  27 -122 -68 0
  -155 20 -122 0
  -118 90 159 0
  3 -72 -31 0
  -112 -35 34 0
  79 -74 -91 0
  -66 17 133 0
  -40 -15 52 0
  64 -136 73 0
  9 -46 -27 0
  -73 34 -43 0
  -11 -48 -63 0
  -156 113 -144 0
  -144 -131 -157 0
  -119 91 -30 0
  28 -94 15 0
  127 -32 -56 0
  156 55 -90 0
  122 -65 -79 0
  137 -120 99 0
  -143 -99 -25 0
  85 -109 6 0
  -123 -30 -160 0
  43 48 -56 0
  -36 -91 41 0
  -13 148 101 0
  84 -68 -86 0
  -66 -4 61 0
  131 30 -148 0
  -123 59 9 0
  -78 -97 64 0
  30 157 7 0
  131 -11 -7 0
  -130 20 -102 0
  84 52 78 0
  -136 77 -95 0
  -22 -77 -142 0
  -139 -142 -121 0
  11 -70 102 0
  -145 10 131 0
  -57 -113 6 0
  -15 97 -109 0
  74 -39 92 0
  143 -59 21 0
  -40 22 -133 0
  -97 -142 -8 0
  -118 68 -119 0
  -150 14 156 0
  -108 7 -154 0
  -23 20 -33 0
  -32 86 -124 0
  67 -49 -77 0
  -22 38 -56 0
  95 72 -17 0
  152 -110 -72 0
  99 -36 -50 0
  30 -85 34 0
  102 61 80 0
  55 2 57 0
  135 48 116 0
  -100 -127 81 0
  68 -142 -156 0
  -32 -129 80 0
  115 -123 114 0
  -11 -30 51 0
  -43 146 15 0
  43 -67 -157 0
  -92 -8 158 0
  -65 146 99 0
  -105 -67 41 0
  92 -137 116 0
  28 -136 8 0
  138 -127 38 0
  -127 4 -21 0
  -54 -68 100 0
  -138 -65 -18 0
  -100 -89 49 0
  38 -97 60 0
  -26 -99 -21 0
  -101 21 -110 0
  101 14 -125 0
  123 -30 -94 0
  57 -141 127 0
  54 42 -112 0
  17 117 -50 0
  -109 -44 -89 0
  -116 -40 28 0
  -125 -132 100 0
  40 -43 -96 0
  -24 -138 -105 0
  -36 143 114 0
  25 -135 -111 0
  -114 60 75 0
  -122 -107 88 0
  116 104 28 0
  -145 -78 -24 0
  145 -47 148 0
  23 -108 -73 0
  116 59 91 0
  -118 -160 -114 0
  -54 139 -13 0
  -25 -131 -82 0
  152 29 16 0
  -100 -60 50 0
  -54 135 -38 0
  51 -145 72 0
  -78 -63 153 0
  -46 97 17 0
  -115 -24 89 0
  -61 -45 -42 0
  108 -68 -113 0
  102 96 -127 0
  -69 -52 19 0
  73 -72 82 0
  -116 21 129 0
  -61 -5 30 0
  -77 154 91 0
  108 -140 35 0
  -105 -109 -125 0
  153 -149 34 0
  -102 -90 153 0
  66 30 -31 0
  155 49 -73 0
  -19 -48 99 0
  -64 106 -61 0
  145 -21 -143 0
  116 86 -41 0
  7 -17 -72 0
  32 -36 25 0
  160 16 -35 0
  -159 -27 -82 0
  -84 150 28 0
  104 128 67 0
  -61 144 -22 0
  -49 -59 -71 0
  -42 32 58 0
  65 -156 82 0
  116 -66 -9 0
  10 160 44 0
  -100 144 -90 0
  52 -146 5 0
  -13 -160 159 0
  -30 141 54 0
  -153 -42 10 0
  -57 -61 43 0
  79 30 128 0
  -153 -118 -27 0
  8 140 -94 0
  130 -103 55 0
  -137 87 158 0
  5 153 -61 0
  -9 6 -140 0
  -147 62 132 0
  -1 89 155 0
  146 29 122 0
  1 -113 128 0
  14 -56 33 0
  -12 -147 59 0
  26 -11 121 0
  30 19 -100 0
  99 -81 57 0
  -12 -45 -93 0
  20 -55 43 0
  156 95 89 0
  159 -82 -123 0
  48 -19 -13 0
  -139 -159 118 0
  -116 154 5 0
  -91 -16 -28 0
  157 42 106 0
  -44 118 -19 0
  76 25 -150 0
  -11 -70 51 0
  -108 48 73 0
  -106 84 104 0
  142 18 131 0
  -157 -118 -19 0
  -154 62 -90 0
  -150 56 -39 0
  146 101 -20 0
  47 -14 89 0
  145 -129 -33 0
  63 59 141 0
  -154 -160 140 0
  -83 107 156 0
  -24 -22 49 0
  96 -103 -137 0
  -132 -61 143 0
  123 -68 -119 0
  -51 33 146 0
  154 50 91 0
  -64 -60 115 0
  """
  
  output = "SAT"
  