3人対戦ゲームの試合数・対戦表

2020/11/15 18:57 整数計画問題
数学でこんな問題がありました。

・3人で行うゲームがある
・9人が参加する
・各プレイヤーは4回だけプレイできて、さらに他のすべてのプレイヤーとちょうど1回ずつプレイする
・このような条件をみたすゲームの個数(=試合数)は何通りあるか、対戦表は作れるか

この問題を整数計画問題として GLPK (Gnu Linear Programming Kit) を使って解いてみたので、これで正解なのか自信がありませんが私なりの解答を披露したいと思います。

#Yahoo!知恵袋 でも、同じ問題の答えを聞いている人がいました(こちらこちら)。
#前者の回答例は、私の解答での m02,m12,m22,m23,m30,m46,m47,m51,m63,m66,m74,m76 パターンで、対戦表では No. 352 にあたります。

まず、9人に1,2,3,・・・,9と番号を付ける。
9人のうち3人でゲームをするから、その組み合わせは 9C3で、84通りある。
この組み合わせにも番号を付け、それぞれ m01, m02, ..., m84 と表す。
一覧は次の通り。
m01  [1 x 2 x 3]
m02  [1 x 2 x 4]
m03  [1 x 2 x 5]
m04  [1 x 2 x 6]
m05  [1 x 2 x 7]
m06  [1 x 2 x 8]
m07  [1 x 2 x 9]
m08  [1 x 3 x 4]
m09  [1 x 3 x 5]
m10  [1 x 3 x 6]
m11  [1 x 3 x 7]
m12  [1 x 3 x 8]
m13  [1 x 3 x 9]
m14  [1 x 4 x 5]
m15  [1 x 4 x 6]
m16  [1 x 4 x 7]
m17  [1 x 4 x 8]
m18  [1 x 4 x 9]
m19  [1 x 5 x 6]
m20  [1 x 5 x 7]
m21  [1 x 5 x 8]
m22  [1 x 5 x 9]
m23  [1 x 6 x 7]
m24  [1 x 6 x 8]
m25  [1 x 6 x 9]
m26  [1 x 7 x 8]
m27  [1 x 7 x 9]
m28  [1 x 8 x 9]
m29  [2 x 3 x 4]
m30  [2 x 3 x 5]
m31  [2 x 3 x 6]
m32  [2 x 3 x 7]
m33  [2 x 3 x 8]
m34  [2 x 3 x 9]
m35  [2 x 4 x 5]
m36  [2 x 4 x 6]
m37  [2 x 4 x 7]
m38  [2 x 4 x 8]
m39  [2 x 4 x 9]
m40  [2 x 5 x 6]
m41  [2 x 5 x 7]
m42  [2 x 5 x 8]
m43  [2 x 5 x 9]
m44  [2 x 6 x 7]
m45  [2 x 6 x 8]
m46  [2 x 6 x 9]
m47  [2 x 7 x 8]
m48  [2 x 7 x 9]
m49  [2 x 8 x 9]
m50  [3 x 4 x 5]
m51  [3 x 4 x 6]
m52  [3 x 4 x 7]
m53  [3 x 4 x 8]
m54  [3 x 4 x 9]
m55  [3 x 5 x 6]
m56  [3 x 5 x 7]
m57  [3 x 5 x 8]
m58  [3 x 5 x 9]
m59  [3 x 6 x 7]
m60  [3 x 6 x 8]
m61  [3 x 6 x 9]
m62  [3 x 7 x 8]
m63  [3 x 7 x 9]
m64  [3 x 8 x 9]
m65  [4 x 5 x 6]
m66  [4 x 5 x 7]
m67  [4 x 5 x 8]
m68  [4 x 5 x 9]
m69  [4 x 6 x 7]
m70  [4 x 6 x 8]
m71  [4 x 6 x 9]
m72  [4 x 7 x 8]
m73  [4 x 7 x 9]
m74  [4 x 8 x 9]
m75  [5 x 6 x 7]
m76  [5 x 6 x 8]
m77  [5 x 6 x 9]
m78  [5 x 7 x 8]
m79  [5 x 7 x 9]
m80  [5 x 8 x 9]
m81  [6 x 7 x 8]
m82  [6 x 7 x 9]
m83  [6 x 8 x 9]
m84  [7 x 8 x 9]

