vars
	s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 s19 s20 s21 s22 s23 s24 s25 s26 s27 s28 s29 s30 s31 s32 s33 s34 s35 s36 s37 s38 s39 s40 l0 l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 l11 l12 l13 l14 l15 l16 l17 l18 l19 l20 l21 l22 l23 l24 l25 l26 l27 l28 l29 l30 l31 l32 l33 l34 l35 l36 l37 l38 l39 l40 l41 l42 l43 l44 l45 l46 l47 l48 l49 l50 l51 l52 l53 l54 l55 l56 l57 l58 l59 l60 l61 l62 l63 l64 l65 l66 l67 l68 l69 l70 l71 l72 l73 l74 l75 l76 l77 l78 l79 l80 l81 l82 l83 l84 l85 l86 l87 l88 l89 l90 l91 l92 l93 l94 l95 l96 l97 l98 l99 l100 l101 l102 l103 l104 l105 l106 l107 l108 l109 l110 l111 l112 l113 l114 l115 l116 l117 l118 l119 l120 l121 l122 l123 l124 l125 l126 l127 l128 l129 l130 l131 l132 l133 l134 l135 l136 l137 l138 l139 l140 l141 l142 l143 l144 l145 l146 l147 l148 l149 l150 l151 l152 l153 l154 l155 l156 l157 l158 l159 l160 l161 l162 l163 l164 l165 l166 l167 l168 l169 l170 l171 l172 l173 l174 l175 l176 l177 l178 l179 l180 l181 l182 l183 l184 l185 l186 l187 l188 l189 l190 l191 l192 l193 l194 l195 l196 l197 l198 l199 l200 l201 l202 l203 l204 l205 l206 l207 l208 l209 l210 l211 l212 l213 l214 l215 l216 l217 l218 l219 l220 l221 l222 l223 l224 l225 l226 l227 l228 l229 l230 l231 l232 l233

