var m01 binary; var m02 binary; var m03 binary; var m04 binary; var m05 binary; var m06 binary; var m07 binary; var m08 binary; var m09 binary; var m10 binary; var m11 binary; var m12 binary; var m13 binary; var m14 binary; var m15 binary; var m16 binary; var m17 binary; var m18 binary; var m19 binary; var m20 binary; var m21 binary; var m22 binary; var m23 binary; var m24 binary; var m25 binary; var m26 binary; var m27 binary; var m28 binary; var m29 binary; var m30 binary; var m31 binary; var m32 binary; var m33 binary; var m34 binary; var m35 binary; var m36 binary; var m37 binary; var m38 binary; var m39 binary; var m40 binary; var m41 binary; var m42 binary; var m43 binary; var m44 binary; var m45 binary; var m46 binary; var m47 binary; var m48 binary; var m49 binary; var m50 binary; var m51 binary; var m52 binary; var m53 binary; var m54 binary; var m55 binary; var m56 binary; var m57 binary; var m58 binary; var m59 binary; var m60 binary; var m61 binary; var m62 binary; var m63 binary; var m64 binary; var m65 binary; var m66 binary; var m67 binary; var m68 binary; var m69 binary; var m70 binary; var m71 binary; var m72 binary; var m73 binary; var m74 binary; var m75 binary; var m76 binary; var m77 binary; var m78 binary; var m79 binary; var m80 binary; var m81 binary; var m82 binary; var m83 binary; var m84 binary; minimize z: m01 + m02 + m03 + m04 + m05 + m06 + m07 + m08 + m09 + m10 + m11 + m12 + m13 + m14 + m15 + m16 + m17 + m18 + m19 + m20 + m21 + m22 + m23 + m24 + m25 + m26 + m27 + m28 + m29 + m30 + m31 + m32 + m33 + m34 + m35 + m36 + m37 + m38 + m39 + m40 + m41 + m42 + m43 + m44 + m45 + m46 + m47 + m48 + m49 + m50 + m51 + m52 + m53 + m54 + m55 + m56 + m57 + m58 + m59 + m60 + m61 + m62 + m63 + m64 + m65 + m66 + m67 + m68 + m69 + m70 + m71 + m72 + m73 + m74 + m75 + m76 + m77 + m78 + m79 + m80 + m81 + m82 + m83 + m84 ; s.t. st1: m01 + m02 + m03 + m04 + m05 + m06 + m07 + m08 + m09 + m10 + m11 + m12 + m13 + m14 + m15 + m16 + m17 + m18 + m19 + m20 + m21 + m22 + m23 + m24 + m25 + m26 + m27 + m28 = 4; s.t. st2: m01 + m02 + m03 + m04 + m05 + m06 + m07 + m29 + m30 + m31 + m32 + m33 + m34 + m35 + m36 + m37 + m38 + m39 + m40 + m41 + m42 + m43 + m44 + m45 + m46 + m47 + m48 + m49 = 4; s.t. st3: m01 + m08 + m09 + m10 + m11 + m12 + m13 + m29 + m30 + m31 + m32 + m33 + m34 + m50 + m51 + m52 + m53 + m54 + m55 + m56 + m57 + m58 + m59 + m60 + m61 + m62 + m63 + m64 = 4; s.t. st4: m02 + m08 + m14 + m15 + m16 + m17 + m18 + m29 + m35 + m36 + m37 + m38 + m39 + m50 + m51 + m52 + m53 + m54 + m65 + m66 + m67 + m68 + m69 + m70 + m71 + m72 + m73 + m74 = 4; s.t. st5: m03 + m09 + m14 + m19 + m20 + m21 + m22 + m30 + m35 + m40 + m41 + m42 + m43 + m50 + m55 + m56 + m57 + m58 + m65 + m66 + m67 + m68 + m75 + m76 + m77 + m78 + m79 + m80 = 4; s.t. st6: m04 + m10 + m15 + m19 + m23 + m24 + m25 + m31 + m36 + m40 + m44 + m45 + m46 + m51 + m55 + m59 + m60 + m61 + m65 + m69 + m70 + m71 + m75 + m76 + m77 + m81 + m82 + m83 = 4; s.t. st7: m05 + m11 + m16 + m20 + m23 + m26 + m27 + m32 + m37 + m41 + m44 + m47 + m48 + m52 + m56 + m59 + m62 + m63 + m66 + m69 + m72 + m73 + m75 + m78 + m79 + m81 + m82 + m84 = 4; s.t. st8: m06 + m12 + m17 + m21 + m24 + m26 + m28 + m33 + m38 + m42 + m45 + m47 + m49 + m53 + m57 + m60 + m62 + m64 + m67 + m70 + m72 + m74 + m76 + m78 + m80 + m81 + m83 + m84 = 4; s.t. st9: m07 + m13 + m18 + m22 + m25 + m27 + m28 + m34 + m39 + m43 + m46 + m48 + m49 + m54 + m58 + m61 + m63 + m64 + m68 + m71 + m73 + m74 + m77 + m79 + m80 + m82 + m83 + m84 = 4; s.t. st12: m01 + m02 + m03 + m04 + m05 + m06 + m07 = 1; s.t. st13: m01 + m08 + m09 + m10 + m11 + m12 + m13 = 1; s.t. st14: m02 + m08 + m14 + m15 + m16 + m17 + m18 = 1; s.t. st15: m03 + m09 + m14 + m19 + m20 + m21 + m22 = 1; s.t. st16: m04 + m10 + m15 + m19 + m23 + m24 + m25 = 1; s.t. st17: m05 + m11 + m16 + m20 + m23 + m26 + m27 = 1; s.t. st18: m06 + m12 + m17 + m21 + m24 + m26 + m28 = 1; s.t. st19: m07 + m13 + m18 + m22 + m25 + m27 + m28 = 1; s.t. st23: m01 + m29 + m30 + m31 + m32 + m33 + m34 = 1; s.t. st24: m02 + m29 + m35 + m36 + m37 + m38 + m39 = 1; s.t. st25: m03 + m30 + m35 + m40 + m41 + m42 + m43 = 1; s.t. st26: m04 + m31 + m36 + m40 + m44 + m45 + m46 = 1; s.t. st27: m05 + m32 + m37 + m41 + m44 + m47 + m48 = 1; s.t. st28: m06 + m33 + m38 + m42 + m45 + m47 + m49 = 1; s.t. st29: m07 + m34 + m39 + m43 + m46 + m48 + m49 = 1; s.t. st34: m08 + m29 + m50 + m51 + m52 + m53 + m54 = 1; s.t. st35: m09 + m30 + m50 + m55 + m56 + m57 + m58 = 1; s.t. st36: m10 + m31 + m51 + m55 + m59 + m60 + m61 = 1; s.t. st37: m11 + m32 + m52 + m56 + m59 + m62 + m63 = 1; s.t. st38: m12 + m33 + m53 + m57 + m60 + m62 + m64 = 1; s.t. st39: m13 + m34 + m54 + m58 + m61 + m63 + m64 = 1; s.t. st45: m14 + m35 + m50 + m65 + m66 + m67 + m68 = 1; s.t. st46: m15 + m36 + m51 + m65 + m69 + m70 + m71 = 1; s.t. st47: m16 + m37 + m52 + m66 + m69 + m72 + m73 = 1; s.t. st48: m17 + m38 + m53 + m67 + m70 + m72 + m74 = 1; s.t. st49: m18 + m39 + m54 + m68 + m71 + m73 + m74 = 1; s.t. st56: m19 + m40 + m55 + m65 + m75 + m76 + m77 = 1; s.t. st57: m20 + m41 + m56 + m66 + m75 + m78 + m79 = 1; s.t. st58: m21 + m42 + m57 + m67 + m76 + m78 + m80 = 1; s.t. st59: m22 + m43 + m58 + m68 + m77 + m79 + m80 = 1; s.t. st67: m23 + m44 + m59 + m69 + m75 + m81 + m82 = 1; s.t. st68: m24 + m45 + m60 + m70 + m76 + m81 + m83 = 1; s.t. st69: m25 + m46 + m61 + m71 + m77 + m82 + m83 = 1; s.t. st78: m26 + m47 + m62 + m72 + m78 + m81 + m84 = 1; s.t. st79: m27 + m48 + m63 + m73 + m79 + m82 + m84 = 1; s.t. st89: m28 + m49 + m64 + m74 + m80 + m83 + m84 = 1; s.t. pm1: m04 + m12 + m14 + m27 + m34 + m38 + m41 + m52 + m55 + m71 + m80 + m81 <= 11; s.t. pm2: m04 + m12 + m18 + m20 + m34 + m35 + m47 + m52 + m55 + m70 + m80 + m82 <= 11; s.t. pm3: m03 + m11 + m18 + m24 + m34 + m36 + m47 + m53 + m55 + m66 + m80 + m82 <= 11; s.t. pm4: m01 + m14 + m24 + m27 + m38 + m41 + m46 + m54 + m55 + m62 + m69 + m80 <= 11; s.t. pm5: m01 + m18 + m20 + m24 + m35 + m46 + m47 + m53 + m55 + m63 + m69 + m80 <= 11; s.t. pm6: m01 + m14 + m25 + m26 + m39 + m41 + m45 + m53 + m55 + m63 + m69 + m80 <= 11; s.t. pm7: m04 + m13 + m17 + m20 + m33 + m35 + m48 + m52 + m55 + m71 + m80 + m81 <= 11; s.t. pm8: m01 + m17 + m20 + m25 + m35 + m45 + m48 + m54 + m55 + m62 + m69 + m80 <= 11; s.t. pm9: m04 + m13 + m14 + m26 + m33 + m39 + m41 + m52 + m55 + m70 + m80 + m82 <= 11; s.t. pm10: m05 + m08 + m22 + m24 + m33 + m35 + m46 + m55 + m63 + m69 + m74 + m78 <= 11; s.t. pm11: m07 + m12 + m14 + m23 + m29 + m41 + m45 + m55 + m63 + m71 + m72 + m80 <= 11; s.t. pm12: m06 + m11 + m14 + m25 + m34 + m36 + m41 + m53 + m55 + m73 + m80 + m81 <= 11; s.t. pm13: m06 + m13 + m14 + m23 + m29 + m41 + m46 + m55 + m62 + m70 + m73 + m80 <= 11; s.t. pm14: m04 + m12 + m14 + m27 + m32 + m38 + m43 + m54 + m55 + m69 + m78 + m83 <= 11; s.t. pm15: m04 + m11 + m14 + m28 + m33 + m37 + m43 + m54 + m55 + m70 + m78 + m82 <= 11; s.t. pm16: m03 + m08 + m24 + m27 + m34 + m38 + m44 + m55 + m62 + m66 + m71 + m80 <= 11; s.t. pm17: m06 + m13 + m15 + m20 + m32 + m35 + m46 + m53 + m55 + m73 + m80 + m81 <= 11; s.t. pm18: m01 + m16 + m21 + m25 + m35 + m44 + m49 + m54 + m55 + m62 + m70 + m79 <= 11; s.t. pm19: m03 + m12 + m16 + m25 + m32 + m36 + m49 + m54 + m55 + m67 + m79 + m81 <= 11; s.t. pm20: m04 + m08 + m21 + m27 + m32 + m38 + m43 + m55 + m64 + m66 + m71 + m81 <= 11; s.t. pm21: m03 + m13 + m16 + m24 + m32 + m36 + m49 + m53 + m55 + m68 + m78 + m82 <= 11; s.t. pm22: m04 + m08 + m21 + m27 + m34 + m38 + m41 + m55 + m62 + m68 + m69 + m83 <= 11; s.t. pm23: m03 + m12 + m15 + m27 + m34 + m38 + m44 + m52 + m55 + m68 + m78 + m83 <= 11; s.t. pm24: m03 + m13 + m16 + m24 + m29 + m44 + m49 + m55 + m62 + m67 + m71 + m79 <= 11; s.t. pm25: m07 + m08 + m20 + m24 + m33 + m35 + m44 + m55 + m63 + m71 + m72 + m80 <= 11; s.t. pm26: m04 + m12 + m16 + m22 + m32 + m35 + m49 + m54 + m55 + m70 + m78 + m82 <= 11; s.t. pm27: m04 + m13 + m16 + m21 + m32 + m35 + m49 + m53 + m55 + m71 + m79 + m81 <= 11; s.t. pm28: m04 + m08 + m22 + m26 + m33 + m39 + m41 + m55 + m63 + m67 + m69 + m83 <= 11; s.t. pm29: m03 + m08 + m24 + m27 + m32 + m38 + m46 + m55 + m64 + m68 + m69 + m78 <= 11; s.t. pm30: m07 + m08 + m21 + m23 + m32 + m35 + m45 + m55 + m64 + m71 + m72 + m79 <= 11; s.t. pm31: m06 + m08 + m20 + m25 + m32 + m36 + m43 + m55 + m64 + m67 + m73 + m81 <= 11; s.t. pm32: m04 + m08 + m20 + m28 + m33 + m37 + m43 + m55 + m63 + m67 + m71 + m81 <= 11; s.t. pm33: m05 + m08 + m21 + m25 + m33 + m36 + m43 + m55 + m63 + m66 + m74 + m81 <= 11; s.t. pm34: m06 + m08 + m22 + m23 + m34 + m36 + m41 + m55 + m62 + m67 + m73 + m83 <= 11; s.t. pm35: m04 + m08 + m22 + m26 + m32 + m39 + m42 + m55 + m64 + m66 + m70 + m82 <= 11; s.t. pm36: m04 + m08 + m20 + m28 + m34 + m37 + m42 + m55 + m62 + m68 + m70 + m82 <= 11; s.t. pm37: m03 + m08 + m23 + m28 + m33 + m37 + m46 + m55 + m63 + m68 + m70 + m78 <= 11; s.t. pm38: m01 + m14 + m24 + m27 + m36 + m43 + m47 + m52 + m57 + m61 + m74 + m75 <= 11; s.t. pm39: m07 + m08 + m21 + m23 + m33 + m36 + m41 + m55 + m63 + m68 + m72 + m83 <= 11; s.t. pm40: m06 + m08 + m22 + m23 + m32 + m35 + m46 + m55 + m64 + m70 + m73 + m78 <= 11; s.t. pm41: m03 + m08 + m25 + m26 + m32 + m39 + m45 + m55 + m64 + m67 + m69 + m79 <= 11; s.t. pm42: m01 + m16 + m22 + m24 + m36 + m42 + m48 + m50 + m61 + m62 + m74 + m75 <= 11; s.t. pm43: m07 + m08 + m20 + m24 + m32 + m36 + m42 + m55 + m64 + m68 + m72 + m82 <= 11; s.t. pm44: m01 + m14 + m25 + m26 + m36 + m42 + m48 + m52 + m58 + m60 + m74 + m75 <= 11; s.t. pm45: m01 + m18 + m21 + m23 + m36 + m41 + m49 + m50 + m60 + m63 + m72 + m77 <= 11; s.t. pm46: m01 + m16 + m21 + m25 + m36 + m43 + m47 + m50 + m60 + m63 + m74 + m75 <= 11; s.t. pm47: m01 + m17 + m19 + m27 + m36 + m41 + m49 + m52 + m57 + m61 + m68 + m81 <= 11; s.t. pm48: m01 + m14 + m24 + m27 + m36 + m41 + m49 + m54 + m57 + m59 + m72 + m77 <= 11; s.t. pm49: m01 + m14 + m23 + m28 + m36 + m42 + m48 + m54 + m56 + m60 + m72 + m77 <= 11; s.t. pm50: m01 + m17 + m19 + m27 + m36 + m43 + m47 + m54 + m57 + m59 + m66 + m83 <= 11; s.t. pm51: m01 + m16 + m19 + m28 + m36 + m43 + m47 + m54 + m56 + m60 + m67 + m82 <= 11; s.t. pm52: m01 + m18 + m19 + m26 + m36 + m42 + m48 + m53 + m58 + m59 + m66 + m83 <= 11; s.t. pm53: m01 + m16 + m19 + m28 + m36 + m42 + m48 + m53 + m56 + m61 + m68 + m81 <= 11; s.t. pm54: m01 + m18 + m19 + m26 + m36 + m41 + m49 + m52 + m58 + m60 + m67 + m82 <= 11; s.t. pm55: m01 + m14 + m25 + m26 + m36 + m41 + m49 + m53 + m58 + m59 + m73 + m76 <= 11; s.t. pm56: m01 + m17 + m22 + m23 + m36 + m41 + m49 + m50 + m61 + m62 + m73 + m76 <= 11; s.t. pm57: m05 + m13 + m14 + m24 + m29 + m42 + m46 + m55 + m62 + m69 + m74 + m79 <= 11; s.t. pm58: m05 + m13 + m14 + m24 + m33 + m36 + m43 + m52 + m55 + m74 + m78 + m82 <= 11; s.t. pm59: m04 + m13 + m14 + m26 + m32 + m39 + m42 + m53 + m55 + m69 + m79 + m83 <= 11; s.t. pm60: m06 + m13 + m14 + m23 + m32 + m36 + m43 + m53 + m55 + m73 + m78 + m83 <= 11; s.t. pm61: m04 + m11 + m14 + m28 + m34 + m37 + m42 + m53 + m55 + m71 + m79 + m81 <= 11; s.t. pm62: m01 + m16 + m21 + m25 + m36 + m41 + m49 + m53 + m55 + m63 + m68 + m81 <= 11; s.t. pm63: m01 + m16 + m22 + m24 + m36 + m41 + m49 + m54 + m55 + m62 + m67 + m82 <= 11; s.t. pm64: m01 + m16 + m22 + m24 + m35 + m44 + m49 + m53 + m55 + m63 + m71 + m78 <= 11; s.t. pm65: m01 + m15 + m20 + m28 + m37 + m42 + m46 + m53 + m55 + m63 + m68 + m81 <= 11; s.t. pm66: m05 + m08 + m22 + m24 + m34 + m36 + m42 + m55 + m62 + m66 + m74 + m82 <= 11; s.t. pm67: m01 + m17 + m20 + m25 + m36 + m42 + m48 + m52 + m55 + m64 + m68 + m81 <= 11; s.t. pm68: m01 + m15 + m20 + m28 + m37 + m43 + m45 + m54 + m55 + m62 + m67 + m82 <= 11; s.t. pm69: m01 + m18 + m20 + m24 + m36 + m43 + m47 + m52 + m55 + m64 + m67 + m82 <= 11; s.t. pm70: m03 + m08 + m25 + m26 + m33 + m39 + m44 + m55 + m63 + m66 + m70 + m80 <= 11; s.t. pm71: m06 + m08 + m20 + m25 + m34 + m35 + m44 + m55 + m62 + m70 + m73 + m80 <= 11; s.t. pm72: m01 + m17 + m20 + m25 + m36 + m43 + m47 + m50 + m59 + m64 + m73 + m76 <= 11; s.t. pm73: m01 + m14 + m23 + m28 + m36 + m43 + m47 + m53 + m56 + m61 + m73 + m76 <= 11; s.t. pm74: m01 + m18 + m20 + m24 + m36 + m42 + m48 + m50 + m59 + m64 + m72 + m77 <= 11; s.t. pm75: m01 + m15 + m22 + m26 + m39 + m41 + m45 + m52 + m55 + m64 + m67 + m82 <= 11; s.t. pm76: m01 + m17 + m22 + m23 + m35 + m45 + m48 + m52 + m55 + m64 + m71 + m78 <= 11; s.t. pm77: m01 + m17 + m22 + m23 + m36 + m42 + m48 + m54 + m55 + m62 + m66 + m83 <= 11; s.t. pm78: m01 + m15 + m22 + m26 + m39 + m42 + m44 + m53 + m55 + m63 + m66 + m83 <= 11; s.t. pm79: m01 + m15 + m21 + m27 + m38 + m41 + m46 + m52 + m55 + m64 + m68 + m81 <= 11; s.t. pm80: m01 + m18 + m21 + m23 + m35 + m46 + m47 + m52 + m55 + m64 + m70 + m79 <= 11; s.t. pm81: m01 + m15 + m21 + m27 + m38 + m43 + m44 + m54 + m55 + m62 + m66 + m83 <= 11; s.t. pm82: m01 + m18 + m21 + m23 + m36 + m43 + m47 + m53 + m55 + m63 + m66 + m83 <= 11; s.t. pm83: m04 + m09 + m17 + m27 + m34 + m35 + m47 + m52 + m60 + m71 + m75 + m80 <= 11; s.t. pm84: m02 + m09 + m24 + m27 + m31 + m43 + m47 + m52 + m64 + m67 + m71 + m75 <= 11; s.t. pm85: m04 + m09 + m17 + m27 + m29 + m43 + m47 + m59 + m64 + m66 + m71 + m76 <= 11; s.t. pm86: m02 + m09 + m24 + m27 + m34 + m40 + m47 + m53 + m59 + m66 + m71 + m80 <= 11; s.t. pm87: m04 + m09 + m17 + m27 + m33 + m39 + m41 + m52 + m61 + m65 + m80 + m81 <= 11; s.t. pm88: m02 + m09 + m24 + m27 + m33 + m41 + m46 + m54 + m59 + m65 + m72 + m80 <= 11; s.t. pm89: m04 + m09 + m17 + m27 + m29 + m41 + m49 + m61 + m62 + m68 + m69 + m76 <= 11; s.t. pm90: m06 + m09 + m15 + m27 + m31 + m39 + m41 + m52 + m64 + m67 + m77 + m81 <= 11; s.t. pm91: m06 + m09 + m15 + m27 + m29 + m41 + m46 + m59 + m64 + m68 + m72 + m76 <= 11; s.t. pm92: m02 + m09 + m24 + m27 + m31 + m41 + m49 + m54 + m62 + m67 + m69 + m77 <= 11; s.t. pm93: m04 + m09 + m17 + m27 + m34 + m37 + m42 + m51 + m62 + m68 + m75 + m83 <= 11; s.t. pm94: m06 + m09 + m15 + m27 + m34 + m37 + m40 + m53 + m59 + m68 + m78 + m83 <= 11; s.t. pm95: m02 + m09 + m24 + m27 + m32 + m42 + m46 + m51 + m64 + m68 + m72 + m75 <= 11; s.t. pm96: m04 + m09 + m17 + m27 + m32 + m39 + m42 + m51 + m64 + m66 + m77 + m81 <= 11; s.t. pm97: m02 + m09 + m24 + m27 + m34 + m42 + m44 + m51 + m62 + m66 + m74 + m77 <= 11; s.t. pm98: m06 + m09 + m15 + m27 + m34 + m35 + m44 + m52 + m60 + m74 + m77 + m78 <= 11; s.t. pm99: m06 + m09 + m15 + m27 + m32 + m39 + m40 + m53 + m61 + m66 + m80 + m81 <= 11; s.t. pm100: m06 + m09 + m15 + m27 + m29 + m43 + m44 + m61 + m62 + m66 + m74 + m76 <= 11; s.t. pm101: m02 + m09 + m24 + m27 + m33 + m43 + m44 + m52 + m61 + m65 + m74 + m78 <= 11; s.t. pm102: m07 + m11 + m14 + m24 + m29 + m42 + m44 + m55 + m64 + m71 + m72 + m79 <= 11; s.t. pm103: m01 + m14 + m25 + m26 + m39 + m42 + m44 + m52 + m55 + m64 + m70 + m79 <= 11; s.t. pm104: m01 + m14 + m23 + m28 + m37 + m42 + m46 + m54 + m55 + m62 + m70 + m79 <= 11; s.t. pm105: m01 + m14 + m24 + m27 + m38 + m43 + m44 + m52 + m55 + m64 + m71 + m78 <= 11; s.t. pm106: m01 + m14 + m23 + m28 + m37 + m43 + m45 + m53 + m55 + m63 + m71 + m78 <= 11; s.t. pm107: m03 + m12 + m16 + m25 + m29 + m44 + m49 + m55 + m63 + m68 + m70 + m78 <= 11; s.t. pm108: m04 + m13 + m16 + m21 + m29 + m41 + m49 + m55 + m62 + m68 + m70 + m82 <= 11; s.t. pm109: m04 + m12 + m16 + m22 + m29 + m41 + m49 + m55 + m63 + m67 + m71 + m81 <= 11; s.t. pm110: m05 + m08 + m21 + m25 + m34 + m35 + m45 + m55 + m62 + m69 + m74 + m79 <= 11; s.t. pm111: m03 + m08 + m23 + m28 + m34 + m37 + m45 + m55 + m62 + m67 + m71 + m79 <= 11; s.t. pm112: m04 + m12 + m14 + m27 + m30 + m39 + m47 + m52 + m61 + m70 + m75 + m80 <= 11; s.t. pm113: m02 + m12 + m19 + m27 + m30 + m46 + m47 + m54 + m59 + m66 + m70 + m80 <= 11; s.t. pm114: m02 + m12 + m19 + m27 + m30 + m44 + m49 + m52 + m61 + m68 + m70 + m78 <= 11; s.t. pm115: m04 + m12 + m14 + m27 + m30 + m37 + m49 + m54 + m59 + m70 + m77 + m78 <= 11; s.t. pm116: m04 + m08 + m21 + m27 + m30 + m39 + m47 + m59 + m64 + m66 + m70 + m77 <= 11; s.t. pm117: m06 + m10 + m14 + m27 + m30 + m37 + m46 + m54 + m62 + m70 + m75 + m80 <= 11; s.t. pm118: m04 + m08 + m21 + m27 + m30 + m37 + m49 + m61 + m62 + m68 + m70 + m75 <= 11; s.t. pm119: m06 + m08 + m19 + m27 + m30 + m37 + m46 + m59 + m64 + m68 + m70 + m78 <= 11; s.t. pm120: m02 + m10 + m21 + m27 + m30 + m46 + m47 + m52 + m64 + m68 + m70 + m75 <= 11; s.t. pm121: m06 + m10 + m14 + m27 + m30 + m39 + m44 + m52 + m64 + m70 + m77 + m78 <= 11; s.t. pm122: m06 + m08 + m19 + m27 + m30 + m39 + m44 + m61 + m62 + m66 + m70 + m80 <= 11; s.t. pm123: m02 + m10 + m21 + m27 + m30 + m44 + m49 + m54 + m62 + m66 + m70 + m77 <= 11; s.t. pm124: m02 + m09 + m24 + m27 + m32 + m40 + m49 + m53 + m61 + m68 + m69 + m78 <= 11; s.t. pm125: m06 + m10 + m18 + m20 + m29 + m43 + m44 + m57 + m63 + m65 + m72 + m83 <= 11; s.t. pm126: m06 + m10 + m18 + m20 + m29 + m40 + m48 + m58 + m62 + m67 + m69 + m83 <= 11; s.t. pm127: m06 + m10 + m16 + m22 + m29 + m40 + m48 + m56 + m64 + m67 + m71 + m81 <= 11; s.t. pm128: m06 + m10 + m16 + m22 + m29 + m41 + m46 + m57 + m63 + m65 + m74 + m81 <= 11; s.t. pm129: m06 + m09 + m16 + m25 + m29 + m43 + m44 + m60 + m63 + m65 + m74 + m78 <= 11; s.t. pm130: m06 + m13 + m14 + m23 + m29 + m40 + m48 + m56 + m60 + m71 + m72 + m80 <= 11; s.t. pm131: m04 + m09 + m17 + m27 + m32 + m35 + m49 + m54 + m60 + m69 + m77 + m78 <= 11; s.t. pm132: m06 + m09 + m15 + m27 + m32 + m35 + m46 + m54 + m60 + m72 + m75 + m80 <= 11; s.t. pm133: m04 + m09 + m17 + m27 + m33 + m37 + m43 + m54 + m59 + m65 + m78 + m83 <= 11; s.t. pm134: m06 + m09 + m15 + m27 + m31 + m37 + m43 + m54 + m62 + m67 + m75 + m83 <= 11; s.t. pm135: m06 + m13 + m16 + m19 + m29 + m43 + m44 + m56 + m60 + m67 + m71 + m84 <= 11; s.t. pm136: m06 + m09 + m18 + m23 + m29 + m40 + m48 + m61 + m62 + m66 + m70 + m80 <= 11; s.t. pm137: m06 + m11 + m18 + m19 + m29 + m43 + m44 + m57 + m61 + m66 + m70 + m84 <= 11; s.t. pm138: m06 + m09 + m16 + m25 + m29 + m40 + m48 + m59 + m64 + m68 + m70 + m78 <= 11; s.t. pm139: m06 + m09 + m18 + m23 + m29 + m41 + m46 + m60 + m63 + m65 + m72 + m80 <= 11; s.t. pm140: m06 + m11 + m15 + m22 + m29 + m40 + m48 + m57 + m61 + m66 + m74 + m81 <= 11; s.t. pm141: m06 + m11 + m14 + m25 + m29 + m40 + m48 + m58 + m60 + m69 + m74 + m78 <= 11; s.t. pm142: m06 + m13 + m15 + m20 + m29 + m40 + m48 + m57 + m59 + m68 + m72 + m83 <= 11; s.t. pm143: m06 + m13 + m16 + m19 + m29 + m41 + m46 + m57 + m59 + m68 + m70 + m84 <= 11; s.t. pm144: m06 + m11 + m18 + m19 + m29 + m41 + m46 + m58 + m60 + m67 + m69 + m84 <= 11; s.t. pm145: m07 + m10 + m16 + m21 + m29 + m40 + m47 + m56 + m64 + m68 + m70 + m82 <= 11; s.t. pm146: m07 + m10 + m17 + m20 + m29 + m40 + m47 + m57 + m63 + m68 + m69 + m83 <= 11; s.t. pm147: m03 + m10 + m16 + m28 + m29 + m46 + m47 + m57 + m63 + m68 + m70 + m75 <= 11; s.t. pm148: m03 + m10 + m18 + m26 + m29 + m44 + m49 + m57 + m63 + m66 + m70 + m77 <= 11; s.t. pm149: m03 + m10 + m18 + m26 + m29 + m45 + m48 + m56 + m64 + m67 + m69 + m77 <= 11; s.t. pm150: m03 + m10 + m16 + m28 + m29 + m45 + m48 + m58 + m62 + m67 + m71 + m75 <= 11; s.t. pm151: m05 + m10 + m17 + m22 + m29 + m42 + m46 + m56 + m64 + m65 + m73 + m81 <= 11; s.t. pm152: m07 + m10 + m14 + m26 + m29 + m42 + m44 + m56 + m64 + m70 + m73 + m77 <= 11; s.t. pm153: m07 + m10 + m17 + m20 + m29 + m42 + m44 + m58 + m62 + m65 + m73 + m83 <= 11; s.t. pm154: m05 + m10 + m14 + m28 + m29 + m42 + m46 + m58 + m62 + m70 + m73 + m75 <= 11; s.t. pm155: m05 + m10 + m18 + m21 + m29 + m43 + m45 + m56 + m64 + m65 + m72 + m82 <= 11; s.t. pm156: m07 + m10 + m16 + m21 + m29 + m41 + m45 + m58 + m62 + m65 + m74 + m82 <= 11; s.t. pm157: m05 + m10 + m14 + m28 + m29 + m43 + m45 + m57 + m63 + m71 + m72 + m75 <= 11; s.t. pm158: m07 + m10 + m14 + m26 + m29 + m41 + m45 + m57 + m63 + m69 + m74 + m77 <= 11; s.t. pm159: m05 + m13 + m17 + m19 + m29 + m42 + m46 + m56 + m60 + m68 + m69 + m84 <= 11; s.t. pm160: m05 + m13 + m15 + m21 + m29 + m40 + m49 + m56 + m60 + m68 + m72 + m82 <= 11; s.t. pm161: m05 + m12 + m15 + m22 + m29 + m40 + m49 + m56 + m61 + m67 + m73 + m81 <= 11; s.t. pm162: m05 + m12 + m18 + m19 + m29 + m43 + m45 + m56 + m61 + m67 + m69 + m84 <= 11; s.t. pm163: m05 + m09 + m15 + m28 + m29 + m42 + m46 + m60 + m63 + m68 + m72 + m75 <= 11; s.t. pm164: m03 + m11 + m15 + m28 + m29 + m46 + m47 + m58 + m60 + m67 + m73 + m75 <= 11; s.t. pm165: m03 + m11 + m15 + m28 + m29 + m45 + m48 + m57 + m61 + m68 + m72 + m75 <= 11; s.t. pm166: m04 + m11 + m14 + m28 + m29 + m42 + m48 + m58 + m60 + m71 + m72 + m75 <= 11; s.t. pm167: m04 + m09 + m16 + m28 + m29 + m43 + m47 + m60 + m63 + m67 + m71 + m75 <= 11; s.t. pm168: m05 + m09 + m15 + m28 + m29 + m43 + m45 + m61 + m62 + m67 + m73 + m75 <= 11; s.t. pm169: m04 + m09 + m16 + m28 + m29 + m42 + m48 + m61 + m62 + m68 + m70 + m75 <= 11; s.t. pm170: m04 + m11 + m14 + m28 + m29 + m43 + m47 + m57 + m61 + m70 + m73 + m75 <= 11; s.t. pm171: m03 + m13 + m15 + m26 + m29 + m44 + m49 + m56 + m60 + m67 + m73 + m77 <= 11; s.t. pm172: m04 + m13 + m14 + m26 + m29 + m42 + m48 + m56 + m60 + m69 + m74 + m77 <= 11; s.t. pm173: m07 + m11 + m17 + m19 + m29 + m42 + m44 + m58 + m60 + m66 + m71 + m84 <= 11; s.t. pm174: m07 + m09 + m15 + m26 + m29 + m42 + m44 + m60 + m63 + m66 + m74 + m77 <= 11; s.t. pm175: m03 + m11 + m17 + m25 + m29 + m44 + m49 + m58 + m60 + m65 + m73 + m78 <= 11; s.t. pm176: m05 + m09 + m17 + m25 + m29 + m40 + m49 + m60 + m63 + m68 + m69 + m78 <= 11; s.t. pm177: m07 + m11 + m15 + m21 + m29 + m40 + m47 + m58 + m60 + m66 + m74 + m82 <= 11; s.t. pm178: m07 + m09 + m17 + m23 + m29 + m40 + m47 + m60 + m63 + m66 + m71 + m80 <= 11; s.t. pm179: m04 + m11 + m18 + m21 + m29 + m41 + m49 + m58 + m60 + m65 + m72 + m82 <= 11; s.t. pm180: m04 + m09 + m18 + m26 + m29 + m41 + m49 + m60 + m63 + m67 + m69 + m77 <= 11; s.t. pm181: m05 + m10 + m18 + m21 + m29 + m40 + m49 + m58 + m62 + m66 + m70 + m82 <= 11; s.t. pm182: m05 + m10 + m17 + m22 + m29 + m40 + m49 + m57 + m63 + m66 + m71 + m81 <= 11; s.t. pm183: m05 + m12 + m14 + m25 + m29 + m43 + m45 + m55 + m63 + m69 + m74 + m78 <= 11; s.t. pm184: m05 + m12 + m14 + m25 + m34 + m36 + m42 + m52 + m55 + m74 + m79 + m81 <= 11; s.t. pm185: m07 + m12 + m14 + m23 + m32 + m36 + m42 + m54 + m55 + m72 + m79 + m83 <= 11; s.t. pm186: m03 + m12 + m15 + m27 + m32 + m38 + m46 + m54 + m55 + m66 + m80 + m81 <= 11; s.t. pm187: m06 + m11 + m14 + m25 + m29 + m43 + m44 + m55 + m64 + m70 + m73 + m78 <= 11; s.t. pm188: m07 + m12 + m15 + m20 + m32 + m35 + m45 + m54 + m55 + m72 + m80 + m82 <= 11; s.t. pm189: m03 + m13 + m15 + m26 + m32 + m39 + m45 + m53 + m55 + m66 + m80 + m82 <= 11; s.t. pm190: m05 + m13 + m17 + m19 + m29 + m43 + m45 + m57 + m59 + m66 + m71 + m84 <= 11; s.t. pm191: m05 + m09 + m17 + m25 + m29 + m43 + m45 + m59 + m64 + m65 + m73 + m78 <= 11; s.t. pm192: m07 + m09 + m15 + m26 + m29 + m41 + m45 + m59 + m64 + m67 + m73 + m77 <= 11; s.t. pm193: m05 + m13 + m14 + m24 + m29 + m40 + m49 + m57 + m59 + m71 + m72 + m79 <= 11; s.t. pm194: m03 + m13 + m16 + m24 + m29 + m46 + m47 + m57 + m59 + m65 + m74 + m79 <= 11; s.t. pm195: m04 + m13 + m17 + m20 + m29 + m43 + m47 + m57 + m59 + m65 + m73 + m83 <= 11; s.t. pm196: m05 + m09 + m18 + m24 + m29 + m42 + m46 + m59 + m64 + m65 + m72 + m79 <= 11; s.t. pm197: m05 + m09 + m18 + m24 + m29 + m40 + m49 + m61 + m62 + m67 + m69 + m79 <= 11; s.t. pm198: m05 + m12 + m14 + m25 + m29 + m40 + m49 + m58 + m59 + m70 + m73 + m78 <= 11; s.t. pm199: m07 + m12 + m15 + m20 + m29 + m40 + m47 + m58 + m59 + m67 + m73 + m83 <= 11; s.t. pm200: m07 + m09 + m17 + m23 + m29 + m41 + m45 + m61 + m62 + m65 + m73 + m80 <= 11; s.t. pm201: m04 + m13 + m14 + m26 + m29 + m41 + m49 + m57 + m59 + m70 + m73 + m77 <= 11; s.t. pm202: m04 + m11 + m17 + m22 + m29 + m41 + m49 + m57 + m61 + m65 + m73 + m81 <= 11; s.t. pm203: m03 + m13 + m15 + m26 + m29 + m45 + m48 + m57 + m59 + m66 + m74 + m77 <= 11; s.t. pm204: m05 + m12 + m18 + m19 + m29 + m42 + m46 + m58 + m59 + m66 + m70 + m84 <= 11; s.t. pm205: m07 + m09 + m16 + m24 + m29 + m40 + m47 + m59 + m64 + m67 + m71 + m79 <= 11; s.t. pm206: m07 + m11 + m14 + m24 + m29 + m40 + m47 + m57 + m61 + m69 + m74 + m79 <= 11; s.t. pm207: m07 + m09 + m16 + m24 + m29 + m42 + m44 + m61 + m62 + m65 + m74 + m79 <= 11; s.t. pm208: m03 + m11 + m18 + m24 + m29 + m44 + m49 + m57 + m61 + m65 + m72 + m79 <= 11; s.t. pm209: m07 + m11 + m17 + m19 + m29 + m41 + m45 + m57 + m61 + m68 + m69 + m84 <= 11; s.t. pm210: m03 + m13 + m17 + m23 + m29 + m45 + m48 + m55 + m62 + m66 + m71 + m80 <= 11; s.t. pm211: m03 + m12 + m18 + m23 + m29 + m46 + m47 + m55 + m63 + m66 + m70 + m80 <= 11; s.t. pm212: m03 + m11 + m17 + m25 + m33 + m36 + m48 + m54 + m55 + m66 + m80 + m81 <= 11; s.t. pm213: m04 + m12 + m18 + m20 + m29 + m42 + m48 + m58 + m59 + m65 + m72 + m83 <= 11; s.t. pm214: m02 + m13 + m20 + m24 + m33 + m43 + m44 + m52 + m55 + m67 + m71 + m84 <= 11; s.t. pm215: m06 + m13 + m15 + m20 + m29 + m43 + m44 + m55 + m62 + m67 + m73 + m83 <= 11; s.t. pm216: m06 + m11 + m15 + m22 + m29 + m41 + m46 + m55 + m64 + m67 + m73 + m81 <= 11; s.t. pm217: m03 + m11 + m18 + m24 + m29 + m46 + m47 + m55 + m64 + m67 + m69 + m79 <= 11; s.t. pm218: m04 + m12 + m18 + m20 + m29 + m43 + m47 + m55 + m63 + m67 + m69 + m83 <= 11; s.t. pm219: m02 + m12 + m22 + m23 + m34 + m41 + m45 + m52 + m55 + m67 + m71 + m84 <= 11; s.t. pm220: m02 + m12 + m20 + m25 + m32 + m43 + m45 + m54 + m55 + m67 + m69 + m84 <= 11; s.t. pm221: m02 + m11 + m22 + m24 + m33 + m41 + m46 + m54 + m55 + m67 + m69 + m84 <= 11; s.t. pm222: m03 + m13 + m15 + m26 + m33 + m39 + m44 + m52 + m55 + m67 + m79 + m83 <= 11; s.t. pm223: m03 + m11 + m15 + m28 + m33 + m37 + m46 + m54 + m55 + m67 + m79 + m81 <= 11; s.t. pm224: m03 + m12 + m18 + m23 + m34 + m36 + m47 + m52 + m55 + m67 + m79 + m83 <= 11; s.t. pm225: m03 + m10 + m17 + m27 + m34 + m36 + m47 + m52 + m57 + m68 + m75 + m83 <= 11; s.t. pm226: m03 + m10 + m17 + m27 + m29 + m46 + m47 + m56 + m64 + m68 + m69 + m76 <= 11; s.t. pm227: m03 + m12 + m15 + m27 + m29 + m46 + m47 + m58 + m59 + m66 + m74 + m76 <= 11; s.t. pm228: m03 + m08 + m24 + m27 + m34 + m36 + m47 + m57 + m59 + m66 + m74 + m77 <= 11; s.t. pm229: m03 + m08 + m24 + m27 + m31 + m39 + m47 + m56 + m64 + m67 + m69 + m77 <= 11; s.t. pm230: m03 + m12 + m15 + m27 + m31 + m39 + m47 + m52 + m58 + m67 + m75 + m83 <= 11; s.t. pm231: m04 + m08 + m21 + m27 + m34 + m35 + m47 + m56 + m60 + m69 + m74 + m77 <= 11; s.t. pm232: m04 + m12 + m14 + m27 + m29 + m43 + m47 + m56 + m61 + m69 + m74 + m76 <= 11; s.t. pm233: m02 + m12 + m19 + m27 + m31 + m43 + m47 + m54 + m56 + m67 + m69 + m83 <= 11; s.t. pm234: m02 + m10 + m21 + m27 + m34 + m40 + m47 + m53 + m56 + m68 + m69 + m83 <= 11; s.t. pm235: m03 + m08 + m24 + m27 + m31 + m37 + m49 + m58 + m62 + m67 + m71 + m75 <= 11; s.t. pm236: m03 + m08 + m24 + m27 + m33 + m37 + m46 + m58 + m59 + m65 + m74 + m78 <= 11; s.t. pm237: m03 + m10 + m17 + m27 + m34 + m37 + m45 + m50 + m62 + m71 + m75 + m80 <= 11; s.t. pm238: m03 + m10 + m17 + m27 + m32 + m36 + m49 + m54 + m57 + m66 + m77 + m81 <= 11; s.t. pm239: m03 + m10 + m17 + m27 + m33 + m37 + m46 + m54 + m56 + m65 + m80 + m81 <= 11; s.t. pm240: m03 + m10 + m17 + m27 + m32 + m39 + m45 + m50 + m64 + m69 + m77 + m78 <= 11; s.t. pm241: m03 + m08 + m24 + m27 + m32 + m36 + m49 + m57 + m61 + m68 + m72 + m75 <= 11; s.t. pm242: m03 + m12 + m15 + m27 + m34 + m37 + m45 + m50 + m59 + m74 + m77 + m78 <= 11; s.t. pm243: m03 + m12 + m15 + m27 + m31 + m37 + m49 + m54 + m56 + m67 + m77 + m81 <= 11; s.t. pm244: m03 + m10 + m17 + m27 + m29 + m44 + m49 + m58 + m62 + m66 + m71 + m76 <= 11; s.t. pm245: m03 + m12 + m15 + m27 + m29 + m44 + m49 + m56 + m61 + m68 + m72 + m76 <= 11; s.t. pm246: m03 + m10 + m17 + m27 + m33 + m39 + m44 + m52 + m58 + m65 + m78 + m83 <= 11; s.t. pm247: m06 + m10 + m14 + m27 + m34 + m36 + m41 + m52 + m57 + m74 + m77 + m81 <= 11; s.t. pm248: m06 + m10 + m14 + m27 + m29 + m41 + m46 + m58 + m62 + m69 + m74 + m76 <= 11; s.t. pm249: m06 + m08 + m19 + m27 + m31 + m39 + m41 + m58 + m62 + m67 + m69 + m83 <= 11; s.t. pm250: m06 + m08 + m19 + m27 + m34 + m36 + m41 + m57 + m59 + m68 + m72 + m83 <= 11; s.t. pm251: m03 + m12 + m15 + m27 + m32 + m39 + m45 + m50 + m61 + m72 + m75 + m80 <= 11; s.t. pm252: m06 + m10 + m14 + m27 + m32 + m36 + m43 + m54 + m57 + m72 + m75 + m83 <= 11; s.t. pm253: m06 + m08 + m19 + m27 + m32 + m36 + m43 + m57 + m61 + m66 + m74 + m81 <= 11; s.t. pm254: m06 + m08 + m19 + m27 + m32 + m35 + m46 + m58 + m60 + m69 + m74 + m78 <= 11; s.t. pm255: m06 + m10 + m14 + m27 + m32 + m39 + m40 + m53 + m58 + m69 + m78 + m83 <= 11; s.t. pm256: m06 + m10 + m14 + m27 + m34 + m37 + m40 + m53 + m56 + m71 + m80 + m81 <= 11; s.t. pm257: m06 + m08 + m19 + m27 + m34 + m35 + m44 + m56 + m60 + m71 + m72 + m80 <= 11; s.t. pm258: m03 + m08 + m24 + m27 + m33 + m39 + m44 + m56 + m61 + m65 + m72 + m80 <= 11; s.t. pm259: m05 + m08 + m19 + m28 + m31 + m38 + m43 + m57 + m63 + m66 + m71 + m81 <= 11; s.t. pm260: m05 + m08 + m22 + m24 + m34 + m38 + m40 + m57 + m59 + m66 + m71 + m84 <= 11; s.t. pm261: m05 + m12 + m18 + m19 + m31 + m38 + m43 + m50 + m63 + m69 + m78 + m83 <= 11; s.t. pm262: m05 + m13 + m14 + m24 + m31 + m38 + m43 + m52 + m57 + m71 + m75 + m84 <= 11; s.t. pm263: m05 + m10 + m14 + m28 + m30 + m38 + m46 + m54 + m62 + m69 + m76 + m79 <= 11; s.t. pm264: m05 + m09 + m15 + m28 + m31 + m38 + m43 + m54 + m62 + m66 + m76 + m82 <= 11; s.t. pm265: m05 + m12 + m15 + m22 + m30 + m38 + m46 + m54 + m59 + m66 + m76 + m84 <= 11; s.t. pm266: m05 + m12 + m14 + m25 + m31 + m38 + m43 + m54 + m56 + m69 + m76 + m84 <= 11; s.t. pm267: m05 + m08 + m21 + m25 + m34 + m38 + m40 + m56 + m60 + m68 + m69 + m84 <= 11; s.t. pm268: m05 + m10 + m18 + m21 + m34 + m38 + m40 + m50 + m62 + m69 + m79 + m83 <= 11; s.t. pm269: m05 + m13 + m15 + m21 + m30 + m38 + m46 + m52 + m60 + m68 + m75 + m84 <= 11; s.t. pm270: m05 + m10 + m14 + m28 + m34 + m38 + m40 + m52 + m57 + m71 + m79 + m81 <= 11; s.t. pm271: m05 + m08 + m21 + m25 + m31 + m38 + m43 + m56 + m64 + m65 + m73 + m81 <= 11; s.t. pm272: m05 + m13 + m15 + m21 + m31 + m38 + m43 + m50 + m62 + m73 + m75 + m83 <= 11; s.t. pm273: m05 + m08 + m22 + m24 + m30 + m38 + m46 + m59 + m64 + m65 + m73 + m78 <= 11; s.t. pm274: m05 + m12 + m15 + m22 + m34 + m38 + m40 + m50 + m59 + m73 + m78 + m83 <= 11; s.t. pm275: m03 + m12 + m16 + m25 + m31 + m38 + m48 + m54 + m56 + m65 + m80 + m81 <= 11; s.t. pm276: m03 + m10 + m16 + m28 + m32 + m38 + m46 + m54 + m57 + m65 + m79 + m81 <= 11; s.t. pm277: m03 + m10 + m16 + m28 + m34 + m38 + m44 + m50 + m62 + m71 + m76 + m79 <= 11; s.t. pm278: m03 + m13 + m16 + m24 + m31 + m38 + m48 + m50 + m62 + m71 + m75 + m80 <= 11; s.t. pm279: m03 + m13 + m15 + m26 + m31 + m38 + m48 + m52 + m57 + m68 + m75 + m83 <= 11; s.t. pm280: m03 + m08 + m25 + m26 + m31 + m38 + m48 + m56 + m64 + m68 + m69 + m76 <= 11; s.t. pm281: m03 + m11 + m15 + m28 + m34 + m38 + m44 + m50 + m60 + m73 + m77 + m78 <= 11; s.t. pm282: m03 + m13 + m15 + m26 + m32 + m38 + m46 + m50 + m60 + m73 + m75 + m80 <= 11; s.t. pm283: m03 + m11 + m15 + m28 + m31 + m38 + m48 + m54 + m57 + m66 + m77 + m81 <= 11; s.t. pm284: m03 + m08 + m23 + m28 + m32 + m38 + m46 + m58 + m60 + m65 + m73 + m78 <= 11; s.t. pm285: m03 + m10 + m18 + m26 + m34 + m38 + m44 + m52 + m57 + m65 + m79 + m83 <= 11; s.t. pm286: m03 + m08 + m25 + m26 + m34 + m38 + m44 + m56 + m60 + m65 + m73 + m80 <= 11; s.t. pm287: m03 + m12 + m18 + m23 + m31 + m38 + m48 + m52 + m58 + m65 + m78 + m83 <= 11; s.t. pm288: m03 + m10 + m18 + m26 + m32 + m38 + m46 + m50 + m64 + m69 + m76 + m79 <= 11; s.t. pm289: m03 + m08 + m23 + m28 + m31 + m38 + m48 + m58 + m62 + m66 + m71 + m76 <= 11; s.t. pm290: m03 + m11 + m18 + m24 + m31 + m38 + m48 + m50 + m64 + m69 + m77 + m78 <= 11; s.t. pm291: m07 + m10 + m16 + m21 + m32 + m38 + m40 + m50 + m64 + m71 + m79 + m81 <= 11; s.t. pm292: m07 + m10 + m16 + m21 + m30 + m38 + m44 + m54 + m62 + m65 + m79 + m83 <= 11; s.t. pm293: m07 + m10 + m14 + m26 + m32 + m38 + m40 + m54 + m57 + m69 + m79 + m83 <= 11; s.t. pm294: m07 + m10 + m14 + m26 + m30 + m38 + m44 + m52 + m64 + m71 + m76 + m79 <= 11; s.t. pm295: m04 + m11 + m14 + m28 + m33 + m39 + m41 + m51 + m58 + m72 + m76 + m82 <= 11; s.t. pm296: m04 + m11 + m14 + m28 + m34 + m38 + m41 + m51 + m57 + m73 + m77 + m81 <= 11; s.t. pm297: m07 + m11 + m14 + m24 + m33 + m37 + m40 + m51 + m58 + m74 + m78 + m82 <= 11; s.t. pm298: m07 + m11 + m14 + m24 + m30 + m38 + m44 + m51 + m64 + m73 + m77 + m78 <= 11; s.t. pm299: m06 + m11 + m14 + m25 + m34 + m37 + m40 + m51 + m57 + m74 + m79 + m81 <= 11; s.t. pm300: m06 + m11 + m14 + m25 + m30 + m39 + m44 + m51 + m64 + m72 + m76 + m79 <= 11; s.t. pm301: m05 + m12 + m14 + m25 + m30 + m39 + m45 + m51 + m63 + m72 + m75 + m80 <= 11; s.t. pm302: m05 + m13 + m14 + m24 + m33 + m39 + m40 + m51 + m56 + m72 + m80 + m82 <= 11; s.t. pm303: m06 + m13 + m14 + m23 + m32 + m39 + m40 + m51 + m57 + m72 + m79 + m83 <= 11; s.t. pm304: m06 + m13 + m14 + m23 + m30 + m37 + m46 + m51 + m62 + m74 + m76 + m79 <= 11; s.t. pm305: m07 + m12 + m14 + m23 + m30 + m37 + m45 + m51 + m63 + m74 + m77 + m78 <= 11; s.t. pm306: m05 + m12 + m14 + m25 + m34 + m38 + m40 + m51 + m56 + m73 + m80 + m81 <= 11; s.t. pm307: m05 + m13 + m14 + m24 + m30 + m38 + m46 + m51 + m62 + m73 + m75 + m80 <= 11; s.t. pm308: m07 + m12 + m14 + m23 + m32 + m38 + m40 + m51 + m58 + m73 + m78 + m83 <= 11; s.t. pm309: m04 + m13 + m14 + m26 + m32 + m38 + m43 + m51 + m57 + m73 + m75 + m83 <= 11; s.t. pm310: m04 + m13 + m14 + m26 + m33 + m37 + m43 + m51 + m56 + m74 + m76 + m82 <= 11; s.t. pm311: m06 + m13 + m16 + m19 + m32 + m35 + m46 + m51 + m57 + m74 + m79 + m81 <= 11; s.t. pm312: m04 + m13 + m17 + m20 + m32 + m35 + m49 + m51 + m57 + m73 + m77 + m81 <= 11; s.t. pm313: m04 + m11 + m18 + m21 + m33 + m35 + m48 + m51 + m58 + m72 + m75 + m83 <= 11; s.t. pm314: m04 + m13 + m16 + m21 + m33 + m35 + m48 + m51 + m56 + m74 + m77 + m81 <= 11; s.t. pm315: m04 + m09 + m18 + m26 + m33 + m37 + m43 + m51 + m63 + m67 + m75 + m83 <= 11; s.t. pm316: m04 + m09 + m16 + m28 + m33 + m39 + m41 + m51 + m63 + m67 + m77 + m81 <= 11; s.t. pm317: m04 + m09 + m18 + m26 + m32 + m38 + m43 + m51 + m64 + m66 + m76 + m82 <= 11; s.t. pm318: m04 + m12 + m18 + m20 + m32 + m35 + m49 + m51 + m58 + m72 + m76 + m82 <= 11; s.t. pm319: m04 + m11 + m18 + m21 + m30 + m38 + m48 + m51 + m64 + m66 + m77 + m81 <= 11; s.t. pm320: m04 + m11 + m17 + m22 + m30 + m39 + m47 + m51 + m64 + m66 + m76 + m82 <= 11; s.t. pm321: m03 + m13 + m16 + m24 + m32 + m38 + m46 + m51 + m57 + m68 + m75 + m84 <= 11; s.t. pm322: m04 + m12 + m16 + m22 + m34 + m35 + m47 + m51 + m56 + m74 + m76 + m82 <= 11; s.t. pm323: m04 + m13 + m17 + m20 + m30 + m37 + m49 + m51 + m62 + m68 + m76 + m82 <= 11; s.t. pm324: m04 + m12 + m18 + m20 + m30 + m37 + m49 + m51 + m63 + m67 + m77 + m81 <= 11; s.t. pm325: m04 + m13 + m16 + m21 + m30 + m38 + m48 + m51 + m62 + m68 + m75 + m83 <= 11; s.t. pm326: m04 + m12 + m16 + m22 + m30 + m39 + m47 + m51 + m63 + m67 + m75 + m83 <= 11; s.t. pm327: m04 + m09 + m16 + m28 + m34 + m38 + m41 + m51 + m62 + m68 + m76 + m82 <= 11; s.t. pm328: m03 + m11 + m17 + m25 + m34 + m37 + m45 + m51 + m57 + m68 + m75 + m84 <= 11; s.t. pm329: m03 + m11 + m18 + m24 + m34 + m38 + m44 + m51 + m57 + m66 + m77 + m84 <= 11; s.t. pm330: m04 + m11 + m17 + m22 + m34 + m35 + m47 + m51 + m57 + m73 + m75 + m83 <= 11; s.t. pm331: m02 + m11 + m22 + m24 + m30 + m46 + m47 + m51 + m64 + m67 + m73 + m75 <= 11; s.t. pm332: m02 + m11 + m19 + m28 + m33 + m41 + m46 + m51 + m58 + m67 + m73 + m81 <= 11; s.t. pm333: m02 + m11 + m21 + m25 + m33 + m40 + m48 + m51 + m58 + m66 + m74 + m81 <= 11; s.t. pm334: m02 + m11 + m21 + m25 + m30 + m45 + m48 + m51 + m64 + m68 + m72 + m75 <= 11; s.t. pm335: m02 + m11 + m22 + m24 + m34 + m40 + m47 + m51 + m57 + m66 + m74 + m82 <= 11; s.t. pm336: m02 + m11 + m19 + m28 + m34 + m41 + m45 + m51 + m57 + m68 + m72 + m82 <= 11; s.t. pm337: m02 + m13 + m20 + m24 + m32 + m40 + m49 + m51 + m57 + m68 + m72 + m82 <= 11; s.t. pm338: m02 + m13 + m19 + m26 + m32 + m43 + m45 + m51 + m57 + m66 + m74 + m82 <= 11; s.t. pm339: m02 + m13 + m19 + m26 + m33 + m43 + m44 + m51 + m56 + m67 + m73 + m83 <= 11; s.t. pm340: m02 + m09 + m25 + m26 + m33 + m43 + m44 + m51 + m63 + m66 + m74 + m76 <= 11; s.t. pm341: m02 + m09 + m25 + m26 + m32 + m43 + m45 + m51 + m64 + m67 + m73 + m75 <= 11; s.t. pm342: m02 + m09 + m23 + m28 + m33 + m41 + m46 + m51 + m63 + m68 + m72 + m76 <= 11; s.t. pm343: m06 + m09 + m18 + m23 + m32 + m35 + m46 + m51 + m64 + m72 + m76 + m79 <= 11; s.t. pm344: m07 + m09 + m17 + m23 + m32 + m35 + m45 + m51 + m64 + m73 + m77 + m78 <= 11; s.t. pm345: m02 + m09 + m23 + m28 + m34 + m41 + m45 + m51 + m62 + m67 + m73 + m77 <= 11; s.t. pm346: m07 + m09 + m17 + m23 + m33 + m37 + m40 + m51 + m63 + m68 + m78 + m83 <= 11; s.t. pm347: m06 + m09 + m18 + m23 + m34 + m37 + m40 + m51 + m62 + m67 + m79 + m83 <= 11; s.t. pm348: m02 + m13 + m21 + m23 + m33 + m40 + m48 + m51 + m56 + m68 + m72 + m83 <= 11; s.t. pm349: m03 + m13 + m17 + m23 + m33 + m37 + m46 + m51 + m56 + m68 + m76 + m84 <= 11; s.t. pm350: m02 + m13 + m21 + m23 + m30 + m45 + m48 + m51 + m62 + m66 + m74 + m77 <= 11; s.t. pm351: m03 + m13 + m17 + m23 + m32 + m39 + m45 + m51 + m57 + m66 + m77 + m84 <= 11; s.t. pm352: m02 + m12 + m22 + m23 + m30 + m46 + m47 + m51 + m63 + m66 + m74 + m76 <= 11; s.t. pm353: m02 + m12 + m22 + m23 + m34 + m40 + m47 + m51 + m56 + m67 + m73 + m83 <= 11; s.t. pm354: m03 + m12 + m18 + m23 + m34 + m37 + m45 + m51 + m56 + m67 + m77 + m84 <= 11; s.t. pm355: m02 + m10 + m20 + m28 + m30 + m46 + m47 + m53 + m63 + m68 + m69 + m76 <= 11; s.t. pm356: m02 + m11 + m19 + m28 + m30 + m46 + m47 + m54 + m60 + m67 + m69 + m79 <= 11; s.t. pm357: m05 + m10 + m14 + m28 + m30 + m39 + m45 + m53 + m63 + m69 + m77 + m78 <= 11; s.t. pm358: m05 + m08 + m19 + m28 + m30 + m39 + m45 + m61 + m62 + m67 + m69 + m79 <= 11; s.t. pm359: m02 + m10 + m20 + m28 + m30 + m45 + m48 + m54 + m62 + m67 + m69 + m77 <= 11; s.t. pm360: m02 + m11 + m19 + m28 + m30 + m45 + m48 + m53 + m61 + m68 + m69 + m78 <= 11; s.t. pm361: m03 + m12 + m18 + m23 + m32 + m38 + m46 + m51 + m58 + m66 + m76 + m84 <= 11; s.t. pm362: m02 + m10 + m20 + m28 + m33 + m40 + m48 + m52 + m58 + m67 + m71 + m81 <= 11; s.t. pm363: m02 + m11 + m19 + m28 + m31 + m42 + m48 + m53 + m58 + m66 + m71 + m81 <= 11; s.t. pm364: m02 + m09 + m23 + m28 + m31 + m43 + m47 + m53 + m63 + m66 + m71 + m76 <= 11; s.t. pm365: m02 + m10 + m20 + m28 + m33 + m43 + m44 + m50 + m63 + m71 + m72 + m76 <= 11; s.t. pm366: m02 + m09 + m23 + m28 + m34 + m40 + m47 + m52 + m60 + m67 + m71 + m79 <= 11; s.t. pm367: m02 + m11 + m19 + m28 + m34 + m42 + m44 + m50 + m60 + m71 + m72 + m79 <= 11; s.t. pm368: m04 + m11 + m14 + m28 + m30 + m39 + m47 + m53 + m61 + m69 + m76 + m79 <= 11; s.t. pm369: m04 + m08 + m20 + m28 + m30 + m39 + m47 + m60 + m63 + m67 + m69 + m77 <= 11; s.t. pm370: m02 + m10 + m20 + m28 + m32 + m42 + m46 + m53 + m58 + m65 + m73 + m81 <= 11; s.t. pm371: m02 + m09 + m23 + m28 + m32 + m43 + m45 + m53 + m61 + m65 + m73 + m78 <= 11; s.t. pm372: m02 + m10 + m20 + m28 + m32 + m43 + m45 + m54 + m57 + m65 + m72 + m82 <= 11; s.t. pm373: m02 + m09 + m23 + m28 + m32 + m42 + m46 + m54 + m60 + m65 + m72 + m79 <= 11; s.t. pm374: m04 + m09 + m16 + m28 + m32 + m39 + m42 + m53 + m61 + m65 + m79 + m81 <= 11; s.t. pm375: m04 + m08 + m20 + m28 + m32 + m39 + m42 + m58 + m60 + m65 + m72 + m82 <= 11; s.t. pm376: m03 + m08 + m23 + m28 + m32 + m39 + m45 + m57 + m61 + m65 + m72 + m79 <= 11; s.t. pm377: m03 + m10 + m16 + m28 + m32 + m39 + m45 + m53 + m58 + m65 + m78 + m82 <= 11; s.t. pm378: m02 + m11 + m19 + m28 + m33 + m43 + m44 + m50 + m61 + m70 + m73 + m78 <= 11; s.t. pm379: m04 + m08 + m20 + m28 + m33 + m35 + m48 + m58 + m59 + m71 + m72 + m76 <= 11; s.t. pm380: m05 + m08 + m19 + m28 + m34 + m35 + m45 + m57 + m59 + m71 + m72 + m79 <= 11; s.t. pm381: m04 + m09 + m16 + m28 + m34 + m35 + m47 + m53 + m59 + m71 + m76 + m79 <= 11; s.t. pm382: m05 + m08 + m19 + m28 + m31 + m39 + m42 + m58 + m62 + m66 + m70 + m82 <= 11; s.t. pm383: m02 + m11 + m19 + m28 + m31 + m43 + m47 + m54 + m57 + m66 + m70 + m82 <= 11; s.t. pm384: m06 + m09 + m18 + m23 + m32 + m36 + m43 + m53 + m61 + m66 + m76 + m84 <= 11; s.t. pm385: m06 + m13 + m14 + m23 + m31 + m37 + m43 + m53 + m56 + m71 + m76 + m84 <= 11; s.t. pm386: m06 + m09 + m18 + m23 + m31 + m37 + m43 + m53 + m63 + m65 + m78 + m83 <= 11; s.t. pm387: m06 + m11 + m18 + m19 + m30 + m36 + m48 + m53 + m61 + m66 + m80 + m81 <= 11; s.t. pm388: m06 + m10 + m18 + m20 + m30 + m37 + m46 + m53 + m63 + m65 + m80 + m81 <= 11; s.t. pm389: m06 + m10 + m18 + m20 + m32 + m35 + m46 + m53 + m58 + m69 + m76 + m84 <= 11; s.t. pm390: m06 + m11 + m18 + m19 + m31 + m35 + m48 + m53 + m58 + m69 + m78 + m83 <= 11; s.t. pm391: m06 + m13 + m16 + m19 + m31 + m35 + m48 + m53 + m56 + m71 + m80 + m81 <= 11; s.t. pm392: m06 + m13 + m16 + m19 + m30 + m36 + m48 + m53 + m59 + m68 + m78 + m83 <= 11; s.t. pm393: m06 + m13 + m15 + m20 + m30 + m37 + m46 + m53 + m59 + m68 + m76 + m84 <= 11; s.t. pm394: m07 + m10 + m14 + m26 + m33 + m37 + m40 + m54 + m56 + m70 + m80 + m82 <= 11; s.t. pm395: m07 + m10 + m17 + m20 + m33 + m37 + m40 + m50 + m63 + m71 + m80 + m81 <= 11; s.t. pm396: m02 + m10 + m22 + m26 + m32 + m40 + m49 + m54 + m57 + m66 + m70 + m82 <= 11; s.t. pm397: m02 + m09 + m25 + m26 + m33 + m40 + m48 + m54 + m59 + m66 + m70 + m80 <= 11; s.t. pm398: m02 + m09 + m25 + m26 + m32 + m40 + m49 + m54 + m60 + m67 + m69 + m79 <= 11; s.t. pm399: m02 + m09 + m25 + m26 + m31 + m42 + m48 + m52 + m64 + m68 + m70 + m75 <= 11; s.t. pm400: m02 + m10 + m22 + m26 + m30 + m45 + m48 + m52 + m64 + m67 + m71 + m75 <= 11; s.t. pm401: m02 + m09 + m25 + m26 + m31 + m41 + m49 + m53 + m63 + m68 + m69 + m76 <= 11; s.t. pm402: m02 + m09 + m25 + m26 + m34 + m41 + m45 + m53 + m59 + m65 + m73 + m80 <= 11; s.t. pm403: m02 + m09 + m25 + m26 + m34 + m42 + m44 + m52 + m60 + m65 + m74 + m79 <= 11; s.t. pm404: m02 + m10 + m22 + m26 + m33 + m41 + m46 + m50 + m63 + m69 + m74 + m76 <= 11; s.t. pm405: m02 + m10 + m22 + m26 + m32 + m42 + m46 + m50 + m64 + m70 + m73 + m75 <= 11; s.t. pm406: m02 + m10 + m22 + m26 + m34 + m41 + m45 + m52 + m57 + m65 + m74 + m82 <= 11; s.t. pm407: m03 + m11 + m18 + m24 + m33 + m36 + m48 + m50 + m61 + m72 + m75 + m80 <= 11; s.t. pm408: m03 + m12 + m18 + m23 + m32 + m36 + m49 + m50 + m61 + m72 + m76 + m79 <= 11; s.t. pm409: m03 + m10 + m18 + m26 + m32 + m36 + m49 + m53 + m58 + m66 + m76 + m82 <= 11; s.t. pm410: m03 + m10 + m18 + m26 + m34 + m37 + m45 + m53 + m56 + m65 + m80 + m82 <= 11; s.t. pm411: m03 + m11 + m18 + m24 + m31 + m37 + m49 + m53 + m58 + m65 + m78 + m82 <= 11; s.t. pm412: m04 + m11 + m18 + m21 + m33 + m37 + m43 + m50 + m61 + m70 + m75 + m84 <= 11; s.t. pm413: m04 + m11 + m18 + m21 + m30 + m37 + m49 + m53 + m61 + m65 + m79 + m81 <= 11; s.t. pm414: m03 + m13 + m17 + m23 + m31 + m39 + m47 + m52 + m57 + m65 + m79 + m83 <= 11; s.t. pm415: m07 + m09 + m17 + m23 + m31 + m37 + m42 + m54 + m62 + m65 + m79 + m83 <= 11; s.t. pm416: m04 + m09 + m18 + m26 + m34 + m37 + m42 + m53 + m59 + m65 + m79 + m83 <= 11; s.t. pm417: m04 + m13 + m16 + m21 + m30 + m39 + m47 + m53 + m59 + m65 + m79 + m83 <= 11; s.t. pm418: m07 + m11 + m17 + m19 + m31 + m35 + m47 + m54 + m57 + m69 + m79 + m83 <= 11; s.t. pm419: m05 + m13 + m17 + m19 + m31 + m39 + m42 + m50 + m62 + m69 + m79 + m83 <= 11; s.t. pm420: m05 + m13 + m15 + m21 + m33 + m39 + m40 + m50 + m59 + m72 + m79 + m83 <= 11; s.t. pm421: m05 + m12 + m18 + m19 + m34 + m36 + m42 + m50 + m59 + m72 + m79 + m83 <= 11; s.t. pm422: m07 + m12 + m16 + m19 + m30 + m36 + m47 + m54 + m59 + m67 + m79 + m83 <= 11; s.t. pm423: m07 + m09 + m15 + m26 + m33 + m37 + m40 + m54 + m59 + m67 + m79 + m83 <= 11; s.t. pm424: m06 + m11 + m14 + m25 + m31 + m39 + m41 + m53 + m58 + m69 + m76 + m84 <= 11; s.t. pm425: m06 + m10 + m16 + m22 + m34 + m35 + m44 + m53 + m56 + m71 + m76 + m84 <= 11; s.t. pm426: m06 + m09 + m16 + m25 + m34 + m36 + m41 + m53 + m59 + m68 + m76 + m84 <= 11; s.t. pm427: m06 + m09 + m16 + m25 + m31 + m39 + m41 + m53 + m63 + m65 + m80 + m81 <= 11; s.t. pm428: m06 + m10 + m16 + m22 + m30 + m39 + m44 + m53 + m63 + m65 + m78 + m83 <= 11; s.t. pm429: m02 + m13 + m21 + m23 + m30 + m46 + m47 + m52 + m60 + m65 + m74 + m79 <= 11; s.t. pm430: m02 + m13 + m20 + m24 + m30 + m46 + m47 + m53 + m59 + m65 + m73 + m80 <= 11; s.t. pm431: m02 + m13 + m19 + m26 + m30 + m45 + m48 + m53 + m59 + m66 + m71 + m80 <= 11; s.t. pm432: m02 + m11 + m21 + m25 + m31 + m41 + m49 + m53 + m58 + m65 + m73 + m81 <= 11; s.t. pm433: m02 + m10 + m22 + m26 + m30 + m44 + m49 + m53 + m63 + m66 + m71 + m76 <= 11; s.t. pm434: m02 + m11 + m22 + m24 + m30 + m44 + m49 + m53 + m61 + m65 + m73 + m78 <= 11; s.t. pm435: m02 + m13 + m19 + m26 + m31 + m42 + m48 + m53 + m56 + m68 + m69 + m83 <= 11; s.t. pm436: m02 + m10 + m22 + m26 + m33 + m40 + m48 + m54 + m56 + m67 + m69 + m83 <= 11; s.t. pm437: m02 + m10 + m22 + m26 + m34 + m42 + m44 + m53 + m56 + m65 + m73 + m83 <= 11; s.t. pm438: m02 + m13 + m21 + m23 + m31 + m43 + m47 + m53 + m56 + m65 + m73 + m83 <= 11; s.t. pm439: m02 + m12 + m22 + m23 + m31 + m42 + m48 + m54 + m56 + m65 + m72 + m83 <= 11; s.t. pm440: m03 + m12 + m16 + m25 + m31 + m39 + m47 + m50 + m63 + m70 + m75 + m80 <= 11; s.t. pm441: m03 + m10 + m18 + m26 + m33 + m37 + m46 + m50 + m63 + m70 + m75 + m80 <= 11; s.t. pm442: m07 + m08 + m20 + m24 + m31 + m35 + m47 + m57 + m63 + m69 + m74 + m77 <= 11; s.t. pm443: m07 + m08 + m21 + m23 + m30 + m36 + m47 + m60 + m63 + m66 + m74 + m77 <= 11; s.t. pm444: m07 + m09 + m16 + m24 + m31 + m35 + m47 + m53 + m63 + m71 + m75 + m80 <= 11; s.t. pm445: m07 + m10 + m14 + m26 + m30 + m37 + m45 + m53 + m63 + m71 + m75 + m80 <= 11; s.t. pm446: m07 + m12 + m15 + m20 + m31 + m37 + m42 + m50 + m63 + m74 + m77 + m81 <= 11; s.t. pm447: m07 + m10 + m16 + m21 + m33 + m36 + m41 + m50 + m63 + m74 + m77 + m81 <= 11; s.t. pm448: m04 + m08 + m22 + m26 + m30 + m37 + m49 + m60 + m63 + m67 + m71 + m75 <= 11; s.t. pm449: m05 + m10 + m18 + m21 + m30 + m36 + m49 + m53 + m63 + m66 + m77 + m81 <= 11; s.t. pm450: m05 + m08 + m21 + m25 + m30 + m36 + m49 + m60 + m63 + m68 + m72 + m75 <= 11; s.t. pm451: m05 + m09 + m18 + m24 + m31 + m35 + m49 + m53 + m63 + m69 + m77 + m78 <= 11; s.t. pm452: m05 + m08 + m22 + m24 + m31 + m35 + m49 + m57 + m63 + m71 + m72 + m75 <= 11; s.t. pm453: m03 + m08 + m25 + m26 + m31 + m37 + m49 + m57 + m63 + m68 + m70 + m75 <= 11; s.t. pm454: m03 + m12 + m18 + m23 + m31 + m37 + m49 + m50 + m63 + m70 + m77 + m78 <= 11; s.t. pm455: m05 + m12 + m14 + m25 + m31 + m39 + m42 + m52 + m58 + m70 + m75 + m84 <= 11; s.t. pm456: m07 + m12 + m14 + m23 + m30 + m36 + m47 + m52 + m61 + m74 + m76 + m79 <= 11; s.t. pm457: m04 + m09 + m18 + m26 + m33 + m35 + m48 + m52 + m61 + m70 + m75 + m80 <= 11; s.t. pm458: m04 + m13 + m17 + m20 + m30 + m39 + m47 + m52 + m60 + m65 + m80 + m82 <= 11; s.t. pm459: m06 + m10 + m18 + m20 + m34 + m37 + m40 + m50 + m62 + m70 + m80 + m82 <= 11; s.t. pm460: m06 + m10 + m18 + m20 + m32 + m36 + m43 + m50 + m64 + m72 + m76 + m82 <= 11; s.t. pm461: m06 + m10 + m16 + m22 + m32 + m39 + m40 + m50 + m64 + m70 + m78 + m82 <= 11; s.t. pm462: m06 + m10 + m18 + m20 + m30 + m36 + m48 + m52 + m64 + m67 + m77 + m81 <= 11; s.t. pm463: m06 + m10 + m16 + m22 + m30 + m36 + m48 + m54 + m62 + m67 + m75 + m83 <= 11; s.t. pm464: m06 + m10 + m16 + m22 + m32 + m35 + m46 + m54 + m57 + m70 + m75 + m84 <= 11; s.t. pm465: m06 + m10 + m16 + m22 + m34 + m36 + m41 + m50 + m62 + m74 + m76 + m82 <= 11; s.t. pm466: m06 + m09 + m16 + m25 + m31 + m35 + m48 + m54 + m62 + m70 + m75 + m80 <= 11; s.t. pm467: m06 + m11 + m15 + m22 + m30 + m39 + m44 + m53 + m61 + m66 + m76 + m84 <= 11; s.t. pm468: m06 + m13 + m16 + m19 + m31 + m39 + m41 + m50 + m62 + m70 + m80 + m82 <= 11; s.t. pm469: m06 + m13 + m16 + m19 + m32 + m36 + m43 + m50 + m60 + m74 + m78 + m82 <= 11; s.t. pm470: m06 + m09 + m16 + m25 + m32 + m36 + m43 + m54 + m60 + m67 + m75 + m84 <= 11; s.t. pm471: m06 + m11 + m15 + m22 + m31 + m39 + m41 + m50 + m64 + m72 + m76 + m82 <= 11; s.t. pm472: m06 + m11 + m15 + m22 + m31 + m35 + m48 + m54 + m57 + m72 + m75 + m83 <= 11; s.t. pm473: m06 + m11 + m15 + m22 + m34 + m37 + m40 + m50 + m60 + m74 + m78 + m82 <= 11; s.t. pm474: m06 + m11 + m15 + m22 + m30 + m37 + m46 + m54 + m60 + m67 + m75 + m84 <= 11; s.t. pm475: m06 + m08 + m20 + m25 + m31 + m35 + m48 + m58 + m62 + m69 + m74 + m76 <= 11; s.t. pm476: m06 + m08 + m20 + m25 + m31 + m37 + m43 + m57 + m63 + m65 + m74 + m81 <= 11; s.t. pm477: m06 + m08 + m22 + m23 + m32 + m39 + m40 + m57 + m61 + m66 + m70 + m84 <= 11; s.t. pm478: m06 + m11 + m14 + m25 + m31 + m37 + m43 + m54 + m57 + m70 + m75 + m84 <= 11; s.t. pm479: m06 + m08 + m22 + m23 + m31 + m35 + m48 + m56 + m64 + m71 + m72 + m76 <= 11; s.t. pm480: m06 + m11 + m14 + m25 + m30 + m36 + m48 + m54 + m60 + m72 + m75 + m80 <= 11; s.t. pm481: m06 + m11 + m18 + m19 + m34 + m36 + m41 + m50 + m60 + m72 + m80 + m82 <= 11; s.t. pm482: m06 + m11 + m18 + m19 + m31 + m37 + m43 + m50 + m64 + m70 + m78 + m82 <= 11; s.t. pm483: m06 + m08 + m20 + m25 + m34 + m37 + m40 + m57 + m59 + m68 + m70 + m84 <= 11; s.t. pm484: m06 + m08 + m22 + m23 + m31 + m39 + m41 + m57 + m63 + m65 + m72 + m83 <= 11; s.t. pm485: m06 + m08 + m20 + m25 + m32 + m39 + m40 + m58 + m60 + m67 + m69 + m84 <= 11; s.t. pm486: m06 + m08 + m20 + m25 + m30 + m39 + m44 + m60 + m63 + m65 + m72 + m80 <= 11; s.t. pm487: m06 + m08 + m22 + m23 + m34 + m37 + m40 + m56 + m60 + m67 + m71 + m84 <= 11; s.t. pm488: m06 + m08 + m20 + m25 + m30 + m36 + m48 + m59 + m64 + m68 + m72 + m76 <= 11; s.t. pm489: m06 + m08 + m22 + m23 + m30 + m37 + m46 + m60 + m63 + m65 + m74 + m78 <= 11; s.t. pm490: m06 + m13 + m14 + m23 + m31 + m39 + m41 + m52 + m57 + m70 + m77 + m84 <= 11; s.t. pm491: m06 + m08 + m22 + m23 + m30 + m36 + m48 + m61 + m62 + m66 + m74 + m76 <= 11; s.t. pm492: m06 + m09 + m18 + m23 + m34 + m36 + m41 + m52 + m60 + m67 + m77 + m84 <= 11; s.t. pm493: m06 + m13 + m14 + m23 + m30 + m36 + m48 + m52 + m60 + m74 + m77 + m78 <= 11; s.t. pm494: m06 + m13 + m15 + m20 + m31 + m37 + m43 + m50 + m62 + m74 + m76 + m82 <= 11; s.t. pm495: m06 + m09 + m18 + m23 + m31 + m35 + m48 + m52 + m64 + m70 + m77 + m78 <= 11; s.t. pm496: m06 + m13 + m15 + m20 + m31 + m35 + m48 + m52 + m57 + m74 + m77 + m81 <= 11; s.t. pm497: m05 + m10 + m18 + m21 + m30 + m38 + m46 + m52 + m64 + m65 + m79 + m81 <= 11; s.t. pm498: m06 + m13 + m15 + m20 + m32 + m39 + m40 + m50 + m60 + m72 + m80 + m82 <= 11; s.t. pm499: m06 + m13 + m15 + m20 + m30 + m39 + m44 + m52 + m60 + m67 + m77 + m84 <= 11; s.t. pm500: m05 + m09 + m18 + m24 + m31 + m38 + m43 + m52 + m64 + m65 + m78 + m82 <= 11; s.t. pm501: m05 + m09 + m15 + m28 + m34 + m38 + m40 + m52 + m60 + m68 + m78 + m82 <= 11; s.t. pm502: m05 + m08 + m19 + m28 + m30 + m38 + m46 + m60 + m63 + m68 + m69 + m78 <= 11; s.t. pm503: m05 + m12 + m18 + m19 + m30 + m38 + m46 + m51 + m63 + m66 + m80 + m81 <= 11; s.t. pm504: m05 + m13 + m17 + m19 + m33 + m35 + m46 + m51 + m56 + m73 + m80 + m81 <= 11; s.t. pm505: m05 + m09 + m17 + m25 + m33 + m39 + m40 + m51 + m63 + m66 + m80 + m81 <= 11; s.t. pm506: m05 + m09 + m18 + m24 + m34 + m38 + m40 + m51 + m62 + m66 + m80 + m82 <= 11; s.t. pm507: m05 + m12 + m18 + m19 + m34 + m35 + m45 + m51 + m56 + m72 + m80 + m82 <= 11; s.t. pm508: m05 + m13 + m17 + m19 + m30 + m39 + m45 + m51 + m62 + m66 + m80 + m82 <= 11; s.t. pm509: m05 + m09 + m17 + m25 + m34 + m35 + m45 + m51 + m62 + m73 + m75 + m80 <= 11; s.t. pm510: m05 + m09 + m18 + m24 + m33 + m35 + m46 + m51 + m63 + m72 + m75 + m80 <= 11; s.t. pm511: m03 + m11 + m17 + m25 + m33 + m39 + m44 + m51 + m58 + m66 + m76 + m84 <= 11; s.t. pm512: m07 + m11 + m17 + m19 + m33 + m35 + m44 + m51 + m58 + m73 + m78 + m83 <= 11; s.t. pm513: m03 + m11 + m18 + m24 + m33 + m37 + m46 + m51 + m58 + m67 + m75 + m84 <= 11; s.t. pm514: m07 + m12 + m16 + m19 + m32 + m35 + m45 + m51 + m58 + m74 + m78 + m82 <= 11; s.t. pm515: m07 + m09 + m16 + m24 + m32 + m38 + m40 + m51 + m64 + m68 + m78 + m82 <= 11; s.t. pm516: m07 + m12 + m16 + m19 + m30 + m38 + m44 + m51 + m63 + m68 + m78 + m83 <= 11; s.t. pm517: m07 + m09 + m16 + m24 + m33 + m35 + m44 + m51 + m63 + m74 + m77 + m78 <= 11; s.t. pm518: m06 + m11 + m18 + m19 + m30 + m37 + m46 + m51 + m64 + m67 + m79 + m81 <= 11; s.t. pm519: m07 + m11 + m17 + m19 + m30 + m37 + m45 + m51 + m64 + m68 + m78 + m82 <= 11; s.t. pm520: m02 + m12 + m20 + m25 + m32 + m40 + m49 + m51 + m58 + m67 + m73 + m81 <= 11; s.t. pm521: m02 + m12 + m20 + m25 + m30 + m44 + m49 + m51 + m63 + m68 + m72 + m76 <= 11; s.t. pm522: m02 + m13 + m20 + m24 + m30 + m44 + m49 + m51 + m62 + m67 + m73 + m77 <= 11; s.t. pm523: m05 + m08 + m19 + m28 + m33 + m35 + m46 + m58 + m59 + m70 + m73 + m78 <= 11; s.t. pm524: m05 + m08 + m19 + m28 + m34 + m36 + m42 + m56 + m60 + m68 + m72 + m82 <= 11; s.t. pm525: m05 + m08 + m19 + m28 + m33 + m36 + m43 + m56 + m61 + m67 + m73 + m81 <= 11; s.t. pm526: m03 + m12 + m16 + m25 + m34 + m38 + m44 + m51 + m56 + m68 + m76 + m84 <= 11; s.t. pm527: m03 + m12 + m16 + m25 + m32 + m39 + m45 + m51 + m58 + m67 + m75 + m84 <= 11; s.t. pm528: m03 + m13 + m16 + m24 + m33 + m39 + m44 + m51 + m56 + m67 + m77 + m84 <= 11; s.t. pm529: m07 + m12 + m16 + m19 + m29 + m42 + m44 + m56 + m61 + m68 + m70 + m84 <= 11; s.t. pm530: m07 + m12 + m14 + m23 + m29 + m40 + m47 + m56 + m61 + m70 + m73 + m80 <= 11; s.t. pm531: m04 + m12 + m16 + m22 + m29 + m42 + m48 + m56 + m61 + m65 + m74 + m81 <= 11; s.t. pm532: m03 + m13 + m17 + m23 + m29 + m46 + m47 + m56 + m60 + m65 + m73 + m80 <= 11; s.t. pm533: m03 + m12 + m18 + m23 + m29 + m45 + m48 + m56 + m61 + m65 + m72 + m80 <= 11; s.t. pm534: m03 + m12 + m16 + m25 + m29 + m45 + m48 + m58 + m59 + m65 + m74 + m78 <= 11; s.t. pm535: m07 + m12 + m16 + m19 + m29 + m41 + m45 + m58 + m59 + m67 + m71 + m84 <= 11; s.t. pm536: m07 + m11 + m14 + m24 + m33 + m36 + m41 + m54 + m55 + m72 + m80 + m82 <= 11; s.t. pm537: m04 + m09 + m18 + m26 + m29 + m42 + m48 + m59 + m64 + m66 + m70 + m77 <= 11; s.t. pm538: m04 + m08 + m21 + m27 + m33 + m39 + m41 + m58 + m59 + m65 + m72 + m83 <= 11; s.t. pm539: m04 + m08 + m21 + m27 + m33 + m37 + m43 + m56 + m61 + m65 + m74 + m81 <= 11; s.t. pm540: m04 + m12 + m14 + m27 + m34 + m37 + m42 + m51 + m56 + m74 + m77 + m81 <= 11; s.t. pm541: m04 + m12 + m14 + m27 + m29 + m41 + m49 + m58 + m59 + m71 + m72 + m76 <= 11; s.t. pm542: m04 + m08 + m21 + m27 + m32 + m35 + m49 + m58 + m60 + m71 + m72 + m75 <= 11; s.t. pm543: m04 + m12 + m14 + m27 + m32 + m39 + m42 + m51 + m58 + m72 + m75 + m83 <= 11; s.t. pm544: m06 + m10 + m14 + m27 + m29 + m43 + m44 + m56 + m64 + m71 + m72 + m76 <= 11; s.t. pm545: m06 + m08 + m19 + m27 + m31 + m37 + m43 + m56 + m64 + m67 + m71 + m81 <= 11; s.t. pm546: m04 + m13 + m14 + m26 + m30 + m38 + m48 + m52 + m60 + m71 + m75 + m80 <= 11; s.t. pm547: m04 + m12 + m18 + m20 + m30 + m38 + m48 + m52 + m61 + m65 + m80 + m81 <= 11; s.t. pm548: m04 + m09 + m18 + m26 + m34 + m38 + m41 + m52 + m60 + m65 + m80 + m82 <= 11; s.t. pm549: m04 + m12 + m16 + m22 + m30 + m38 + m48 + m54 + m59 + m65 + m78 + m83 <= 11; s.t. pm550: m04 + m08 + m22 + m26 + m34 + m38 + m41 + m57 + m59 + m65 + m73 + m83 <= 11; s.t. pm551: m04 + m09 + m16 + m28 + m32 + m38 + m43 + m54 + m60 + m65 + m78 + m82 <= 11; s.t. pm552: m04 + m08 + m20 + m28 + m32 + m38 + m43 + m57 + m61 + m65 + m73 + m81 <= 11; s.t. pm553: m04 + m08 + m20 + m28 + m30 + m38 + m48 + m61 + m62 + m68 + m69 + m76 <= 11; s.t. pm554: m04 + m12 + m18 + m20 + m32 + m38 + m43 + m50 + m61 + m69 + m76 + m84 <= 11; s.t. pm555: m04 + m08 + m22 + m26 + m30 + m38 + m48 + m59 + m64 + m66 + m71 + m76 <= 11; s.t. pm556: m04 + m11 + m18 + m21 + m34 + m38 + m41 + m50 + m60 + m69 + m77 + m84 <= 11; s.t. pm557: m04 + m11 + m14 + m28 + m30 + m38 + m48 + m54 + m60 + m69 + m77 + m78 <= 11; s.t. pm558: m04 + m13 + m16 + m21 + m32 + m38 + m43 + m50 + m60 + m71 + m75 + m84 <= 11; s.t. pm559: m04 + m12 + m16 + m22 + m34 + m38 + m41 + m50 + m59 + m71 + m76 + m84 <= 11; s.t. pm560: m07 + m09 + m15 + m26 + m31 + m38 + m41 + m52 + m64 + m68 + m76 + m82 <= 11; s.t. pm561: m07 + m12 + m15 + m20 + m30 + m38 + m44 + m52 + m61 + m68 + m76 + m84 <= 11; s.t. pm562: m07 + m12 + m14 + m23 + m31 + m38 + m41 + m52 + m58 + m71 + m76 + m84 <= 11; s.t. pm563: m07 + m09 + m16 + m24 + m31 + m38 + m41 + m54 + m62 + m65 + m80 + m82 <= 11; s.t. pm564: m07 + m12 + m16 + m19 + m31 + m38 + m41 + m50 + m63 + m71 + m80 + m81 <= 11; s.t. pm565: m07 + m11 + m15 + m21 + m31 + m38 + m41 + m50 + m64 + m73 + m77 + m81 <= 11; s.t. pm566: m07 + m12 + m15 + m20 + m32 + m38 + m40 + m50 + m61 + m73 + m80 + m81 <= 11; s.t. pm567: m07 + m09 + m15 + m26 + m32 + m38 + m40 + m54 + m60 + m66 + m80 + m82 <= 11; s.t. pm568: m07 + m08 + m20 + m24 + m30 + m38 + m44 + m61 + m62 + m65 + m73 + m80 <= 11; s.t. pm569: m07 + m08 + m21 + m23 + m31 + m38 + m41 + m58 + m62 + m65 + m73 + m83 <= 11; s.t. pm570: m07 + m08 + m19 + m26 + m30 + m38 + m44 + m60 + m63 + m66 + m71 + m80 <= 11; s.t. pm571: m07 + m08 + m19 + m26 + m31 + m38 + m41 + m57 + m63 + m68 + m69 + m83 <= 11; s.t. pm572: m07 + m11 + m14 + m24 + m31 + m38 + m41 + m54 + m57 + m69 + m77 + m84 <= 11; s.t. pm573: m07 + m11 + m15 + m21 + m30 + m38 + m44 + m54 + m60 + m66 + m77 + m84 <= 11; s.t. pm574: m07 + m08 + m20 + m24 + m32 + m38 + m40 + m57 + m61 + m68 + m69 + m84 <= 11; s.t. pm575: m07 + m08 + m21 + m23 + m32 + m38 + m40 + m58 + m60 + m66 + m71 + m84 <= 11; s.t. pm576: m06 + m11 + m18 + m19 + m34 + m35 + m44 + m51 + m57 + m72 + m79 + m83 <= 11; s.t. pm577: m07 + m11 + m15 + m21 + m33 + m37 + m40 + m50 + m61 + m74 + m79 + m81 <= 11; s.t. pm578: m07 + m08 + m20 + m24 + m33 + m37 + m40 + m58 + m59 + m67 + m71 + m84 <= 11; s.t. pm579: m07 + m08 + m21 + m23 + m33 + m37 + m40 + m56 + m61 + m68 + m70 + m84 <= 11; s.t. pm580: m02 + m12 + m22 + m23 + m31 + m41 + m49 + m50 + m63 + m71 + m72 + m76 <= 11; s.t. pm581: m02 + m11 + m22 + m24 + m31 + m42 + m48 + m50 + m64 + m71 + m72 + m75 <= 11; s.t. pm582: m02 + m12 + m22 + m23 + m30 + m45 + m48 + m52 + m61 + m65 + m74 + m78 <= 11; s.t. pm583: m02 + m11 + m22 + m24 + m31 + m41 + m49 + m54 + m57 + m65 + m72 + m82 <= 11; s.t. pm584: m02 + m12 + m20 + m25 + m30 + m45 + m48 + m54 + m59 + m65 + m72 + m80 <= 11; s.t. pm585: m02 + m11 + m21 + m25 + m30 + m44 + m49 + m54 + m60 + m65 + m72 + m79 <= 11; s.t. pm586: m02 + m13 + m19 + m26 + m31 + m41 + m49 + m52 + m57 + m68 + m70 + m82 <= 11; s.t. pm587: m02 + m13 + m20 + m24 + m31 + m43 + m47 + m52 + m57 + m65 + m74 + m82 <= 11; s.t. pm588: m02 + m12 + m20 + m25 + m31 + m42 + m48 + m52 + m58 + m65 + m74 + m81 <= 11; s.t. pm589: m02 + m12 + m20 + m25 + m31 + m43 + m47 + m50 + m63 + m69 + m74 + m76 <= 11; s.t. pm590: m03 + m13 + m16 + m24 + m31 + m39 + m47 + m53 + m56 + m65 + m80 + m82 <= 11; s.t. pm591: m03 + m13 + m15 + m26 + m31 + m37 + m49 + m53 + m56 + m68 + m76 + m82 <= 11; s.t. pm592: m03 + m13 + m17 + m23 + m32 + m36 + m49 + m50 + m60 + m73 + m77 + m78 <= 11; s.t. pm593: m03 + m13 + m16 + m24 + m33 + m36 + m48 + m50 + m59 + m74 + m77 + m78 <= 11; s.t. pm594: m03 + m13 + m17 + m23 + m31 + m37 + m49 + m50 + m62 + m71 + m76 + m79 <= 11; s.t. pm595: m03 + m08 + m25 + m26 + m33 + m36 + m48 + m58 + m59 + m66 + m74 + m76 <= 11; s.t. pm596: m03 + m11 + m17 + m25 + m31 + m39 + m47 + m50 + m64 + m69 + m76 + m79 <= 11; s.t. pm597: m03 + m11 + m17 + m25 + m31 + m37 + m49 + m54 + m57 + m65 + m79 + m81 <= 11; s.t. pm598: m03 + m12 + m16 + m25 + m34 + m36 + m47 + m50 + m59 + m74 + m76 + m79 <= 11; s.t. pm599: m03 + m08 + m25 + m26 + m34 + m37 + m45 + m57 + m59 + m65 + m74 + m79 <= 11; s.t. pm600: m07 + m10 + m14 + m26 + m33 + m36 + m41 + m52 + m58 + m74 + m76 + m82 <= 11; s.t. pm601: m06 + m10 + m18 + m20 + m34 + m35 + m44 + m52 + m57 + m70 + m77 + m84 <= 11; s.t. pm602: m06 + m09 + m16 + m25 + m32 + m39 + m40 + m51 + m64 + m67 + m79 + m81 <= 11; s.t. pm603: m06 + m13 + m16 + m19 + m30 + m39 + m44 + m51 + m62 + m67 + m79 + m83 <= 11; s.t. pm604: m06 + m09 + m16 + m25 + m34 + m35 + m44 + m51 + m62 + m74 + m76 + m79 <= 11; s.t. pm605: m04 + m13 + m16 + m21 + m29 + m43 + m47 + m56 + m60 + m65 + m74 + m82 <= 11; s.t. pm606: m02 + m12 + m20 + m25 + m34 + m40 + m47 + m50 + m59 + m70 + m73 + m80 <= 11; s.t. pm607: m02 + m11 + m21 + m25 + m34 + m40 + m47 + m50 + m60 + m69 + m74 + m79 <= 11; s.t. pm608: m07 + m08 + m19 + m26 + m30 + m37 + m45 + m59 + m64 + m67 + m71 + m79 <= 11; s.t. pm609: m07 + m08 + m19 + m26 + m33 + m35 + m44 + m56 + m61 + m70 + m73 + m80 <= 11; s.t. pm610: m07 + m08 + m19 + m26 + m31 + m37 + m42 + m56 + m64 + m68 + m70 + m82 <= 11; s.t. pm611: m07 + m08 + m19 + m26 + m32 + m35 + m45 + m57 + m61 + m69 + m74 + m79 <= 11; s.t. pm612: m07 + m08 + m19 + m26 + m32 + m36 + m42 + m58 + m60 + m66 + m74 + m82 <= 11; s.t. pm613: m07 + m08 + m21 + m23 + m31 + m35 + m47 + m56 + m64 + m70 + m73 + m77 <= 11; s.t. pm614: m05 + m08 + m21 + m25 + m31 + m35 + m49 + m58 + m62 + m70 + m73 + m75 <= 11; s.t. pm615: m04 + m08 + m22 + m26 + m34 + m37 + m42 + m56 + m60 + m65 + m74 + m82 <= 11; s.t. pm616: m04 + m08 + m22 + m26 + m33 + m35 + m48 + m56 + m61 + m69 + m74 + m76 <= 11; s.t. pm617: m04 + m08 + m22 + m26 + m32 + m35 + m49 + m57 + m61 + m70 + m73 + m75 <= 11; s.t. pm618: m04 + m13 + m14 + m26 + m30 + m37 + m49 + m53 + m59 + m71 + m76 + m79 <= 11; s.t. pm619: m03 + m11 + m17 + m25 + m34 + m36 + m47 + m50 + m60 + m73 + m75 + m80 <= 11; s.t. pm620: m03 + m08 + m25 + m26 + m32 + m36 + m49 + m58 + m60 + m67 + m73 + m75 <= 11; s.t. pm621: m03 + m13 + m15 + m26 + m33 + m37 + m46 + m50 + m59 + m74 + m76 + m79 <= 11; s.t. pm622: m05 + m12 + m14 + m25 + m30 + m36 + m49 + m54 + m59 + m72 + m76 + m79 <= 11; s.t. pm623: m07 + m11 + m14 + m24 + m30 + m36 + m47 + m53 + m61 + m73 + m75 + m80 <= 11; s.t. pm624: m05 + m13 + m14 + m24 + m30 + m36 + m49 + m53 + m59 + m73 + m77 + m78 <= 11; s.t. pm625: m07 + m11 + m15 + m21 + m30 + m37 + m45 + m53 + m61 + m68 + m75 + m84 <= 11; s.t. pm626: m07 + m10 + m17 + m20 + m30 + m37 + m45 + m54 + m62 + m65 + m80 + m82 <= 11; s.t. pm627: m07 + m12 + m15 + m20 + m30 + m37 + m45 + m54 + m59 + m67 + m77 + m84 <= 11; s.t. pm628: m05 + m13 + m15 + m21 + m30 + m39 + m45 + m53 + m59 + m66 + m77 + m84 <= 11; s.t. pm629: m07 + m11 + m17 + m19 + m30 + m36 + m47 + m54 + m60 + m66 + m80 + m82 <= 11; s.t. pm630: m05 + m10 + m17 + m22 + m30 + m36 + m49 + m54 + m62 + m66 + m76 + m82 <= 11; s.t. pm631: m04 + m12 + m16 + m22 + m32 + m39 + m42 + m50 + m61 + m70 + m75 + m84 <= 11; s.t. pm632: m04 + m11 + m17 + m22 + m34 + m37 + m42 + m50 + m60 + m71 + m75 + m84 <= 11; s.t. pm633: m04 + m11 + m17 + m22 + m30 + m37 + m49 + m54 + m60 + m65 + m78 + m82 <= 11; s.t. pm634: m04 + m11 + m17 + m22 + m33 + m39 + m41 + m50 + m61 + m69 + m76 + m84 <= 11; s.t. pm635: m04 + m13 + m16 + m21 + m33 + m39 + m41 + m50 + m59 + m70 + m77 + m84 <= 11; s.t. pm636: m04 + m13 + m17 + m20 + m33 + m37 + m43 + m50 + m59 + m71 + m76 + m84 <= 11; s.t. pm637: m04 + m13 + m17 + m20 + m32 + m39 + m42 + m50 + m60 + m69 + m77 + m84 <= 11; s.t. pm638: m07 + m11 + m15 + m21 + m29 + m41 + m45 + m55 + m64 + m68 + m72 + m82 <= 11; s.t. pm639: m04 + m13 + m17 + m20 + m29 + m42 + m48 + m55 + m62 + m68 + m69 + m83 <= 11; s.t. pm640: m04 + m11 + m18 + m21 + m29 + m43 + m47 + m55 + m64 + m66 + m70 + m82 <= 11; s.t. pm641: m02 + m11 + m21 + m25 + m34 + m41 + m45 + m53 + m55 + m68 + m69 + m84 <= 11; s.t. pm642: m02 + m11 + m22 + m24 + m34 + m42 + m44 + m53 + m55 + m66 + m71 + m84 <= 11; s.t. pm643: m07 + m12 + m15 + m20 + m29 + m42 + m44 + m55 + m63 + m68 + m72 + m83 <= 11; s.t. pm644: m02 + m11 + m21 + m25 + m33 + m43 + m44 + m54 + m55 + m66 + m70 + m84 <= 11; s.t. pm645: m07 + m11 + m15 + m21 + m33 + m35 + m44 + m54 + m55 + m72 + m79 + m83 <= 11; s.t. pm646: m03 + m11 + m17 + m25 + m29 + m45 + m48 + m55 + m64 + m68 + m69 + m78 <= 11; s.t. pm647: m04 + m11 + m17 + m22 + m29 + m42 + m48 + m55 + m64 + m66 + m71 + m81 <= 11; s.t. pm648: m02 + m12 + m22 + m23 + m32 + m42 + m46 + m54 + m55 + m66 + m70 + m84 <= 11; s.t. pm649: m03 + m13 + m17 + m23 + m33 + m36 + m48 + m52 + m55 + m68 + m78 + m83 <= 11; s.t. pm650: m02 + m13 + m21 + m23 + m33 + m41 + m46 + m52 + m55 + m68 + m70 + m84 <= 11; s.t. pm651: m02 + m13 + m21 + m23 + m32 + m43 + m45 + m53 + m55 + m66 + m71 + m84 <= 11; s.t. pm652: m03 + m11 + m15 + m28 + m34 + m37 + m45 + m53 + m55 + m68 + m78 + m82 <= 11; s.t. pm653: m05 + m13 + m15 + m21 + m33 + m35 + m46 + m52 + m55 + m74 + m79 + m81 <= 11; s.t. pm654: m05 + m13 + m15 + m21 + m29 + m43 + m45 + m55 + m62 + m66 + m74 + m82 <= 11; s.t. pm655: m04 + m11 + m18 + m21 + m34 + m35 + m47 + m53 + m55 + m69 + m79 + m83 <= 11; s.t. pm656: m04 + m11 + m17 + m22 + m33 + m35 + m48 + m54 + m55 + m69 + m78 + m83 <= 11; s.t. pm657: m02 + m13 + m20 + m24 + m32 + m42 + m46 + m53 + m55 + m68 + m69 + m84 <= 11; s.t. pm658: m05 + m12 + m15 + m22 + m34 + m35 + m45 + m52 + m55 + m74 + m78 + m82 <= 11; s.t. pm659: m05 + m12 + m15 + m22 + m29 + m42 + m46 + m55 + m63 + m66 + m74 + m81 <= 11; s.t. pm660: m02 + m12 + m20 + m25 + m34 + m42 + m44 + m52 + m55 + m68 + m70 + m84 <= 11; s.t. pm661: m06 + m11 + m15 + m22 + m34 + m35 + m44 + m53 + m55 + m73 + m78 + m83 <= 11; s.t. pm662: m05 + m08 + m21 + m25 + m30 + m39 + m45 + m59 + m64 + m65 + m72 + m79 <= 11; s.t. pm663: m07 + m08 + m20 + m24 + m30 + m36 + m47 + m59 + m64 + m67 + m73 + m77 <= 11; s.t. pm664: m05 + m08 + m22 + m24 + m30 + m36 + m49 + m61 + m62 + m67 + m73 + m75 <= 11; s.t. pm665: m07 + m08 + m21 + m23 + m30 + m37 + m45 + m61 + m62 + m65 + m74 + m79 <= 11; s.t. pm666: m05 + m08 + m22 + m24 + m31 + m39 + m42 + m56 + m64 + m65 + m72 + m82 <= 11; s.t. pm667: m07 + m08 + m20 + m24 + m31 + m37 + m42 + m58 + m62 + m65 + m74 + m82 <= 11; s.t. pm668: m05 + m10 + m14 + m28 + m33 + m39 + m40 + m52 + m58 + m70 + m78 + m82 <= 11; s.t. pm669: m05 + m10 + m14 + m28 + m33 + m36 + m43 + m54 + m56 + m72 + m76 + m82 <= 11; s.t. pm670: m05 + m10 + m14 + m28 + m34 + m36 + m42 + m53 + m56 + m73 + m77 + m81 <= 11; s.t. pm671: m03 + m08 + m23 + m28 + m31 + m39 + m47 + m57 + m63 + m66 + m70 + m77 <= 11; s.t. pm672: m03 + m08 + m23 + m28 + m33 + m36 + m48 + m56 + m61 + m68 + m72 + m76 <= 11; s.t. pm673: m03 + m08 + m23 + m28 + m34 + m36 + m47 + m56 + m60 + m67 + m73 + m77 <= 11; s.t. pm674: m03 + m11 + m15 + m28 + m31 + m39 + m47 + m53 + m58 + m66 + m76 + m82 <= 11; s.t. pm675: m03 + m10 + m16 + m28 + m33 + m39 + m44 + m50 + m63 + m70 + m77 + m78 <= 11; s.t. pm676: m03 + m11 + m15 + m28 + m33 + m39 + m44 + m50 + m61 + m72 + m76 + m79 <= 11; s.t. pm677: m03 + m10 + m16 + m28 + m33 + m36 + m48 + m54 + m56 + m67 + m77 + m81 <= 11; s.t. pm678: m03 + m10 + m16 + m28 + m34 + m36 + m47 + m53 + m56 + m68 + m76 + m82 <= 11; s.t. pm679: m04 + m09 + m16 + m28 + m33 + m35 + m48 + m54 + m59 + m70 + m77 + m78 <= 11; s.t. pm680: m05 + m09 + m15 + m28 + m33 + m35 + m46 + m54 + m59 + m72 + m76 + m79 <= 11; s.t. pm681: m02 + m09 + m23 + m28 + m33 + m40 + m48 + m52 + m61 + m68 + m70 + m78 <= 11; s.t. pm682: m02 + m10 + m20 + m28 + m34 + m40 + m47 + m52 + m57 + m68 + m70 + m82 <= 11; s.t. pm683: m05 + m09 + m15 + m28 + m33 + m39 + m40 + m52 + m61 + m67 + m79 + m81 <= 11; s.t. pm684: m02 + m10 + m20 + m28 + m34 + m42 + m44 + m50 + m62 + m70 + m73 + m77 <= 11; s.t. pm685: m04 + m08 + m20 + m28 + m34 + m35 + m47 + m57 + m59 + m70 + m73 + m77 <= 11; s.t. pm686: m05 + m09 + m15 + m28 + m34 + m35 + m45 + m53 + m59 + m73 + m77 + m78 <= 11; s.t. pm687: m02 + m09 + m23 + m28 + m31 + m42 + m48 + m54 + m62 + m66 + m70 + m77 <= 11; s.t. pm688: m05 + m09 + m15 + m28 + m31 + m39 + m42 + m53 + m63 + m66 + m77 + m81 <= 11; s.t. pm689: m01 + m14 + m23 + m28 + m38 + m40 + m48 + m52 + m58 + m60 + m71 + m78 <= 11; s.t. pm690: m01 + m14 + m23 + m28 + m38 + m41 + m46 + m51 + m58 + m62 + m73 + m76 <= 11; s.t. pm691: m01 + m14 + m23 + m28 + m39 + m41 + m45 + m51 + m57 + m63 + m72 + m77 <= 11; s.t. pm692: m01 + m14 + m23 + m28 + m39 + m40 + m47 + m52 + m57 + m61 + m70 + m79 <= 11; s.t. pm693: m01 + m14 + m24 + m27 + m37 + m40 + m49 + m53 + m58 + m59 + m71 + m78 <= 11; s.t. pm694: m01 + m14 + m24 + m27 + m37 + m42 + m46 + m51 + m58 + m62 + m74 + m75 <= 11; s.t. pm695: m01 + m14 + m24 + m27 + m39 + m40 + m47 + m53 + m56 + m61 + m69 + m80 <= 11; s.t. pm696: m01 + m14 + m24 + m27 + m39 + m42 + m44 + m51 + m56 + m64 + m72 + m77 <= 11; s.t. pm697: m01 + m15 + m20 + m28 + m35 + m45 + m48 + m54 + m57 + m59 + m72 + m77 <= 11; s.t. pm698: m01 + m15 + m20 + m28 + m39 + m42 + m44 + m50 + m60 + m63 + m72 + m77 <= 11; s.t. pm699: m01 + m15 + m20 + m28 + m38 + m43 + m44 + m50 + m61 + m62 + m73 + m76 <= 11; s.t. pm700: m01 + m15 + m20 + m28 + m35 + m46 + m47 + m53 + m58 + m59 + m73 + m76 <= 11; s.t. pm701: m01 + m14 + m25 + m26 + m38 + m40 + m48 + m54 + m56 + m60 + m69 + m80 <= 11; s.t. pm702: m01 + m15 + m20 + m28 + m39 + m40 + m47 + m52 + m58 + m60 + m67 + m82 <= 11; s.t. pm703: m01 + m15 + m22 + m26 + m35 + m45 + m48 + m52 + m57 + m61 + m74 + m75 <= 11; s.t. pm704: m01 + m15 + m21 + m27 + m35 + m46 + m47 + m52 + m58 + m60 + m74 + m75 <= 11; s.t. pm705: m01 + m15 + m20 + m28 + m38 + m40 + m48 + m52 + m57 + m61 + m68 + m81 <= 11; s.t. pm706: m01 + m17 + m20 + m25 + m39 + m40 + m47 + m50 + m60 + m63 + m69 + m80 <= 11; s.t. pm707: m01 + m17 + m20 + m25 + m37 + m40 + m49 + m51 + m57 + m63 + m68 + m81 <= 11; s.t. pm708: m01 + m16 + m22 + m24 + m35 + m46 + m47 + m51 + m57 + m63 + m74 + m75 <= 11; s.t. pm709: m01 + m17 + m20 + m25 + m37 + m43 + m45 + m54 + m57 + m59 + m65 + m84 <= 11; s.t. pm710: m01 + m16 + m21 + m25 + m38 + m40 + m48 + m51 + m56 + m64 + m68 + m81 <= 11; s.t. pm711: m01 + m16 + m21 + m25 + m38 + m43 + m44 + m54 + m56 + m60 + m65 + m84 <= 11; s.t. pm712: m01 + m17 + m20 + m25 + m39 + m42 + m44 + m52 + m58 + m60 + m65 + m84 <= 11; s.t. pm713: m01 + m17 + m20 + m25 + m35 + m44 + m49 + m51 + m58 + m62 + m73 + m76 <= 11; s.t. pm714: m01 + m16 + m21 + m25 + m39 + m41 + m45 + m53 + m58 + m59 + m65 + m84 <= 11; s.t. pm715: m01 + m16 + m21 + m25 + m35 + m45 + m48 + m51 + m58 + m62 + m74 + m75 <= 11; s.t. pm716: m01 + m16 + m22 + m24 + m39 + m40 + m47 + m51 + m56 + m64 + m67 + m82 <= 11; s.t. pm717: m01 + m16 + m21 + m25 + m39 + m40 + m47 + m50 + m59 + m64 + m70 + m79 <= 11; s.t. pm718: m01 + m18 + m20 + m24 + m38 + m43 + m44 + m52 + m57 + m61 + m65 + m84 <= 11; s.t. pm719: m01 + m18 + m19 + m26 + m38 + m41 + m46 + m50 + m60 + m63 + m69 + m80 <= 11; s.t. pm720: m01 + m18 + m19 + m26 + m38 + m43 + m44 + m51 + m57 + m63 + m66 + m83 <= 11; s.t. pm721: m01 + m18 + m20 + m24 + m38 + m40 + m48 + m50 + m61 + m62 + m69 + m80 <= 11; s.t. pm722: m01 + m16 + m19 + m28 + m38 + m41 + m46 + m51 + m57 + m63 + m68 + m81 <= 11; s.t. pm723: m01 + m17 + m19 + m27 + m35 + m46 + m47 + m54 + m56 + m60 + m69 + m80 <= 11; s.t. pm724: m01 + m16 + m19 + m28 + m38 + m43 + m44 + m50 + m60 + m63 + m71 + m78 <= 11; s.t. pm725: m01 + m16 + m19 + m28 + m39 + m42 + m44 + m50 + m61 + m62 + m70 + m79 <= 11; s.t. pm726: m01 + m16 + m19 + m28 + m39 + m41 + m45 + m51 + m58 + m62 + m67 + m82 <= 11; s.t. pm727: m01 + m18 + m19 + m26 + m37 + m43 + m45 + m51 + m56 + m64 + m67 + m82 <= 11; s.t. pm728: m01 + m17 + m19 + m27 + m39 + m41 + m45 + m50 + m61 + m62 + m69 + m80 <= 11; s.t. pm729: m01 + m16 + m22 + m24 + m39 + m42 + m44 + m53 + m56 + m61 + m65 + m84 <= 11; s.t. pm730: m01 + m16 + m22 + m24 + m38 + m41 + m46 + m54 + m57 + m59 + m65 + m84 <= 11; s.t. pm731: m01 + m16 + m22 + m24 + m38 + m40 + m48 + m50 + m59 + m64 + m71 + m78 <= 11; s.t. pm732: m01 + m18 + m19 + m26 + m37 + m42 + m46 + m50 + m59 + m64 + m70 + m79 <= 11; s.t. pm733: m01 + m17 + m19 + m27 + m37 + m43 + m45 + m50 + m59 + m64 + m71 + m78 <= 11; s.t. pm734: m01 + m18 + m20 + m24 + m37 + m42 + m46 + m53 + m58 + m59 + m65 + m84 <= 11; s.t. pm735: m01 + m16 + m19 + m28 + m35 + m46 + m47 + m54 + m57 + m59 + m70 + m79 <= 11; s.t. pm736: m01 + m16 + m19 + m28 + m35 + m45 + m48 + m53 + m58 + m59 + m71 + m78 <= 11; s.t. pm737: m01 + m18 + m19 + m26 + m35 + m45 + m48 + m53 + m56 + m61 + m69 + m80 <= 11; s.t. pm738: m01 + m17 + m19 + m27 + m37 + m42 + m46 + m51 + m56 + m64 + m68 + m81 <= 11; s.t. pm739: m01 + m17 + m19 + m27 + m39 + m42 + m44 + m51 + m58 + m62 + m66 + m83 <= 11; s.t. pm740: m01 + m15 + m21 + m27 + m37 + m43 + m45 + m50 + m61 + m62 + m74 + m75 <= 11; s.t. pm741: m01 + m15 + m21 + m27 + m37 + m40 + m49 + m53 + m56 + m61 + m68 + m81 <= 11; s.t. pm742: m01 + m15 + m21 + m27 + m35 + m44 + m49 + m54 + m56 + m60 + m72 + m77 <= 11; s.t. pm743: m01 + m15 + m21 + m27 + m39 + m40 + m47 + m53 + m58 + m59 + m66 + m83 <= 11; s.t. pm744: m01 + m15 + m21 + m27 + m39 + m41 + m45 + m50 + m59 + m64 + m72 + m77 <= 11; s.t. pm745: m01 + m18 + m21 + m23 + m38 + m40 + m48 + m51 + m58 + m62 + m66 + m83 <= 11; s.t. pm746: m01 + m18 + m21 + m23 + m37 + m40 + m49 + m50 + m61 + m62 + m70 + m79 <= 11; s.t. pm747: m01 + m17 + m22 + m23 + m37 + m40 + m49 + m50 + m60 + m63 + m71 + m78 <= 11; s.t. pm748: m01 + m17 + m22 + m23 + m39 + m40 + m47 + m51 + m57 + m63 + m66 + m83 <= 11; s.t. pm749: m01 + m18 + m21 + m23 + m38 + m41 + m46 + m52 + m58 + m60 + m65 + m84 <= 11; s.t. pm750: m01 + m17 + m22 + m23 + m35 + m46 + m47 + m51 + m56 + m64 + m73 + m76 <= 11; s.t. pm751: m01 + m18 + m21 + m23 + m37 + m43 + m45 + m53 + m56 + m61 + m65 + m84 <= 11; s.t. pm752: m01 + m17 + m22 + m23 + m37 + m42 + m46 + m54 + m56 + m60 + m65 + m84 <= 11; s.t. pm753: m01 + m18 + m21 + m23 + m35 + m45 + m48 + m51 + m56 + m64 + m72 + m77 <= 11; s.t. pm754: m01 + m17 + m22 + m23 + m39 + m41 + m45 + m52 + m57 + m61 + m65 + m84 <= 11; s.t. pm755: m01 + m14 + m25 + m26 + m37 + m43 + m45 + m51 + m57 + m63 + m74 + m75 <= 11; s.t. pm756: m01 + m14 + m25 + m26 + m37 + m40 + m49 + m54 + m57 + m59 + m70 + m79 <= 11; s.t. pm757: m01 + m14 + m25 + m26 + m38 + m43 + m44 + m51 + m56 + m64 + m73 + m76 <= 11; s.t. pm758: m01 + m18 + m20 + m24 + m35 + m44 + m49 + m51 + m57 + m63 + m72 + m77 <= 11; s.t. pm759: m01 + m18 + m19 + m26 + m35 + m44 + m49 + m52 + m57 + m61 + m70 + m79 <= 11; s.t. pm760: m01 + m17 + m19 + m27 + m35 + m44 + m49 + m52 + m58 + m60 + m71 + m78 <= 11; s.t. pm761: m01 + m18 + m20 + m24 + m37 + m40 + m49 + m51 + m58 + m62 + m67 + m82 <= 11; s.t. pm762: m01 + m15 + m22 + m26 + m38 + m41 + m46 + m50 + m59 + m64 + m73 + m76 <= 11; s.t. pm763: m01 + m15 + m22 + m26 + m38 + m40 + m48 + m54 + m57 + m59 + m66 + m83 <= 11; s.t. pm764: m01 + m15 + m22 + m26 + m37 + m40 + m49 + m54 + m56 + m60 + m67 + m82 <= 11; s.t. pm765: m01 + m15 + m22 + m26 + m35 + m44 + m49 + m53 + m56 + m61 + m73 + m76 <= 11; s.t. pm766: m01 + m15 + m22 + m26 + m37 + m42 + m46 + m50 + m60 + m63 + m74 + m75 <= 11; s.t. pm767: m04 + m09 + m18 + m26 + m32 + m35 + m49 + m53 + m61 + m69 + m76 + m79 <= 11; s.t. pm768: m05 + m09 + m18 + m24 + m34 + m36 + m42 + m53 + m59 + m66 + m77 + m84 <= 11; s.t. pm769: m05 + m10 + m18 + m21 + m34 + m35 + m45 + m53 + m56 + m69 + m77 + m84 <= 11; s.t. pm770: m04 + m12 + m18 + m20 + m34 + m37 + m42 + m50 + m59 + m70 + m77 + m84 <= 11; s.t. pm771: m02 + m13 + m21 + m23 + m32 + m40 + m49 + m50 + m60 + m71 + m72 + m79 <= 11; s.t. pm772: m02 + m13 + m20 + m24 + m33 + m40 + m48 + m50 + m59 + m71 + m72 + m80 <= 11; s.t. pm773: m02 + m12 + m22 + m23 + m32 + m40 + m49 + m50 + m61 + m70 + m73 + m78 <= 11; s.t. pm774: m02 + m11 + m22 + m24 + m33 + m40 + m48 + m50 + m61 + m69 + m74 + m78 <= 11; s.t. pm775: m05 + m08 + m21 + m25 + m33 + m39 + m40 + m58 + m59 + m66 + m70 + m84 <= 11; s.t. pm776: m05 + m08 + m22 + m24 + m33 + m39 + m40 + m56 + m61 + m67 + m69 + m84 <= 11; s.t. pm777: m05 + m12 + m15 + m22 + m31 + m39 + m42 + m50 + m63 + m72 + m75 + m83 <= 11; s.t. pm778: m05 + m13 + m17 + m19 + m33 + m36 + m43 + m50 + m59 + m73 + m78 + m83 <= 11; s.t. pm779: m05 + m10 + m18 + m21 + m33 + m36 + m43 + m50 + m63 + m72 + m75 + m83 <= 11; s.t. pm780: m05 + m10 + m17 + m22 + m34 + m36 + m42 + m50 + m62 + m73 + m75 + m83 <= 11; s.t. pm781: m05 + m10 + m17 + m22 + m33 + m39 + m40 + m50 + m63 + m69 + m78 + m83 <= 11; s.t. pm782: m07 + m11 + m15 + m21 + m31 + m35 + m47 + m53 + m58 + m73 + m75 + m83 <= 11; s.t. pm783: m07 + m10 + m16 + m21 + m30 + m36 + m47 + m53 + m63 + m68 + m75 + m83 <= 11; s.t. pm784: m03 + m10 + m18 + m26 + m33 + m36 + m48 + m52 + m58 + m67 + m75 + m83 <= 11; s.t. pm785: m07 + m10 + m14 + m26 + m32 + m36 + m42 + m53 + m58 + m73 + m75 + m83 <= 11; s.t. pm786: m07 + m09 + m15 + m26 + m31 + m37 + m42 + m53 + m63 + m68 + m75 + m83 <= 11; s.t. pm787: m07 + m08 + m19 + m26 + m33 + m36 + m41 + m58 + m59 + m67 + m73 + m83 <= 11; s.t. pm788: m05 + m10 + m17 + m22 + m34 + m35 + m45 + m52 + m57 + m71 + m75 + m84 <= 11; s.t. pm789: m05 + m10 + m17 + m22 + m30 + m39 + m45 + m52 + m64 + m65 + m78 + m82 <= 11; s.t. pm790: m07 + m10 + m17 + m20 + m33 + m35 + m44 + m52 + m58 + m71 + m76 + m84 <= 11; s.t. pm791: m07 + m10 + m17 + m20 + m30 + m36 + m47 + m52 + m64 + m68 + m76 + m82 <= 11; s.t. pm792: m07 + m09 + m17 + m23 + m33 + m36 + m41 + m52 + m61 + m68 + m76 + m84 <= 11; s.t. pm793: m05 + m12 + m15 + m22 + m30 + m39 + m45 + m52 + m61 + m67 + m75 + m84 <= 11; s.t. pm794: m05 + m12 + m18 + m19 + m30 + m36 + m49 + m52 + m61 + m67 + m79 + m81 <= 11; s.t. pm795: m05 + m13 + m17 + m19 + m30 + m36 + m49 + m52 + m60 + m68 + m78 + m82 <= 11; s.t. pm796: m07 + m09 + m17 + m23 + m31 + m35 + m47 + m52 + m64 + m71 + m76 + m79 <= 11; s.t. pm797: m07 + m12 + m15 + m20 + m31 + m35 + m47 + m52 + m58 + m74 + m76 + m82 <= 11; s.t. pm798: m05 + m09 + m17 + m25 + m34 + m36 + m42 + m52 + m60 + m68 + m75 + m84 <= 11; s.t. pm799: m05 + m09 + m18 + m24 + m33 + m36 + m43 + m52 + m61 + m67 + m75 + m84 <= 11; s.t. pm800: m05 + m09 + m17 + m25 + m31 + m39 + m42 + m52 + m64 + m65 + m79 + m81 <= 11; s.t. pm801: m07 + m09 + m15 + m26 + m33 + m35 + m44 + m52 + m61 + m74 + m76 + m79 <= 11; s.t. pm802: m05 + m13 + m17 + m19 + m31 + m35 + m49 + m52 + m57 + m71 + m79 + m81 <= 11; s.t. pm803: m05 + m12 + m18 + m19 + m31 + m35 + m49 + m52 + m58 + m70 + m78 + m82 <= 11; s.t. pm804: m05 + m10 + m18 + m21 + m33 + m35 + m46 + m52 + m58 + m70 + m75 + m84 <= 11; s.t. pm805: m02 + m12 + m19 + m27 + m31 + m41 + m49 + m52 + m58 + m67 + m71 + m81 <= 11; s.t. pm806: m02 + m10 + m21 + m27 + m33 + m41 + m46 + m52 + m58 + m65 + m74 + m81 <= 11; s.t. pm807: m02 + m12 + m19 + m27 + m32 + m43 + m45 + m50 + m61 + m69 + m74 + m78 <= 11; s.t. pm808: m02 + m10 + m21 + m27 + m34 + m41 + m45 + m50 + m62 + m69 + m74 + m77 <= 11; s.t. pm809: m02 + m10 + m21 + m27 + m32 + m43 + m45 + m50 + m64 + m71 + m72 + m75 <= 11; s.t. pm810: m02 + m12 + m19 + m27 + m34 + m41 + m45 + m50 + m59 + m71 + m72 + m80 <= 11; s.t. pm811: m02 + m10 + m21 + m27 + m32 + m40 + m49 + m53 + m58 + m66 + m71 + m81 <= 11; s.t. pm812: m02 + m10 + m21 + m27 + m33 + m43 + m44 + m54 + m56 + m65 + m72 + m83 <= 11; s.t. pm813: m02 + m12 + m19 + m27 + m32 + m42 + m46 + m51 + m58 + m66 + m74 + m81 <= 11; s.t. pm814: m02 + m12 + m19 + m27 + m34 + m42 + m44 + m51 + m56 + m68 + m72 + m83 <= 11; s.t. pm815: m02 + m11 + m21 + m25 + m31 + m43 + m47 + m50 + m64 + m70 + m73 + m75 <= 11; s.t. pm816: m02 + m13 + m19 + m26 + m33 + m41 + m46 + m50 + m59 + m70 + m73 + m80 <= 11; s.t. pm817: m02 + m13 + m21 + m23 + m31 + m41 + m49 + m50 + m62 + m70 + m73 + m77 <= 11; s.t. pm818: m02 + m13 + m20 + m24 + m31 + m42 + m48 + m50 + m62 + m69 + m74 + m77 <= 11; s.t. pm819: m02 + m13 + m19 + m26 + m32 + m42 + m46 + m50 + m60 + m69 + m74 + m79 <= 11; s.t. pm820: m02 + m13 + m19 + m26 + m30 + m44 + m49 + m52 + m60 + m67 + m71 + m79 <= 11; s.t. pm821: m05 + m10 + m17 + m22 + m33 + m35 + m46 + m54 + m56 + m69 + m76 + m84 <= 11; s.t. pm822: m05 + m13 + m14 + m24 + m31 + m39 + m42 + m53 + m56 + m69 + m77 + m84 <= 11; s.t. pm823: m05 + m13 + m15 + m21 + m31 + m35 + m49 + m53 + m56 + m73 + m77 + m81 <= 11; s.t. pm824: m05 + m12 + m15 + m22 + m31 + m35 + m49 + m54 + m56 + m72 + m76 + m82 <= 11; s.t. pm825: m07 + m12 + m16 + m19 + m31 + m35 + m47 + m54 + m56 + m70 + m80 + m82 <= 11; s.t. pm826: m07 + m10 + m16 + m21 + m33 + m35 + m44 + m54 + m56 + m70 + m77 + m84 <= 11; s.t. pm827: m07 + m10 + m16 + m21 + m32 + m35 + m45 + m53 + m58 + m71 + m75 + m84 <= 11; s.t. pm828: m07 + m12 + m16 + m19 + m32 + m36 + m42 + m50 + m61 + m74 + m79 + m81 <= 11; s.t. pm829: m07 + m09 + m15 + m26 + m32 + m35 + m45 + m53 + m61 + m73 + m75 + m80 <= 11; s.t. pm830: m05 + m09 + m17 + m25 + m31 + m35 + m49 + m54 + m62 + m69 + m76 + m79 <= 11; s.t. pm831: m05 + m09 + m17 + m25 + m33 + m36 + m43 + m54 + m59 + m66 + m76 + m84 <= 11; s.t. pm832: m07 + m09 + m17 + m23 + m32 + m36 + m42 + m54 + m60 + m66 + m77 + m84 <= 11; s.t. pm833: m07 + m11 + m17 + m19 + m31 + m37 + m42 + m50 + m64 + m71 + m79 + m81 <= 11; s.t. pm834: m07 + m11 + m14 + m24 + m31 + m37 + m42 + m53 + m58 + m71 + m75 + m84 <= 11; s.t. pm835: m07 + m11 + m17 + m19 + m33 + m36 + m41 + m50 + m61 + m73 + m80 + m81 <= 11; s.t. pm836: m07 + m09 + m16 + m24 + m32 + m36 + m42 + m53 + m61 + m68 + m75 + m84 <= 11; s.t. pm837: m07 + m09 + m16 + m24 + m33 + m36 + m41 + m54 + m59 + m67 + m77 + m84 <= 11; s.t. pm838: m07 + m12 + m14 + m23 + m31 + m37 + m42 + m54 + m56 + m70 + m77 + m84 <= 11; s.t. pm839: m07 + m10 + m17 + m20 + m32 + m36 + m42 + m50 + m64 + m73 + m77 + m81 <= 11; s.t. pm840: m07 + m10 + m17 + m20 + m32 + m35 + m45 + m54 + m57 + m69 + m77 + m84 <= 11;