このm01~m84を複数組み合わせて(ただし個々のゲームは0回ないし1回だけ行われる)、
 条件1 各プレーヤーは4回だけプレイする
 条件2 他のすべてのプレイヤーとちょうど1回ずつプレイする
の両条件を満たすゲームの組み合わせを考える。

仮に12ゲーム必要なのだとしても(各プレイヤーが4回ずつ、1回のゲームで1/3の人しかプレイできないので 4×3=12より)、
84C12 = 112,992,892,764,570
と百兆を超えるとても大きな数となり、手作業で考えるのはとうてい無理なので、コンピュータをつかう。

GLPKに与えるモデルファイルは次の通り。

game3.mod.txt
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;
m** が、それぞれのゲームが行われる回数(0または1回)を表している。
st1~9 で各人がちょうど4回だけプレイする(条件1)こと、st12~89 で同じ人とはちょうど1度だけプレイすること(条件2)を制約している。
st** の 十の位・一の位の数字でおのおのプレイヤーを表している。

次のように実行する。
glpsol -m game3.mod.txt -o game3.out.txt

実行結果 game3.out.txt の内容は次の通り。
Problem:    first
Rows:       46
Columns:    84 (84 integer, 84 binary)
Non-zeros:  588
Status:     INTEGER OPTIMAL
Objective:  z = 12 (MINimum)

   No.   Row name        Activity     Lower bound   Upper bound
------ ------------    ------------- ------------- -------------
     1 z                          12                             
     2 st1                         4             4             = 
     3 st2                         4             4             = 
     4 st3                         4             4             = 
     5 st4                         4             4             = 
     6 st5                         4             4             = 
     7 st6                         4             4             = 
     8 st7                         4             4             = 
     9 st8                         4             4             = 
    10 st9                         4             4             = 
    11 st12                        1             1             = 
    12 st13                        1             1             = 
    13 st14                        1             1             = 
    14 st15                        1             1             = 
    15 st16                        1             1             = 
    16 st17                        1             1             = 
    17 st18                        1             1             = 
    18 st19                        1             1             = 
    19 st23                        1             1             = 
    20 st24                        1             1             = 
    21 st25                        1             1             = 
    22 st26                        1             1             = 
    23 st27                        1             1             = 
    24 st28                        1             1             = 
    25 st29                        1             1             = 
    26 st34                        1             1             = 
    27 st35                        1             1             = 
    28 st36                        1             1             = 
    29 st37                        1             1             = 
    30 st38                        1             1             = 
    31 st39                        1             1             = 
    32 st45                        1             1             = 
    33 st46                        1             1             = 
    34 st47                        1             1             = 
    35 st48                        1             1             = 
    36 st49                        1             1             = 
    37 st56                        1             1             = 
    38 st57                        1             1             = 
    39 st58                        1             1             = 
    40 st59                        1             1             = 
    41 st67                        1             1             = 
    42 st68                        1             1             = 
    43 st69                        1             1             = 
    44 st78                        1             1             = 
    45 st79                        1             1             = 
    46 st89                        1             1             = 

   No. Column name       Activity     Lower bound   Upper bound