rules
	l0 >= 1, s0 >= 1 ->
		s0' = s0 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l1' = l1 + 1;

	l0 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s2' = s2 + 1;

	l1 >= 1, s1 >= 1 ->
		l1' = l1 - 1,
		l11' = l11 + 1;

	l11 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s3' = s3 + 1,
		l11' = l11 - 1,
		l44' = l44 + 1;

	l14 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s4' = s4 + 1,
		l14' = l14 - 1,
		l16' = l16 + 1;

	l17 >= 1, s1 >= 1 ->
		l17' = l17 - 1,
		l22' = l22 + 1;

	l20 >= 1, s1 >= 1 ->
		l20' = l20 - 1,
		l30' = l30 + 1;

	l22 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s5' = s5 + 1,
		l22' = l22 - 1,
		l23' = l23 + 1;

	l24 >= 1, s1 >= 1 ->
		l24' = l24 - 1,
		l48' = l48 + 1;

	l26 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s6' = s6 + 1,
		l26' = l26 - 1,
		l27' = l27 + 1;

	l28 >= 1, s1 >= 1 ->
		l28' = l28 - 1,
		l14' = l14 + 1;

	l30 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s7' = s7 + 1,
		l30' = l30 - 1,
		l31' = l31 + 1;

	l43 >= 1, s1 >= 1 ->
		l43' = l43 - 1,
		l26' = l26 + 1;

	l44 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s8' = s8 + 1,
		l44' = l44 - 1,
		l0' = l0 + 1;

	l44 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s9' = s9 + 1,
		l44' = l44 - 1,
		l0' = l0 + 1;

	l44 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s10' = s10 + 1,
		l44' = l44 - 1,
		l0' = l0 + 1;

	l48 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s11' = s11 + 1,
		l48' = l48 - 1,
		l0' = l0 + 1;

	l116 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s12' = s12 + 1,
		l116' = l116 - 1,
		l160' = l160 + 1;

	l118 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s13' = s13 + 1,
		l118' = l118 - 1,
		l175' = l175 + 1;

	l120 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s14' = s14 + 1,
		l120' = l120 - 1,
		l185' = l185 + 1;

	l122 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s15' = s15 + 1,
		l122' = l122 - 1,
		l229' = l229 + 1;

	l123 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s16' = s16 + 1,
		l123' = l123 - 1,
		l229' = l229 + 1;

	l125 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s17' = s17 + 1,
		l125' = l125 - 1,
		l160' = l160 + 1;

	l127 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s18' = s18 + 1,
		l127' = l127 - 1,
		l175' = l175 + 1;

	l129 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s19' = s19 + 1,
		l129' = l129 - 1,
		l185' = l185 + 1;

	l131 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s20' = s20 + 1,
		l131' = l131 - 1,
		l229' = l229 + 1;

	l132 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s21' = s21 + 1,
		l132' = l132 - 1,
		l229' = l229 + 1;

	l155 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s22' = s22 + 1,
		l155' = l155 - 1,
		l0' = l0 + 1;

	l155 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s23' = s23 + 1,
		l155' = l155 - 1,
		l0' = l0 + 1;

	l155 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s24' = s24 + 1,
		l155' = l155 - 1,
		l0' = l0 + 1;

	l155 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s25' = s25 + 1,
		l155' = l155 - 1,
		l0' = l0 + 1;

	l156 >= 1, s1 >= 1 ->
		l156' = l156 - 1,
		l155' = l155 + 1;

	l158 >= 1, s1 >= 1 ->
		l158' = l158 - 1,
		l170' = l170 + 1;

	l161 >= 1, s1 >= 1 ->
		l161' = l161 - 1,
		l180' = l180 + 1;

	l163 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s26' = s26 + 1,
		l163' = l163 - 1,
		l52' = l52 + 1;

	l164 >= 1, s1 >= 1 ->
		l164' = l164 - 1,
		l226' = l226 + 1;

	l166 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s27' = s27 + 1,
		l166' = l166 - 1,
		l52' = l52 + 1;

	l167 >= 1, s1 >= 1 ->
		l167' = l167 - 1,
		l226' = l226 + 1;

	l169 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s28' = s28 + 1,
		l169' = l169 - 1,
		l52' = l52 + 1;

	l170 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s29' = s29 + 1,
		l170' = l170 - 1,
		l0' = l0 + 1;

	l170 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s30' = s30 + 1,
		l170' = l170 - 1,
		l0' = l0 + 1;

	l170 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s31' = s31 + 1,
		l170' = l170 - 1,
		l0' = l0 + 1;

	l170 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s32' = s32 + 1,
		l170' = l170 - 1,
		l0' = l0 + 1;

	l171 >= 1, s1 >= 1 ->
		l171' = l171 - 1,
		l155' = l155 + 1;

	l173 >= 1, s1 >= 1 ->
		l173' = l173 - 1,
		l170' = l170 + 1;

	l180 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s33' = s33 + 1,
		l180' = l180 - 1,
		l0' = l0 + 1;

	l180 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s34' = s34 + 1,
		l180' = l180 - 1,
		l0' = l0 + 1;

	l180 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s35' = s35 + 1,
		l180' = l180 - 1,
		l0' = l0 + 1;

	l180 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s36' = s36 + 1,
		l180' = l180 - 1,
		l0' = l0 + 1;

	l181 >= 1, s1 >= 1 ->
		l181' = l181 - 1,
		l155' = l155 + 1;

	l183 >= 1, s1 >= 1 ->
		l183' = l183 - 1,
		l170' = l170 + 1;

	l203 >= 1, s1 >= 1 ->
		l203' = l203 - 1,
		l163' = l163 + 1;

	l204 >= 1, s1 >= 1 ->
		l204' = l204 - 1,
		l166' = l166 + 1;

	l205 >= 1, s1 >= 1 ->
		l205' = l205 - 1,
		l169' = l169 + 1;

	l206 >= 1, s1 >= 1 ->
		l206' = l206 - 1,
		l176' = l176 + 1;

	l207 >= 1, s1 >= 1 ->
		l207' = l207 - 1,
		l177' = l177 + 1;

	l208 >= 1, s1 >= 1 ->
		l208' = l208 - 1,
		l178' = l178 + 1;

	l209 >= 1, s1 >= 1 ->
		l209' = l209 - 1,
		l179' = l179 + 1;

	l210 >= 1, s1 >= 1 ->
		l210' = l210 - 1,
		l116' = l116 + 1;

	l211 >= 1, s1 >= 1 ->
		l211' = l211 - 1,
		l118' = l118 + 1;

	l212 >= 1, s1 >= 1 ->
		l212' = l212 - 1,
		l120' = l120 + 1;

	l213 >= 1, s1 >= 1 ->
		l213' = l213 - 1,
		l122' = l122 + 1;

	l213 >= 1, s1 >= 1 ->
		l213' = l213 - 1,
		l123' = l123 + 1;

	l214 >= 1, s1 >= 1 ->
		l214' = l214 - 1,
		l125' = l125 + 1;

	l215 >= 1, s1 >= 1 ->
		l215' = l215 - 1,
		l127' = l127 + 1;

	l216 >= 1, s1 >= 1 ->
		l216' = l216 - 1,
		l129' = l129 + 1;

	l217 >= 1, s1 >= 1 ->
		l217' = l217 - 1,
		l131' = l131 + 1;

	l217 >= 1, s1 >= 1 ->
		l217' = l217 - 1,
		l132' = l132 + 1;

	l218 >= 1, s1 >= 1 ->
		l218' = l218 - 1,
		l219' = l219 + 1;

	l220 >= 1, s1 >= 1 ->
		l220' = l220 - 1,
		l221' = l221 + 1;

	l222 >= 1, s1 >= 1 ->
		l222' = l222 - 1,
		l223' = l223 + 1;

	l224 >= 1, s1 >= 1 ->
		l224' = l224 - 1,
		l225' = l225 + 1;

	l226 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s37' = s37 + 1,
		l226' = l226 - 1,
		l0' = l0 + 1;

	l226 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s38' = s38 + 1,
		l226' = l226 - 1,
		l0' = l0 + 1;

	l226 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s39' = s39 + 1,
		l226' = l226 - 1,
		l0' = l0 + 1;

	l226 >= 1, s1 >= 1 ->
		s1' = s1 - 1,
		s40' = s40 + 1,
		l226' = l226 - 1,
		l0' = l0 + 1;

	l227 >= 1, s1 >= 1 ->
		l227' = l227 - 1,
		l155' = l155 + 1;

	l228 >= 1, s1 >= 1 ->
		l228' = l228 - 1,
		l170' = l170 + 1;

	l230 >= 1, s1 >= 1 ->
		l230' = l230 - 1,
		l155' = l155 + 1;

	l231 >= 1, s1 >= 1 ->
		l231' = l231 - 1,
		l170' = l170 + 1;

	l177 >= 1, s2 >= 1 ->
		l177' = l177 - 1,
		l233' = l233 + 1;

	l0 >= 1, s3 >= 1 ->
		s3' = s3 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l43' = l43 + 1;

	l0 >= 1, s4 >= 1 ->
		s4' = s4 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l15' = l15 + 1;

	l0 >= 1, s5 >= 1 ->
		s5' = s5 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l20' = l20 + 1;

	l0 >= 1, s6 >= 1 ->
		s6' = s6 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l24' = l24 + 1;

	l0 >= 1, s7 >= 1 ->
		s7' = s7 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l28' = l28 + 1;

	l23 >= 1, s8 >= 1 ->
		s8' = s8 - 1,
		s1' = s1 + 1,
		l23' = l23 - 1,
		l204' = l204 + 1;

	l27 >= 1, s9 >= 1 ->
		s9' = s9 - 1,
		s1' = s1 + 1,
		l27' = l27 - 1,
		l203' = l203 + 1;

	l31 >= 1, s10 >= 1 ->
		s10' = s10 - 1,
		s1' = s1 + 1,
		l31' = l31 - 1,
		l205' = l205 + 1;

	l52 >= 1, s11 >= 1 ->
		s11' = s11 - 1,
		s1' = s1 + 1,
		l52' = l52 - 1,
		l17' = l17 + 1;

	l0 >= 1, s12 >= 1 ->
		s12' = s12 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l156' = l156 + 1;

	l0 >= 1, s13 >= 1 ->
		s13' = s13 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l171' = l171 + 1;

	l0 >= 1, s14 >= 1 ->
		s14' = s14 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l181' = l181 + 1;

	l0 >= 1, s15 >= 1 ->
		s15' = s15 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l227' = l227 + 1;

	l0 >= 1, s16 >= 1 ->
		s16' = s16 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l230' = l230 + 1;

	l0 >= 1, s17 >= 1 ->
		s17' = s17 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l158' = l158 + 1;

	l0 >= 1, s18 >= 1 ->
		s18' = s18 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l173' = l173 + 1;

	l0 >= 1, s19 >= 1 ->
		s19' = s19 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l183' = l183 + 1;

	l0 >= 1, s20 >= 1 ->
		s20' = s20 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l228' = l228 + 1;

	l0 >= 1, s21 >= 1 ->
		s21' = s21 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l231' = l231 + 1;

	l16 >= 1, s22 >= 1 ->
		s22' = s22 - 1,
		s1' = s1 + 1,
		l16' = l16 - 1,
		l218' = l218 + 1;

	l23 >= 1, s23 >= 1 ->
		s23' = s23 - 1,
		s1' = s1 + 1,
		l23' = l23 - 1,
		l210' = l210 + 1;

	l27 >= 1, s24 >= 1 ->
		s24' = s24 - 1,
		s1' = s1 + 1,
		l27' = l27 - 1,
		l206' = l206 + 1;

	l31 >= 1, s25 >= 1 ->
		s25' = s25 - 1,
		s1' = s1 + 1,
		l31' = l31 - 1,
		l214' = l214 + 1;

	l0 >= 1, s26 >= 1 ->
		s26' = s26 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l161' = l161 + 1;

	l0 >= 1, s27 >= 1 ->
		s27' = s27 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l164' = l164 + 1;

	l0 >= 1, s28 >= 1 ->
		s28' = s28 - 1,
		s1' = s1 + 1,
		l0' = l0 - 1,
		l167' = l167 + 1;

	l16 >= 1, s29 >= 1 ->
		s29' = s29 - 1,
		s1' = s1 + 1,
		l16' = l16 - 1,
		l220' = l220 + 1;

	l23 >= 1, s30 >= 1 ->
		s30' = s30 - 1,
		s1' = s1 + 1,
		l23' = l23 - 1,
		l211' = l211 + 1;

	l27 >= 1, s31 >= 1 ->
		s31' = s31 - 1,
		s1' = s1 + 1,
		l27' = l27 - 1,
		l207' = l207 + 1;

	l31 >= 1, s32 >= 1 ->
		s32' = s32 - 1,
		s1' = s1 + 1,
		l31' = l31 - 1,
		l215' = l215 + 1;

	l16 >= 1, s33 >= 1 ->
		s33' = s33 - 1,
		s1' = s1 + 1,
		l16' = l16 - 1,
		l222' = l222 + 1;

	l23 >= 1, s34 >= 1 ->
		s34' = s34 - 1,
		s1' = s1 + 1,
		l23' = l23 - 1,
		l212' = l212 + 1;

	l27 >= 1, s35 >= 1 ->
		s35' = s35 - 1,
		s1' = s1 + 1,
		l27' = l27 - 1,
		l208' = l208 + 1;

	l31 >= 1, s36 >= 1 ->
		s36' = s36 - 1,
		s1' = s1 + 1,
		l31' = l31 - 1,
		l216' = l216 + 1;

	l16 >= 1, s37 >= 1 ->
		s37' = s37 - 1,
		s1' = s1 + 1,
		l16' = l16 - 1,
		l224' = l224 + 1;

	l23 >= 1, s38 >= 1 ->
		s38' = s38 - 1,
		s1' = s1 + 1,
		l23' = l23 - 1,
		l213' = l213 + 1;

	l27 >= 1, s39 >= 1 ->
		s39' = s39 - 1,
		s1' = s1 + 1,
		l27' = l27 - 1,
		l209' = l209 + 1;

	l31 >= 1, s40 >= 1 ->
		s40' = s40 - 1,
		s1' = s1 + 1,
		l31' = l31 - 1,
		l217' = l217 + 1;

