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