------ ------------    ------------- ------------- -------------
     1 m01          *              0             0             1 
     2 m02          *              0             0             1 
     3 m03          *              0             0             1 
     4 m04          *              1             0             1 
     5 m05          *              0             0             1 
     6 m06          *              0             0             1 
     7 m07          *              0             0             1 
     8 m08          *              0             0             1 
     9 m09          *              0             0             1 
    10 m10          *              0             0             1 
    11 m11          *              0             0             1 
    12 m12          *              1             0             1 
    13 m13          *              0             0             1 
    14 m14          *              1             0             1 
    15 m15          *              0             0             1 
    16 m16          *              0             0             1 
    17 m17          *              0             0             1 
    18 m18          *              0             0             1 
    19 m19          *              0             0             1 
    20 m20          *              0             0             1 
    21 m21          *              0             0             1 
    22 m22          *              0             0             1 
    23 m23          *              0             0             1 
    24 m24          *              0             0             1 
    25 m25          *              0             0             1 
    26 m26          *              0             0             1 
    27 m27          *              1             0             1 
    28 m28          *              0             0             1 
    29 m29          *              0             0             1 
    30 m30          *              0             0             1 
    31 m31          *              0             0             1 
    32 m32          *              0             0             1 
    33 m33          *              0             0             1 
    34 m34          *              1             0             1 
    35 m35          *              0             0             1 
    36 m36          *              0             0             1 
    37 m37          *              0             0             1 
    38 m38          *              1             0             1 
    39 m39          *              0             0             1 
    40 m40          *              0             0             1 
    41 m41          *              1             0             1 
    42 m42          *              0             0             1 
    43 m43          *              0             0             1 
    44 m44          *              0             0             1 
    45 m45          *              0             0             1 
    46 m46          *              0             0             1 
    47 m47          *              0             0             1 
    48 m48          *              0             0             1 
    49 m49          *              0             0             1 
    50 m50          *              0             0             1 
    51 m51          *              0             0             1 
    52 m52          *              1             0             1 
    53 m53          *              0             0             1 
    54 m54          *              0             0             1 
    55 m55          *              1             0             1 
    56 m56          *              0             0             1 
    57 m57          *              0             0             1 
    58 m58          *              0             0             1 
    59 m59          *              0             0             1 
    60 m60          *              0             0             1 
    61 m61          *              0             0             1 
    62 m62          *              0             0             1 
    63 m63          *              0             0             1 
    64 m64          *              0             0             1 
    65 m65          *              0             0             1 
    66 m66          *              0             0             1 
    67 m67          *              0             0             1 
    68 m68          *              0             0             1 
    69 m69          *              0             0             1 
    70 m70          *              0             0             1 
    71 m71          *              1             0             1 
    72 m72          *              0             0             1 
    73 m73          *              0             0             1 
    74 m74          *              0             0             1 
    75 m75          *              0             0             1 
    76 m76          *              0             0             1 
    77 m77          *              0             0             1 
    78 m78          *              0             0             1 
    79 m79          *              0             0             1 
    80 m80          *              1             0             1 
    81 m81          *              1             0             1 
    82 m82          *              0             0             1 
    83 m83          *              0             0             1 
    84 m84          *              0             0             1 

Integer feasibility conditions:

KKT.PE: max.abs.err = 0.00e+00 on row 0
        max.rel.err = 0.00e+00 on row 0
        High quality

KKT.PB: max.abs.err = 0.00e+00 on row 0
        max.rel.err = 0.00e+00 on row 0
        High quality

End of output
これから、仮定の通り12ゲーム必要であり、その組み合わせは、
m04, m12, m14, m27, m34, m38, m41, m52, m55, m71, m80, m81
であることがわかった(Activity が1となっている m** の行を拾う)。
対戦表にすると、
[ 1 x 2 x 6 ] [ 1 x 3 x 8 ] [ 1 x 4 x 5 ] [ 1 x 7 x 9 ] [ 2 x 3 x 9 ] [ 2 x 4 x 8 ] 
[ 2 x 5 x 7 ] [ 3 x 4 x 7 ] [ 3 x 5 x 6 ] [ 4 x 6 x 9 ] [ 5 x 8 x 9 ] [ 6 x 7 x 8 ] 
となる。
組み合わせのパターンは複数あると思われるので、1度出たパターンは2度と現れないようにしてもう1度問題を解いてゆく。
具体的には、モデルファイルの末尾に
s.t. pm1: m04 + m12 + m14 + m27 + m34 + m38 + m41 + m52 + m55 + m71 + m80 + m81 <= 11;
を追記して、解く。

この、得られた解が現れないようにする制約式を、追記をしてはまた解くということを、解が得られなくなるまで繰り返す。

そうしたところ、840個の解が得られた後、解を返さなくなった。
最終的に得られたモデルファイルは、次の通り。
joined.mod.txt
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;
問題の「ゲームの個数(=試合数)は何通りあるか」には少々文意がつかみかねるが、
「840通り」と答えた。

対戦表は、こちら→ 対戦表.txt



もちろん、840回もあるので、繰り返しは手作業では行っていません。
Perl で書いたツールで自動化しています。