init
	l0 >= 1, s0 = 1, s1 = 0, s2 = 0, s3 = 0, s4 = 0, s5 = 0, s6 = 0, s7 = 0, s8 = 0, s9 = 0, s10 = 0, s11 = 0, s12 = 0, s13 = 0, s14 = 0, s15 = 0, s16 = 0, s17 = 0, s18 = 0, s19 = 0, s20 = 0, s21 = 0, s22 = 0, s23 = 0, s24 = 0, s25 = 0, s26 = 0, s27 = 0, s28 = 0, s29 = 0, s30 = 0, s31 = 0, s32 = 0, s33 = 0, s34 = 0, s35 = 0, s36 = 0, s37 = 0, s38 = 0, s39 = 0, s40 = 0, l1 = 0, l2 = 0, l3 = 0, l4 = 0, l5 = 0, l6 = 0, l7 = 0, l8 = 0, l9 = 0, l10 = 0, l11 = 0, l12 = 0, l13 = 0, l14 = 0, l15 = 0, l16 = 0, l17 = 0, l18 = 0, l19 = 0, l20 = 0, l21 = 0, l22 = 0, l23 = 0, l24 = 0, l25 = 0, l26 = 0, l27 = 0, l28 = 0, l29 = 0, l30 = 0, l31 = 0, l32 = 0, l33 = 0, l34 = 0, l35 = 0, l36 = 0, l37 = 0, l38 = 0, l39 = 0, l40 = 0, l41 = 0, l42 = 0, l43 = 0, l44 = 0, l45 = 0, l46 = 0, l47 = 0, l48 = 0, l49 = 0, l50 = 0, l51 = 0, l52 = 0, l53 = 0, l54 = 0, l55 = 0, l56 = 0, l57 = 0, l58 = 0, l59 = 0, l60 = 0, l61 = 0, l62 = 0, l63 = 0, l64 = 0, l65 = 0, l66 = 0, l67 = 0, l68 = 0, l69 = 0, l70 = 0, l71 = 0, l72 = 0, l73 = 0, l74 = 0, l75 = 0, l76 = 0, l77 = 0, l78 = 0, l79 = 0, l80 = 0, l81 = 0, l82 = 0, l83 = 0, l84 = 0, l85 = 0, l86 = 0, l87 = 0, l88 = 0, l89 = 0, l90 = 0, l91 = 0, l92 = 0, l93 = 0, l94 = 0, l95 = 0, l96 = 0, l97 = 0, l98 = 0, l99 = 0, l100 = 0, l101 = 0, l102 = 0, l103 = 0, l104 = 0, l105 = 0, l106 = 0, l107 = 0, l108 = 0, l109 = 0, l110 = 0, l111 = 0, l112 = 0, l113 = 0, l114 = 0, l115 = 0, l116 = 0, l117 = 0, l118 = 0, l119 = 0, l120 = 0, l121 = 0, l122 = 0, l123 = 0, l124 = 0, l125 = 0, l126 = 0, l127 = 0, l128 = 0, l129 = 0, l130 = 0, l131 = 0, l132 = 0, l133 = 0, l134 = 0, l135 = 0, l136 = 0, l137 = 0, l138 = 0, l139 = 0, l140 = 0, l141 = 0, l142 = 0, l143 = 0, l144 = 0, l145 = 0, l146 = 0, l147 = 0, l148 = 0, l149 = 0, l150 = 0, l151 = 0, l152 = 0, l153 = 0, l154 = 0, l155 = 0, l156 = 0, l157 = 0, l158 = 0, l159 = 0, l160 = 0, l161 = 0, l162 = 0, l163 = 0, l164 = 0, l165 = 0, l166 = 0, l167 = 0, l168 = 0, l169 = 0, l170 = 0, l171 = 0, l172 = 0, l173 = 0, l174 = 0, l175 = 0, l176 = 0, l177 = 0, l178 = 0, l179 = 0, l180 = 0, l181 = 0, l182 = 0, l183 = 0, l184 = 0, l185 = 0, l186 = 0, l187 = 0, l188 = 0, l189 = 0, l190 = 0, l191 = 0, l192 = 0, l193 = 0, l194 = 0, l195 = 0, l196 = 0, l197 = 0, l198 = 0, l199 = 0, l200 = 0, l201 = 0, l202 = 0, l203 = 0, l204 = 0, l205 = 0, l206 = 0, l207 = 0, l208 = 0, l209 = 0, l210 = 0, l211 = 0, l212 = 0, l213 = 0, l214 = 0, l215 = 0, l216 = 0, l217 = 0, l218 = 0, l219 = 0, l220 = 0, l221 = 0, l222 = 0, l223 = 0, l224 = 0, l225 = 0, l226 = 0, l227 = 0, l228 = 0, l229 = 0, l230 = 0, l231 = 0, l232 = 0, l233 = 0

target
	s2 >= 1, l233 >= 1