sol.pl
use strict;

unlink('prev_match_pattern.txt');

system('glpsol -m game3.mod.txt -o game3.out.txt');

for(my $i = 1; $i <= 1000; $i++){
	print"\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n";
	print "■■■■■ $i ■■■■■\n";

	system('type game3.out.txt | perl pattern.pl >> prev_match_pattern.txt');
	system('type prev_match_pattern.txt | perl make_st_prev_match_pattern.pl > st_prev_match.txt');

	system('copy game3.mod.txt + st_prev_match.txt joined.mod.txt');

	system('glpsol -m joined.mod.txt -o game3.out.txt');
}
pattern.pl
use strict;

my @matches;
foreach my $line (<>){
	chomp($line);

	if($line =~ /(m\d\d)\s+\*\s+(\d)/){
		push(@matches, $1) if($2 == 1);
	}
}

print join(',', @matches). "\n";
make_st_prev_match_pattern.pl
use strict;

my $i = 1;
foreach my $line (<>){
	chomp $line;
	my @mts = split(/,/, $line);
	print "s.t. pm$i: ". join(' + ', @mts). " <= 11;\n";

	$i++;
}
制約式を生成するスクリプト st.pl
#!/usr/bin/perl

use strict;
use warnings;
use Math::Combinatorics;

my @matches;
push @matches, '0';
open(LIST, '9c3.txt');
foreach my $line(<LIST>){
	chomp $line;
	push @matches, $line;
}
close(LIST);


for(my $player = 1; $player <= 9; $player++){
	my @joined_match;
	print "s.t. st$player: ";
	for(my $match = 1; $match <= 84; $match++){
		if($matches[$match] =~ /$player/){
			push @joined_match, sprintf('m%02d', $match);
		}
	}
	
	print join(' + ', @joined_match). " = 4;\n";
}



my @combine = combine(2, 1..9);
@combine = sort {$a->[0] <=> $b->[0]} @combine;
foreach my $a_comb (@combine) {
	my @hit_match;
    my($p1, $p2) = @$a_comb;
    ($p1, $p2) = sort ($p1, $p2);
	print "s.t. st${p1}${p2}: ";
	for(my $match = 1; $match <= 84; $match++){
		if($matches[$match] =~ /$p1/ && $matches[$match] =~ /$p2/){
			push @hit_match, sprintf('m%02d', $match);
		}
	}
	
	print join(' + ', @hit_match). " = 1;\n";
}
組み合わせ(9C3)データファイル 9c3.txt
(1,2,3)
(1,2,4)
(1,2,5)
(1,2,6)
(1,2,7)
(1,2,8)
(1,2,9)
(1,3,4)
(1,3,5)
(1,3,6)
(1,3,7)
(1,3,8)
(1,3,9)
(1,4,5)
(1,4,6)
(1,4,7)
(1,4,8)
(1,4,9)
(1,5,6)
(1,5,7)
(1,5,8)
(1,5,9)
(1,6,7)
(1,6,8)
(1,6,9)
(1,7,8)
(1,7,9)
(1,8,9)
(2,3,4)
(2,3,5)
(2,3,6)
(2,3,7)
(2,3,8)
(2,3,9)
(2,4,5)
(2,4,6)
(2,4,7)
(2,4,8)
(2,4,9)
(2,5,6)
(2,5,7)
(2,5,8)
(2,5,9)
(2,6,7)
(2,6,8)
(2,6,9)
(2,7,8)
(2,7,9)
(2,8,9)
(3,4,5)
(3,4,6)
(3,4,7)
(3,4,8)
(3,4,9)
(3,5,6)
(3,5,7)
(3,5,8)
(3,5,9)
(3,6,7)
(3,6,8)
(3,6,9)
(3,7,8)
(3,7,9)
(3,8,9)
(4,5,6)
(4,5,7)
(4,5,8)
(4,5,9)
(4,6,7)
(4,6,8)
(4,6,9)
(4,7,8)
(4,7,9)
(4,8,9)
(5,6,7)
(5,6,8)
(5,6,9)
(5,7,8)
(5,7,9)
(5,8,9)
(6,7,8)
(6,7,9)
(6,8,9)
(7,8,9)