{
"cells": [
{
"cell_type": "markdown",
"id": "95a492d4",
"metadata": {
"tags": [
"CSP",
"academic",
"easy",
"AllDifferent",
"symmetry-breaking"
]
},
"source": [
"# Problem *All-Interval Series*"
]
},
{
"cell_type": "markdown",
"id": "ec926be8",
"metadata": {},
"source": [
"Given the twelve standard pitch-classes (c, c\\#, d, $\\dots$), represented by numbers $0,1,\\dots,11$, find a series in which each pitch-class occurs exactly once and in which the musical intervals between neighboring notes cover the full set of intervals from the minor second (1 semitone) to the major seventh (11 semitones). \n",
"That is, for each of the intervals, there is a pair of neighboring pitch-classes in the series, between which this interval appears. See [CSPLib (Problem 07)](https://www.csplib.org/Problems/prob007/) "
]
},
{
"attachments": {
"Carter_all-interval_sets.png": {
"image/png": "iVBORw0KGgoAAAANSUhEUgAABFEAAAKRCAMAAACr/8YbAAAABGdBTUEAANkDQtZPoQAAAwBQTFRF/////v7+/f39/Pz8+/v7+vr6+fn5+Pj49/f39vb29fX19PT08/Pz8vLy8fHx8PDw7+/v7u7u7e3t7Ozs6+vr6urq6enp6Ojo5+fn5ubm5eXl5OTk4+Pj4uLi4eHh4ODg39/f3t7e3d3d3Nzc29vb2tra2dnZ2NjY19fX1tbW1dXV1NTU09PT0tLS0dHR0NDQz8/Pzs7Ozc3NzMzMy8vLysrKycnJyMjIx8fHxsbGxcXFxMTEw8PDwsLCwcHBwMDAv7+/vr6+vb29vLy8u7u7urq6ubm5uLi4t7e3tra2tbW1tLS0s7OzsrKysbGxsLCwr6+vrq6ura2trKysq6urqqqqqampqKiop6enpqampaWlpKSko6OjoqKioaGhoKCgn5+fnp6enZ2dnJycm5ubmpqamZmZmJiYl5eXlpaWlZWVlJSUk5OTkpKSkZGRkJCQj4+Pjo6OjY2NjIyMi4uLioqKiYmJiIiIh4eHhoaGhYWFhISEg4ODgoKCgYGBgICAf39/fn5+fX19fHx8e3t7enp6eXl5eHh4d3d3dnZ2dXV1dHR0c3NzcnJycXFxcHBwb29vbm5ubW1tbGxsa2trampqaWlpaGhoZ2dnZmZmZWVlZGRkY2NjYmJiYWFhYGBgX19fXl5eXV1dXFxcW1tbWlpaWVlZWFhYV1dXVlZWVVVVVFRUU1NTUlJSUVFRUFBQT09PTk5OTU1NTExMS0tLSkpKSUlJSEhIR0dHRkZGRUVFREREQ0NDQkJCQUFBQEBAPz8/Pj4+PT09PDw8Ozs7Ojo6OTk5ODg4Nzc3NjY2NTU1NDQ0MzMzMjIyMTExMDAwLy8vLi4uLS0tLCwsKysrKioqKSkpKCgoJycnJiYmJSUlJCQkIyMjIiIiISEhICAgHx8fHh4eHR0dHBwcGxsbGhoaGRkZGBgYFxcXFhYWFRUVFBQUExMTEhISEREREBAQDw8PDg4ODQ0NDAwMCwsLCgoKCQkJCAgIBwcHBgYGBQUFBAQEAwMDAgICAQEBAAAA7q7hlAAAAAlwSFlzAAALEwAACxMBAJqcGAAAACR0RVh0U29mdHdhcmUAUXVpY2tUaW1lIDcuNi40IChNYWMgT1MgWCkAwNfq4wAAAAd0SU1FB9oJGRYKMwLkudMAACAASURBVHic7J0HmNVU2sczwwxlaILMqBQBBaWoCCKILKKuiAUbiIgNVFxFFEVFWFFEXFHUD9HFsrbFXlcRFUEpiwXssBQRRpAiHQakzQwzc98vvZ7k5iQn7d739zxKcpLzPyfJuf+5yX3zHo5DEARBEARBEARBEARBEARBEARBEARBEARBEARBEARBEARBEARBEARBEARBEARBEARBIqbaMZdUj7oPCIJkAK0uuueNxaWwKup+IAgSLX9dI7FY//Xi32sU7nQlkvP9tM3AM5mi4efXkCmuQ9V/BEHiRG5Rlwf2Cm7QX1dYrajPbr7o0061xdXGo/vkptPJ+5mvcDZFw9XqnVEstFuyRGR58fqDwip8TXkAPnFzbAiC0HDsdv6T/Lmx7FGAR3OkxcPLAZ5LK/I0wP4adO1eKTjIHepqztm/8Ov30Gn4xN2xIQhCw1X8JznV0lB0G6xT7oNG8lv3pTWLlQDTKZu9QHCUY3QFeS8DdKAU8Ye7Y0MQhIb7hI/2PwxFk+HvyuLZ/MYf00kcxe90E3lTnXo2dYbzdYwPcw+p/CNdQ7bYNuOEq2NDEISKBVX8B2tjNX3RD9BKWcx54s/ve6STGMYrHEncUvOXv9nUeYev83/GotXPp2vIDvtmnHB1bAiC0NCw8pNf+Q/3Bbqi+pX/0625CDP5BGAZecskaEbekLOFb/QMY9kfF6dvirKZNGAIDYIw5nK4+S4wPgbpBw9TSdQ8APAoccvpqaU2dU7i29ydbyiqtt/rb8f2zSAIEi6vQMvCgwCVTbSiF+E0KolzeHc4nbThuJ02TsNxY/k67xiLqrWlatVVMwiChErOll857l3+432vVrZxdx6VxpMAf+YTyttttnEanm/5Jq9S15rnUDXovhkEQULlJHiC43rxH+/f1VivDvC+bocaxxs/7Yd3b1fbpFEMSo28E2uppfn3lALsITkNT1EV/7XoUGWt++/WPY5qI/3bRPfIt2FzWbpjzTTNEGrntOjRTjjGY7RHLuZjE5o45cSGulVCJQRB7LlXiHXN+V0f8zoarhf/rd356oenrapcqe18/Cs//FnGfyNYf1tNnURrvvJ1wkKT9/ZCyUip8JjHxdD8XZ988slfCM1eow+QzV/2rGlzyzd3QdXKO7gTf94LVwoFecdd8cinG+AGYfnIaQdg5yiHZiy1eeo+uQ8q4I/Hel6950LisfFUu3zejoO81X15CrkSgiDp+Ga/YA738p/K95Si+SA+U6m1br4QxgpPKuWHPl0Js84p4BrzN0nbFgt8I36vGQ6QOoL/98pdwu4H6oo7T16wQPgJaeWCBQsaE5oVfjseLS/nPAfGz2uNiWV/3tas+jmbBj4CUNWIL7l2rRi0L3Zs8J/CUllDu2astXmaboCFg+oVXrdXErEcG0/eLWuqnuldu/E/APa2I1VCECQdDSo/Ef5pUglwsFAqql+h/Xb8Cf9ZOkdePr0E4FPx59acr0BCrMt9BvAz/89d8MdLf/CFlyqV7zMFxerIE8ynvbR81BtQbviRp+4cWNpUWBjw80qAb+VSIbR3Ef/vKPj9n+v45attmiHWzpkLG0WnO6ECthCOjafhbNj0V2Ehd4McKEOqhCCIEwNgmPjvdP7jdZdU1A8eUTe/BlAqPxlpug3gOzlkXYig/98rr7wiBrEUlIoht0NSD+RwN/Eb1N+JFgAU2zR7Gr/fwUk8z33wI784W7+t0Q+wVvq+UVNwrfvl4pZSZO/1laOlZlTjMjZDrt1d/Qr2PHxqPTae9qvhZ9lS5wL8264SgiBOTIWjxH8Fj/hVKnoReqqbVwHMlJaqCz/O9JaLW/HLryj7nMevnMqdVno5v/wAv6w82Dy0ynhXoWciGNCnTSj6FbYrXzl28ttOlpf7i8302CN8rRjPLx9PbMam9q3S1yiezvCg5dh42u6BP4+WFvP3ANxiVwlBEAdyNsvPJqv9oX672Kj9EtycL7xdWvwbv/iTUn6M8B1FWZkCsKPaEVtvFZanAWxUyq9wyHCwjN92/VFHHdWqy4UvlQG0023iJQYpy/y3n63KT1D/4pvJPXzzAGGZ/0ZVovxKY2zGpvZogKqTxKW6cLHl2Diu1lKAy+Xlu3nxw2wqIQjiRCc1T9KD/AfsNWGhA/xH3SzYyLHSIn+PIP3lFrhEby9rAN7InSvpbAT4SCl/3f7F3hZ8ffXZyVWwTrfpGv7eSjGL+vxur+qaeT13tvg0V4jg/5DYjF3tv/DLxdKP1b81sxwbx72k7XrcfvmXK1IlBEGcGKPeyLRIAZQ24IS/zEPUzfxffCVShP9Aw1+V8kn8yhR5+Vh++cp7F4nfa07QvYOcu13nLiZu1j87ydmry1HSbDekuiornUD75tCWXx44Zk6OUn4DqRnb2jWE34fmG97i0R2b6JAdpcVTdkLFzbaVEARx4usDamDJLP7jI9y5zIemSlH1fQBypEie8IKysqH6Nn7lCnllBH9v0Lu0k7g8WvcO8in88o02zX5qeHay8SJty38APlBX/g5QqTyVuZNfPmub9FXhXl1fDM3Y1haeicjfwazHxnE/AiwRF2rcvQ9KzrKthCCIEw0qtd8w+kvPRupXLFGLhFBa5dMuhG8cIS8L6dd+VO40PgdYtPwxaXk+gPrKnvCQ1uZeodYBfpv6Ek8d3W/HR/LG1Udd+wrgG2V5Dt/k8sHS8je6pzj6Zuxrc7lzBHcYp/VBf2ynyQZXb/DvsOvBRvaVEARx4jLt0Yj0xaMr1w8mqkVP6J52TOC3nivv+QPALiXpW+0y/m7p9wJxuX4FaLV/0H3sTQi/Dmlx9w2v07bwrWxR3ylqn9LeNqp7EODAAukRSUPeONSXo/XN2NbmaSTEsKj3eMZj+4j/NnPyuSOnl6V+HllX31FzJQRBnPg3HK2tPMZ/eF7gXtS9dLcSYK6yXOs3gO/FX05qzgDYoX7KxOSO50nLl+qiUQ5LgW1OhKf5/Z4mbRBc7XF17S1+t07ycl9+uUpeGcgvK4mS9M3Y1xY4qZQv+OMQwrHVqBTE13w2eWChuUOmSgiCOJCzWZ+WUXjEureu7rfjo/mCu9XNrRYDzDiSq3Phl1D1rPYy3bOgPbt4mf/uonxHGMSXk17oEVjLbzuftOFC7YsQxx3PfxXZrPxw8yK/Rcnw9hpAiZJyTt+MfW2R6wTvU75C6Y+tPb/8hf5FJbtKCII40dEYgTZf+AVH92hTyAR7gra51v383/WN5dtmPaz/0y+4gxS0weVs0qU8eUf3sTchfIJLC0hb/g5aQH3+IpBjV2XplJypUvh1521SM3a1lVelX+KLtudbj034/vOyuSukSgiCOHGP9iddQEyKr/4sy3Ez+S/8hv3P+/2bG5oaSrh2fJ3/yssdQQsvq7YL4C2bZu8GfbSqHv5LTqXy6Z0g3ItcppP+TF7uyi9fQ2rGpnazXXLZIVtBDabTH5uQwu4NU0+IlRAEceKHSsNzyJoloP99pqAM4CX+X+UZbNdFS7tbJIRPo/Lzyj28IRVxXJGwfCpI7/IdbanBcQtBP1GPnq8B9shRrpds/IA3COUJxr26+6RxUjOFlmZsal8Iyq83o8RAfsuxXc4X/6LrRe3ryZUQBHGiuRb3KvEU6H795fpIf+WHzpWeRlx7cCdhBos5ABuUpxXzAL7nuCvFX2TG8JUP57grVlpvGJqkwG5inqXqM9eeOzovFae+aCaGmC0AWKOE438tlp/+fTVzMza1x0I3ueZfeJepbT024S4spQahcCeuGM8RKyEI4sRYc6JXIeRVS9j6BL9WyPX6QfpL37IMqs60SAg/6irBs7XKhNiN8zeI90UzxT/73XaeYKkihsEdJD9i+Yjf9ISwcM3+i4RfYCZxNb4V3r0R3gYcJ+9T+6DwqPSYlUdZmrGp/QG/INEFYAHh2Kot59fWy7dztcbuE/JNkSohCOJA4Q7tt2GZ7/QTXnwPUNXsqhVyWJvwkAWW/d8lRYYKF/OFyl934fnG45ftlu6MVguPSv5SchVn4RAh6Vr54cQuCemsK+7revm80iu4DkJwWb1ZouldqfsluBu//EDXjedYm7GpvQZK5XRJD8CB40jHJswEBrtvOJxrcPZ96zaKrx2SKiEIYku1v67nP0bX1zcUDtEnbBXe5EltVaYCayHOuM6z6t+Xa3c/zwPsUmoI7gKl8tOOFQBlc8qutzSbc6qUjO0/x5N+P6m/XWrjj84cd5HwVebPN8Rfo9/gi5R7K+EdHNh/IaEZcm3hhcFfOwvb+x4sVxzOeGzcZKliSQpS/xLPCLESgiA2HLO5XDaIOfriOns/1FaEKNnv1T/PdT4ClfJZSoDbBt2vJPX2A/yuPH0QnthuMfySJFD791JVpOof5q08PYVfVipeFb7BHFoBsHeU6CPVdujewWnI9/x3JRGssRli7Z6p155bUvrtC899B/9VI/+Nx8Zxl+8R+7Tvpc6yEqkSgiCU3HOJtlzt3LHnKU9DcwZvmtb65Ls+2a34wbuEPAVHj+qtvah7yririSEnaThs8D8Gy+8aHj/mOuK9Uft7r7BrhlT7FOGX5oLut93fX/cbsP7YRGqf8rcJN5+j/vRFrIQgCBuKvpLTK+Z2vPVtMfk8TIi4SwiCJJX6i+BNbS3nxGcrAXZE1x0EQRLN2wAtDQUXpQDw9TkEQbxQcADWm4qWwNZIuoIgSOI5FeBPY0RajV3wYkSdQRAk4RxSCupknxJ3w/ZGNjsjCJLNFJ45/I5eRzjvMxKgfJg2Wdbhb8PvhOh6JCKa3VfkuhRBAqXjD1J4yfpLHXe76QDAzkcHnnZ0447n3P5lVenz+A0lNrR8vlyZ7zVtKYIESv6jFWoI6zTHqcIb3PrFGnnfPZ+PsiRPRKLimKnCZTF7B7kUQQLmH6BjVZ00e+e1PPOqi09ra5OYDYmA9m9WideuvYtSBAmaUyth25izmp889GtxAFoSIyIxp93ShwfMtXgHuRRBgibvN3hK+l6Se694R3NRmgpIDDminOQd5FIECZIeurzVIwVHedVhZySuFBO9g1yKIAEyfqE2+UTeYjDmWkWSwtdE7yCXIkiAfKufMucyIWNJumezSAyZS/QOcimCBEfOrfo1Yfov8JLQBImYmUTvIJciSFhUKwfYHnUnEA98SvQOcimChMY+U4JI95y3xsRP6esgzEBHQeKIkKr5b96qzgATX7HtGuIIOgoSR04HKG2YfjcCLarMjnJr+koIM9BRkDjyOMB4bzUniC5SekAmBVVp3mRGmIKOgsSQ/PWwwdsvPflb4PN+R6jJ6Wvtg/nMeoW4AB0FiSGDAC73VrN/5d9zdKt9AYYx6RHiEnQUJH5U/9UyYalb5owxrL4FVeQJSJGAQEdB4se9sP4wbzUP+dCQ3aDWXpjHokOIa9BRkNhxbNmBk9goXQIwlI0S4hJ0FCRu1PqfKTG1d96ESsxuGi7oKEjceBUeZaRUc4/XwFvEK+goSMy4HV7PSb+XKy4GuJGRFOISdBQkXvSv+jSfldYbUIlZrUMGHQWJFaeXfc0siUGNPTCblRbiEnQUJE503r2oPjOxCz2/bYh4Bh0FiRGdSlbqf5tp5u+BymtQgVODhQ06ChIfTty5pqlu9eplvtRq/Amf++sPQo+QTOI4l6UIEign7ljXUlsrGHpwtC+5CwCG+OwRQs0c3js6uSxFEBomTDiPav/uu+G9xyX+76nnp++Cqma+2n8VKg71JYB4YAHvHX9xWYogNABMpNn97P3mVEle3xaUqL4bZvoSQDyQuxUIXw3JpQhCBcCDFHv3LTcbCgz21XwfgOt8CSD0NH5VuHAlZ+W5KEUQOgDGUuy9z2IoB+r6an4qHPSWVxLxygz1IlZsa5emFEFoAfD3ZNUf1XfBjAibRxCEMQB3RNj6eX7vmhAEiRXRZqH/N5QfEmHzCIIwJtIXf/NL4JPoWkcQhDkA10bX+LkA10TXOoIgzAFmqdg88DKUs3vlEEGQ6AG4LLK283fCx5E1jiBIAABcHFnbvQGujqxxBEECAIDuvR6WvAhl9SJrHEGQAADoxUKmoNslQ0f07diApk7eTviIRduIb7xcPgQhAdDTt0bT0XPK5BDu2ae7r9bq7beZuBniD4+XD0FIAHTzqVA4qVT/os98fE8nUeDlQ5gC0NlX/Xrj95reHZxfnVHXkODBy4cwBuAEH7XzRu60vI0MzzDrHBIsePkQ5gC08V653izrgATYwa53SJDg5UPYA3C057rNlpJGJEBrhv1DAgMvHxIAAJ7zxNZdRh6RcBHLDiIBgZcPCQKAw4R/Clp1pg02y51uMyKhYwD9dMHlDz+Mbwm5JnaXD8kMABpyNYd9K4yktdPPpKl5i92IrKoVVGcdObkC4MhIWk4kQV6+N9eo/ItBV5EkAVCn/RJ1NH1wlOPO+tDKmpvshqT35PZ+QjcLVgI6inuCuHwKJ+vUqP5IIRkAQBvhF8RKeQDssrcUU2il7d846OqtJz5DN58BdBQKmF8+HR9rYj8x6CqSKACWwKL+hbmtRx8Qh8DPNcn7WUIrp9mNyGme+uE3dPM8QEehgfHl09NJp3Y5g64iiYK/6u/WEJc6SXPxPErayxpaaUuxlzBu36GbhVsqNqOjUMD08hn5EAa2UMhl0FUkUQAsryEvjhOH1HLrPsTQSht2t6XvA4PQzWkw5kt0FAoYXj4THVI/MOgfklQA+iuLp4pjKmX5I0UOrSSzycNbQgxCN6+Hr6qho9DA7vKZeR8DWrIagFOUxebSqDI/nbcLrSSxqCl9DxiEbh69988WHDoKDcwun5njUotz/KsgiQVA/XXnNGlYtTTuYBtaaaVktIdQBgahm9UWwFUcOgoVrC6fhbfhi1410u+GZCoAdZTFe8RxZbrbsA+tNLN/gpfJvFiEbt4Hb3HoKHQwunwW2lbxWvs+utHzux1IwoEydVG6+3hBKmaBY7tsZAROrlgvfBjQUVzB8MSTeEOp/K/arHuOJALYqSz1FgdCqp1UzALHdpkN7IKVVacL/6KjuILdiSdxTJVae1UX5n1HEgBslBdypVj8T+ViFji2y2xgPwuPiP+io7iC3Ykncc7UWUv2yNUrxlZj3nsk9sBv8sIQcRTslD+TFOPO24hkNrDPh5/yxQV0FFcwO/G25HV/YLkk8ATTniOJAFZI/9YW3xxL9TFtXmkz2Iq9Dzhj83b6bkM3C7cckJPQoaPQwOj62ZB7wxZxOJ0WYBtIPIFV0r9PiR/kB8ybbYLvd7cN1lHch25Og6HyEjoKDcE6CsfVfU24jqvx8WzWId/1XClc/8phls3fED/wmzqzGpFkQ3EfujlEmzkZHYWGoB2Fy50qXMkJwTaCxA/YIPy/w37+6u8hzFc6ifSBF0Irg3QU96GbR+/dWqQso6PQELijcLnv8W18G3AjSOwQI9oarOYv/srjCZt7VFo+71JopfsROWGCw8zKBD+hCN2sthDOV1fQUWgI3lG4I/g/Uwfw555sA8o5rmAeP75erUPcfqPp866EVrofkQATnTba6LtiLDytrfh3lObn3n7HXxv5kkgMITgK9xDfSHvPtXNbnjti5IVt8hl2CAkBgDq1eUPZN8huh1H7dZ/3g1MOV+u5d5QHnTYCWd8Nx1TAd/9V2c3XX8j/e376ikRafyjfc/l/oT8BhOEojUH3ZjslOUO2A+zczH9lvS2PaaeQgAHotwxg8bH2ezQav0P6qB2YMfxIXT33jjLWaSOQ9d3Qk3DPBDCESkPlqoOKwL5rvCkkijAchSsB6OWtZptvYfetRfz9+KDtsAKT8ycJgBTA0zapIBWKugwYeEYbwxulNI4y2mkjkPXdwNJReh+E3Qs/Wy9JnOVJIlGE4ihfAbTzVLFuMWw4Qlo8bAtsKGTYJyRg+JG1q6+3eq73vIOFDIHWT+sRQvRe5f/t7kWqxd6tNwiO1kb8ufzXzL95D8VRFsB2b7csrwP0UJYHAszFjCvJAWBhc2/13DvKrSxk0uLryezrS+WzkCsmcj/Fee8MIAxHyd0Hz3mq2BFgnbqSX+Frbm4kZFITvf0VoXGUG1nIpMWPo5y4VQ2BaSw84b2JUZ/iSxiO0g7KvN303ATwhbb2q+dnY0gE9PZYj8ZRrmUhkxY/jnLcX7TlD8DRAzOEMBzlY7jdW8WXAHZqWfR5R3mEUY+Q+ELjKFeykEkLqwi3B3idv6TfLeEE5Cg122mPoK6FWR6ff7wPuhR+DVOOf5OQDIHGUS5jIZMWVo4yEmBF5j8JDMZReuyCNedKizm3HNjW2KPMRL53s5UvKecDlDVh0Tkk1tA4ysUsZNLCylGmZMVMeME4ygvCY+3ZPWtwh/aeBXM8Z9Y/S5AZL688DzCZUfeQ6CBGetCiSJHe66GWSQsjR8lZDVP9q8QX9ideRz+pojC/Y9kdPr7o/cKLVEmPx/mvKF9jToTkQzHu0o1Ictwk+4HNyFEugi8L/KvEF/YnXs/wEqnq5sm+fvDtLgYw/zOP4zruhO/q+ZFC4gHFuEs3IgF6+msg1ANvtv2LjDaUoE98Qb/bHx5z9al+Xzn+m9iBLxqcVALP4zeUTIDKOZxHJEA3fw2EedzdN8A0iskME0hMT7yZe8UeFO/ajlOeZgnuBxyAQ0Y2j+O2cILHSAdnWr9QwXeoYnIWJPWI2DDSc72UmScb3tpEBGgc5QQWMgbaKAm3WTJssTLZzJuZbymxdxTuggPCpah0eIUDySRoHMXhIV2cHKXF2fd+vE2ylMyfFiL+jnJXVZl4LZ7L/Nc2EY7OUY5mISOwqFTO4xKIowjkSwmmyj2HUiSFuDtKzdfhvSZS3vQZ1aPuDBICNI7iMKs23cBeoXzdCcxROK75f7PiS0rMHaXudzAjj6v+b9FS3s38m1CEylEOE/4paNWZEFcQP0fhCoU7nx8DkzfQ7L6i9DsFQrwdJW8W7BYzLj0oWsqj3pW6DL535IAsyR2cbGgcpSFXc9i3wshYO/1MzzICoTgKdwXfqV3ByWu0fL7cR2Znf8TbUZ5R03QNF8bNQYf7ZidyhhWLjlTxvqccQEiY0DhKnfZL1BiHD45ykCnodsnQEX07NrCTCsdR8rbzvaJOUUnNMVOFn6rRUQi0rYJK5cvbXcKoecuTTNEcKP17p/o93gfY149d75BAoPqtZ6fwM6BsKbuOMm5UZZqOnlMm7zP7dLJUOI7CvQLSvGhB0v5N6adqdBQCrwF8qa5M4bu618s7QnV/gi1dxaXb+OE3gFHfkICgcZQlsKh/YW7r0WKAAfxc07BRlimcVKoP15xPnEk9JEe5H+CzAOUF2i19eMBcdBQb1gK8oq7kr+D72tKDyjTtJfLXAfZjZsl4Q+Mo8K50D9Gp3PKcTZapN948Zft80k+GRkfJ95p/Lh13AzwekLSeI8rRUYjUShkGyXWgy2PtntMAlis5Vhryf65+wnl/Yg2NoyxXHkqME81iuVkmb+ROsPAMQUrnKMV9ppYE9Zng/6KdHZC0gWJ0FDK7AF7X1lqD8HCfmvkAd6kr/I0sXM2gZ0hg0DiKOq/cqaJXpBrqNwJXb5bVT0Ccj9mM4ihFY6R9fPTfgZxVMD0YZRNfo6OQ4e8Hf9DWGgKsptfoxR+h9jhWyOG0mEHPkMCgcRR1rormkhGcqd8IzZaSDAWA8Aqw6ChFN81VnvL6PAYbhkHpUen3YsBcdBQydwLs12JIegK8QK/xNOhfUS0EcHxjFYkcGkdRP5+nSUbQUr8RlpENBQivsa+AnpqdsPxMtHj4CfU+p91eGMVM2JGZ6Chk8peAbqafZ2C9bTyBPV+AIVhbmAl3JIOuIUFB4yh1lMV7LPczNm4iYJ3ttsMm0y4+j0HjB17seyl55fX7Uncz03XmU3QUG7ocgKoL5OULoNLL1ATChLMna6vCHebHLLqGeMPhk+4eWapMVZXub16gbECq2/mRYpst/sn5Q5Rb9dpDb6+BNV4mbfVEJI5CfeIj4dgfITXpUH6hweTKdRek3d1KQQr0z1G4F8H4kwASMhTjLt2IhJ2KaG+xNNWOsgHbHu237X664Fszp26QJSsX3hrem67Z4yi014O/8XnoT4C189alyid4ytIpzG0KI7T1+/jVLV6EEDZQjLt0IxI2ypq5Uiz+p7QNkHu0961LbYaai+BbC7ln3HzfY2NuvMDDDbt3ssRRvFwPgeZ9/n5vv/ZeDX4lGGblmMCvltnvjQQNxbhLNyLhN1lziFi480jaBgg92gqra1o7LeIq+DYeZIWjRHU9PuIbW6sFtQmx/OtDahrxgvsBpwTM1xafq6b6mGWIFFsGnrZtzcTObeEXcmMug2/jQQyezAZ9vqK7Hg8LjWlBbdOEpsNpGfEEhaOskv59ShxQD1hkSOxuS2pQthNOiJklOorr4Nt4ELmjBH2+orweTfbxbS1T3zD8CfTvCiHxg8JRpLueK4XRVDnMKkNgEyEWiS9OVSpBKmRHcR98Gw+idpSgz1e012OU0Nj90nLudcJbquNCahnxAoWjiJkBOgj5W/dY5islGsoiUpbXynnDGv+ivddDcBSK4Nt4ELGjBH2+Ir4e1ZcLjT3XmOMaXLRYbBhn6ogzFI4i/FFqsJqvsPJ4koyZktG1SDJCBh5HR6lLEXwbCBMmkCZ4diBiRwn4fEV+PQ75j9hc8W9Q9ZrwYLb00JAaRrxA4SjlHFcwj9//1TqEjWb2TzjEXsopP0rudJsBTAi+DQaAiXQVInaUYM9X9NeD424WgyJ3vtGGE7Lqs3iMQkwMXLPnsHsux1y2PqFwFKhTmzeUfYNsZPbrBtvBKYc7STk5yi12A7iK+JUnAAAepKsQT0dhdL6ivx4CDXpdKEQrNBMiaE9Ju3c6iImB824QI67LXnT4U4ikh8ZR+vHffxcfayfTaPwOaagdmDH8SGcpB0epaX7nR2Wmy376BmAsXYV4Ogqb8xWD66HjTr7d1DQ/WgAAIABJREFURX5FyImBa86EynHt2ty3GtZ28NtCVkPjKPwfiKdtAtIkmaIuAwae0SZ9smgHR7H9kwhdXfbTNwCj6SrE01HYnK8YXA+NWuvA93NZm8TAtT4HuFBYaLIZtrTy10R2Q+MosMv25Tv3MgIOjjLNbgBPo9D3hzojhFti6SiMzlcMrofG/Xy77/uTsEsMPB3gXWmpD8BKu0BuJD00jrLQfrYUVo5i+wGxBt8GBgDlrN9xdBRW5ysG10Ol2X6ANfX96xASA/M2Uian+8lZBfCQ/0ayFvdWkJrokDLYl6PoHs3YDWBC8G1gANxIVyGGjsLsfMXgeqj8B+BgFxZClsTAeSsAPlFW7uKbaceimezEvRU4Zqz37ijHjVumq2ozgEnBt4EBcC1dhRl8D48Lpi9pCfp8xeB6KIzlGx7ORMmSGHgoX6Dm5+oM+sxzCCV0VsBIRnGU/MHSADXoECAG3wYGwJV0FebwXewUTF/SEvT5isH1kLkCoHwwGylLYuAfQfejdHX+puhPT8lcEC5KR8k/9+UScOMoNsG3gQFwGV2FBXwnvSQ8ZEHQ5ysG10PiwjLY2p2Rljkx8GEpgLJ8dVXILXoVo6ayj4gc5QTNTtI4imPwbSAAXEy1f+5WvptDAupMOoI+XzG4HgLVJwMsThPl5B7zg69rwDCf7bPgKWt/dkD6m08NowbUOo3WGQJsxS2s+sPknFG919P4VaFPJWeFPNVd0OcrPteD42pduRg2383uRsTsKG+BYRag+4FBHF2mQjEuvI0YapnDbppdQdjCqj9kqPKjAvRyrzxjn9Krim2h/kAQ6PkKQd8tTfvfPXU3rL4pfdyke8yO8ju/PkdbvV24mskLSQnn0Q/FuPA2YqhlqshbWPWHAG1+VICelC1EQXDnKxx9t1zw9pO39G6Zm35HCsyOInxjfldbFSZohmOYthgCx/4eyq8DFOPC24ihljGXphbe2YKyo1RngD4/KkA3qhaiIajzFZZ+lJgcpZZwEM9q6/2E9ZOt1WLNidtiMsc8owHhXsYwFg/ChqbmreK/tHlNCyfcTix3oXOHOeY+UdNgBv2BTqJhpMXkKEcK4+If2vrZwjrFnW8c6LQLYjLZYoSOsu+dSzuZMy5JOvR5TQlpEdzqWHoOcILLY4kB6CgeMDnKScKw0M0JJDpKP2u1GNNwrdDnA0dH3Q8uOkfh7aSAkMNN1PGQ15ToKO50CI7SxuWxxAB0FA99NDnKqcKw0KX9OV9YP5dN38IhZ4Y0tmdH3REuMkcZKj2YJjoKRV7TRaXyO0EkR3GpQ3CUOFi9S9BR/DtKC2FUXK+tXyysM3mBKCzuU8Y25fsjQRC+o6x5rOuvTu8e0+Q1dUoG51aH4CjNXB5LDEBH8e8o1YXMcLpnEJcLo+QoNn0LhbZqPMbOw6LuS/iOchLnlLma16HJa+rgKK7zoxIcRbwsBa0613N5TBGCjuLfUTgh6HmCtiq8NwgJuPYqM7XBHX2sb+iOIuAhPwo5r6mXZHBmHYKjNORqDvtW2Hft9DMpDisK0FEYOIowrZju1+N7+NVyJj0Lh/N1o7u8SdS9SY6jkPKa2gu5z49KcJQ67Zeou39A//WXKkLXJ+E6CpsjY31+fDuKMLfyO9rqE/zqAiY9C4W8lfrh/XjU3UmOo5DymtoLuc+PSvqtR/jRuVLefxedpdBG6PokREdhc2QBnB/fjiJkXvlCWxUyYd7PpGehcJlheO8J5Q+ZA4lxFGJeU3sh9/lRCY6yBBb1L8xtPfqAWONnilc86CN0fRKao7A5skDOj29HaZ4C2K5OrcwJMxf6n8IjNL6WreSdG866mz+QMRF3JymOQs5rahTK751eyKpDcBR4V3ovrVO5WOdRt8dFG+nLgJAchc2RBXR+fDsK9znowhqr89+hdrJ9kShITpLO5G9iHMX9ANuiyF6jIyGOYpPXVCdU3GdqSfr0kgQdgqMsV150HSdWWu7uqOgjfRkQiqOwObLAzo9/RxF+L75NWTmZX3mKQbdC4hXxPH4rzYUohLoNi7Y/0TpKq/VzLTok7PKaKkJFY6T90gmRdPS1CocdKxT0V9bFaEpIufpu7iHSlwFhOAqbIwvu/FCfA0ti4BolutthfiztIcxhGlPyxXQau5SfeI6thN8i7U/EjkLSIWCb11QUKrpprvIUNY0QUUetVeeqzyqgh1Cg3kQ3l+q5+QmZItKXJSE4CpsjC/D8UJ8Da2Lge/gPpfLFtBjgPv+dCose4lnUkli+EF0WdYkEOIpDXtMV0FOzk3SOYqMj1cq/4G0xr5zoKOqvO6dJNVumPySaSF+WhOAoTI4syPNDfQ6siYGrfQtws7R4IcCq2v47FRYPCCfxI229a9SvIEfiKING2N1HWEecU17TDuagEwchWx2+Vs5pzym3+KKj1FG23SOWufhm7jpClzUhOAqLIwv0/NCeA1Ji4GN2wLYWwkLLnfBbFKn+vfKNcBJ1MzXnbIF5QbbnMCDcw6gBZh2VanR+pJi0hVoHYOJ6rUxwlDK1V9I3dYfIZurWmBF0y0z0KUR8nB/KyuTEwG3/gNXn5NcZtB1WJei1Lq6u8ErPZ/qSt+BgkG8Q0FxST9ea1ZCh7w9hw34vHTKWCY6yU+lUb7EoZZM/Vgj9pG6NGUG3zESfQiQsR7FNDNzkpQo4WAk7RrDMaBs4fYQjOV1f8hiA7fTkDKC5pJ6uNashQ98fc+net4SMKywcZaPcp1wpFv9TUn91oZ9UrTEj6JaZ6Idzflid3OYDx9351zrp94sTk/mDX2IouTPY1wVpLqmna81qyND3x1C0FVbX9NghbX3vK8Wioyg/vw0RS3cSpokxhX5StMaMoFtmoh/O+WF/cpOD8MB7rKHkdoB1EXVGhNHVYHVRKXS0sbhmYue25PSSbqI05fKqL66uzX0pOoocdVdbfO6b6mNp2SpqBznSlyVBf5qYHFnA5yeLHeVw4SwagvW4CfyYjTKFdeIdhbcTzi69pMs8szzLR4khQpKjrJI2PCVuecDcLlGUjE2kL0sichS6Iwv4/GSxowzgj/1XY9GLfFGUKQ0S7SipSiWcgegobvPMbnvyJHn5S91dz5XCzpWWkGayKBG7SF+WROMolEcW8PnJYkcR0kE+bCxaCNFO5pBcR6mcN6yxYzI413lmte+IkqOIU+B2EALe9ljmK7UTJWAb6cuSSByF9sgCPj9Z7CgvgXlO3TrCz8kXRtQdgeQ6ivDqhaOjeMgzKzmK8C2mwWp+z5XHmxu1Df204BDpy5IIHIX+yAI+P1nsKHP5Yz/UUHKOcHJvjKg7Asl1FAFPqZsc8sxKjlLOcQXz+B1ftfySaB/6acIp0pcpoTuKlyML+PxksaP8DspTP4XnhdM7LpLOSGSfozjlmf1SjsKvzRvKvkHW9uwzw8F+3fLBKYfTHIUfQnAU/0fGVxwV4PnJXkfJreT/7hlK6okBfFMi6o9A9jmKU55Z2VH68fc2i4+1NmefvBag0fgd0sKBGcMJESxBEYKj+D8yoZMBnp/sdZR6/KEPN5QME8+x6xxhAZB9juKUZ1Z2lBTA06RUkA5fUQSRoi4DBp7RJtwg7hAchfN9ZHIngzo/2esoR/CHfr6+IF961y3KzJBZ5yiOeWZlR4Fd5DcjbJPXRjemw3GUOIhEJh9jjuYP3RDTM1wajFGmccs2R3HOMys7ysLm5OZW2omiowQvEpl8jDmB/z6tfyx4iHxneZVtjeDJKEfRPfqw+eynyTMrOkpqol0Qs03w/e626CjBi0QmH2O6AWzSrz8pj8huUXWIyyRHOW7cMqeMSyJp8szm/Sg4Sm/rPjLf2ImiowQvEpl8jDkJ4Fvd6pkpaUSmonyBOjMcJX+wdCoNQlac88x2eWqbmM3Ankl2ougowYtEJh9jWhlmLquvZA4rjq5HGeEo+ee+XAIuHMUxz+zRY1eJOzk6So9KG1F0lOBFIpOPMYWGXxreUAbl+9H1KPmOcoJmJ86O4pRnttHNC5TdHB2Fu9FGFB0leJHI5COA8PcQQZBsBQ0FQRCG+HCT49FREAQx4t1Q7v1CcRRXu6+Ef0kLjVdrrVuShIWKr8NnLkOjY76KqYV3tvAipCmsm/hLmucoDhqe6qkd8FPZe8th6QfcyaDPgbsugHWRmvyXYTZH4yhfwuviv4W/6D4JNnM3hESGOMpB2NDUvJVOZ8s/u+dIEW4eQEexUDjhdv8i7sgYR6k/Gypv5mgcZQp8IPxzyCLdZ8H8KmzIZIKj7Hvn0k42matd6ux6qVc1YRkdhZm+/r0IdBRXNF8GO85SJNxpDBG/09RbqP/r2stb66xIvKPwdlJgl7nanc7+ty5S8uOjozDTR0ehpfF6WNlClXCncTKs5b8O/qQ3lP95apwdSXeUoQXiig9HGaibNhsdxa/+olL55Sp0FEpq/wx722oS7jRqVaZqNV2hNxS43EvjDEmwo6x5rOuvTu8ee2geHcWvPvFtcHSU9OR+rJmBe0fhfoF+aw2GMt9D20xJrqMIM2I4Zq720Dw6il99dBSPl/MpgCf1ai413gLjmyEVx3lomynJdRQBx/woHppHR/Grj47i7XIOB1iRr1dzp5HzPhiZRN80Y9BR9KCj+NVPvKN4E/PrKOdUAVxgUHOlUeNtk6H8Xo+6adago+hBR/Grj47i5XLW+wNgnlHNjcYh/zUZSvnJtC2zBx1FDzqKX310FC+X8zmA1EnaqktHaWaZju4W2oYDAB1FDzqKX33jFcnv7UmEksQ7So8UyNH0mkR6jeP/MBvKO5TtBgI6ih50FL/6uitS3GdqCXgSoSTpjlLjV77KCSa1tBpn7jYbyv/q0rUbDBniKK3Wz2XRIXQUv/rKFSkaA9rnAh3FkYf4Gl+Z1dJpXFBuNpTfQpvI0pEMcRS/QjLoKH71xStSdNNcJUrCkwglCXeUEyrAFOnqwlGshrLpKKpWAwMdRQ86il/9FdBTsxN0FDd8wlfYnK8vSe8ofSyGUnI8VaPBkWxHGTTCMqGXNyGZruc08FALHUWlg3lmaC8itCTbUU4QKjxoUUMQBJGhcZS3hArGO5aou48gSKygMJRWwi2iKQNB1N1HECRWUDjK88L+4wiOYluj0z5zc98dStFg0NAdftAy7G6JmQkF3xrlEGTYMmN9wyjfCqtrWkUKJ5Xqd5pv9xjMCYsG03PgTUx3DekuZ2PxEWsHq5qtRjPzoyqA/h56HBjoKJG3loGOsmZi57a6/BKKSL3x5rno51e3E7ODoJFkR/k/YffVBDU7jXpLTIe/8TN41EOPAwMdJfLWMs1ReDvhjBlrJJG8kTstf13hGbruEDUS7Cg1xMDXxwlqNhp5s0xH/tXhA/QvGUYPOkrkrWWSo6Qq4SJpxeIo9cyfBZEdVL0hayTYUfqKvT+HoGaj8bzpwJ/O51rCnlwPXQ4KdJTIW8sYR6mcN6wxMaueINJsKdkLWlN0xk4juY7ynrB3lTmpif0hDTUedtm1QuF2aOuhy0GBjhJ5axnjKEWcTZ5OXqSu5c17mYvc98VWI7GOUk98xryYpEbUaG94Jg2bpXQoM2CQhy4HBTpK5K1ljKMI2OVHmW7nBR1dS+faaiTWUQaJnZ9CUiNp1DQ+lS2W4+LGWRUiBB0l8taywlHsqKrlWvoWBxmqPjoSqqPMFDs/gKRG0vin4Zh/KpKLz4PvPHQ5KNBRIm8tqx3F/ZSaNa1xGEl3lCLplcomJDWCRh/DIX+hZkMphDLqH+GDAx0l8tay2lG6ulZ2+oqSUEe5Wez7dqKaVaPRdv0Rv6szkd+hM32XgwIdJfLWstlRprlXnmarkVhHkQ7pa6KaVeMZw0Hn6ba8A0OpexwY6CiRt5bFjlJMEYW/0lYjqY6SI0XrvUxUs2gcp5/q6/Ma+k13wr/puxwU6CiRt5bJjnKsIkJkN00chTn4XtNIqqMcLx3BaKKaReML3UF/XWDYdBoso+5xYKCjRN5axjrKceOWgSJCYhPV3f83thpJdRT5yVBfoppZ40LdQf9U37itdmVVHeouBwU6SuStZaSj5A8G7XNBNpRFTamUJ9lqJNVR3pOOwTpTMcFR8lZpB73VcuKWQE/aHgcGOkrkrWWeo+Sf+3IJpHGUktHuI1FEelTaaSTVUbZKR1HfsoHgKJdqR11hdY8X4S7KDgcHOkrkrWWYo5yg2Ym9o+yfcAh1V26000ioo7SRj6MaUQ1BEETGlaMMkfbdT/YnBEEQGVeO8ri07xZ0FARBHHHlKHLIXrGNo+gL6uxRpU0ZILv/QGj+q+6uOoDQ4PayxqA110MwCmj6Zh7YqYV3tqAW8QBTeW9iumvo+nIul87Sz2Q1g4b20/Gnxj1vryA6WmpsjoeDQJxAR2GDZ0c5CBua6jYE0rkg5ENzlNwy6UQR3hu2OMpk5azub6EvrvM20U8EppmzOCE+QUdhgzdH2ffOpZ0ImasDIpmO0lw+V5Z8SwRHUfOi/J++9NjltoYC8KMxrBbxCzoKGzw4Cm8nBaTM1YGRTEc5Sz5dv5HV9BqFKXnfiua60i7awxUSH8Qp+WwGgI7CBnpHGSr9cURHSYOSMraErKbX6K+4xNu6wsP+cDQUgIkejgOxBR2FDVSOsuaxrr/avHvMul+GdhPpKI/KH/yUTYSbbv3vikl00cpyvzTYxx5YevvgkU/9pCtKnezhQBA70FHYQNO3kzj7zNWMu2UgmY7ynPLJb0xU02s8Ie/5q65ssGYdO979W8szYZFYfNzrWvmXHg4EsQMdhQ20fbPLj8KyT2aS6SjqR9/6BrbZUd6U9/ynVlRLvefZcpXwwKR+qkJ+FHvzQdVSLvFwJIgN6ChsQEdxW4vWUdScdNb5RcyOMlve80KtSMmRWfW0/HLTCviLvKn7ZkX5G/oDQexAR4kGdBS3l1OxCRhOVNNrLJZ2rKirFX0lFe07VSl4Fe5QFhtvkJVTR1AeBmIPOko0oKO4vZzfKo4yiaim15gj7aidUK6x/HuyFpN/i+6HoCsU6Riln0086CjRgI7i9nKqEyR+QFTTa7wk7fhfrUT+PVn3A3EX+F1dzlkoS39GcQiIM+go0YCO4vZyrlMcxRo0a3aUsdKO72glt4sF3+l+eK5xEIrUla7yVxhC9BziEXSUaFAdpdX6uWohOgqBbYqj/ElU02tcI+34lFbymFgwWF/pB+ijrcgv/BByryAeQUeJBtVR9KCjENioOAocSlLTa/SU9ntSK5GS7hry4D0D47UVJcrWmnES8Qg6SjSgo7i9nFoqaktAitlRGkivKeseuIhRtLsMlQbrZ3w9VL7tOcr1ESBpQEeJhkEjCJN6oaMQWKA6Sn/zJkAQBNFw4yjarKuj0FEQBHHAjaM8re79HDoKgiAOuHGUUeres4iOYiiR3j6+RSu4RFi/2rDPo/ofg6SnNM+66QiSabgdgskl4ANkKu9NTHcN3V7OgaqjrCSpGTUO2y0U6RNICo9hFhn2uRS+VZdzy0WNi112H8ko0FHiJB+ao3RRHaXUnGaa8D3nOrHsWK2g6RZ+/Sz9Ls2hrLqyfKS4e0lt90eAZA7oKHGSD81RGmo3SYcT1MwaM4SyybqCzusAfjOEsmwFNcfSxaLEQ267j2QU6Chxkg/NUThtLtdTCGpmjSbCfU9FB11J/TcB5lfXFXwCw5TFWeJ3n8Pcdh/JKNBR4iQfnqOoLx/DAIKaRWOw+CTFkI76qj/hPV3K+7HwqrzURgxwu9dt75HMAh0lTvLhOcrLqqOYA1KIjsJNEUqHGYoOHfSf79qqa+eqaSPFXRfluew8kmGgo8RJPjxHGak6ivlHXrKj5DwL+hRLMjVOq6UsNoKU9KbPKUJiyL0dOCQ7QUeJk3x4jnK+6ijmNCZkR+Fy/sUX73IwitXQS/jn0PWC9fRw1QkkA0FH8UBBt0uGjujbsQETef9iXhzlKNVRVpi22DgKl/MCX771GFvFt2GMsJfws9CBM1z1AclE0FFoaTp6jjxpMMw+3a88EzEvjpJ7QHGUA6aAFDtH4XLGVgD80d1O8Q6Yzss+w1cuPctuHyTzQUeho3BSKeiY39CPPCMxL47CLVKbNQWk2DoKx528EqDyPpsJSHvAZq5AeAOxrLe7HiAZCToKDfXG7wUj873LMxPz5Chvqq2aAlIcHIUrEL6CzGtG3Fa7Ejp/x29e2s1dB5DMBB3FPXkjdwKJqMU8Ocq9aouXW9XsNc5dwX8JefpI0qYlsJ+/hxqd7659JENBR3FNvVlEC/Amz1LMk6P0U1scbVVz0Mi5hP8icvCltuby6n1/4+t9hnnbsh10FLc0W2rjAV7kmYp5cpS2aov/sqo5a5wxk9/jtyl9dK8CdntW+Mb1pzn+Fsk+0FFcUncZ2BGxmDdHya9QWjRlSHHTi7Z3fV4KUP7rl+9NGTfp7S+L9wt28hHstnloi2QR6CjuyJ1uZwEdWYqF5yjcL0qLpgwp9l1DECQLceko/1H2N2VIibLrCILEDpeO8qBawTjleYQ9RxAkfrh0FHXGczC+/0ejYWQA/OipHpJJeB4+iYHJAU4jfnZ5pjEV89ZX3TWkuJwnqs1eYVHzdsaOhoM1PVVEMgh0FFestPGAYsKUYz7EwnSUWlVKu/dY1DyesRIwpztAsg50FFeY4+VldlsCvfyJheko3Gql4ectah7P2OcwwltFJHNAR3HFN0QP2GSZNNinWKiO8onS8ucWNY9n7CF4w1tFJEoKJ9zOUA0dxRWTSB6wqClrsVAd5TGlaWNAig9HuUTNDIkkiDaWHDl+QEdxRY9KiwWUjK6Vvh6lWKiOcq3SeKlFLY1Gg/53PjziHGsm2aaQque2dSQ2oKPQweYAbzRZwP4JhwQgFqqjnKK2b3i8nNZRDv+PFMC/5W+WTZuhp9vWkahZVCrP6YaOQgejAxy1X2cBB6eY581iIxaqo9RXe3CcWc1J49Idar2Xapi2fQy3uW0diZoV0EZaQEehg9UBNhovf5QOzBhOzA/CQCxUR+E2Ks7wV7Oag8bj+i9X35u+qI2Fl1y3jkQMOopHGB5gUZcBA89oY/7DzFAsXEf5QjGGy8xq9hrdU4b7tX8at54HP7huHYkYdBSPJOkAw3WUpxRfuMmsZquRt8RgKFB5omFzE9hvnpgdiSvoKB5J0gGG6yhDFV+406xmq3ELmPjasLlaFfi+IURCAh3FI0k6wHAdpadiC4YwfEdH+cTsKKZM+luhPUXHkShBR/FIkg4wXEcpUlxhpFnNVmOdxVHON2w/AA0oOo5EidFR8lnNiYKOEifCdRROycZ/i1nNTqO+xVBgrH57Eeyn6TgSJTpHKe4ztYTVpwQdJU6E7Cjfyq5wnVnNTqOb1VGm6refgmH4yUFxlKIx4Pi9lBJ0lDgRsqO8LruCYcYep9F1stVRRum3/x88S9NxJEpERym6aa7yTggjWXSUELF+Hm2hlbUuumCc3NiFlk7aVGhi7eiZus3VtwFOKJgYVkBPzU7QUdwTowOMm6MMlhszzHzu1HzeQXM/U/qo2eugmKbfSJR02ORjyDmQ+Y4SI+LmKGfKjRkyrzk2P9Pczw91G48ogRtp+o1ERudHin0NOQfQUUIkbo7SWm7M/ZuCQ0zdXKP/sXg6zMeI2WRAGHG2v9IVdLtk6Ii+Hd2GBaCjxAlvF8Ozo9SVB1N9s5qtRoNdhlFYdpJu21NQegxNt5HoMNvJ3rcuLSDu2HT0nDJ5n9mnu5Zm2FPEFyE7CicNll0WNXuN4fpxuPYc3ZbHoBKnPU4KBjvZCqtt5jAonFSq33G+mzzt6ChxImxH2SIOlEUWNXuNvJ/V8VX+D10Su0M/hMorbGshMUNziTUTO7eFX4g71RtvzrE+v7o7aca9RTwTtqP8Lo4T45xDzo7CNZbq7J9zf2tdaZ+NsO9y2zpI3NDshBNiZkmOkjdyJ1h4xp006+4iXgnbUaScS5Mtak4ardcCpP5dqCvJ6fsjwFdHU7SLRAx/iVOVcJG0QnSUerOsfgKww5U0OkpsCNtRpOcoxrkV0jkKd8g7/A5l717cWrz5btT3hQ0Am2/LpeoyEi2V84Y1/kV7r8fqKM2WkgwFoLVlTzPoKHEiZEepI42SCyxqaTQuWCjulNryv/XlwsKia1zcXyMxooj/z8lR6i4jG4rytcYBdJQ4EbKjNJdGiTHFiQtH4bi/PPaznB5y67s3t6PpLBIXHPKj5E63MRTomFYWHSVOhOwoncRB8rtVzY1G7aNPOavTkeQoBiQBODiKJVWfQlX6OarQUeJEyI7SSxwlb1rVcEhkAfaOUtP8yo/KzPSyOHziRMiOMlAcJbda1XBIZAH2jmL7FQW6ppfF4RMnQnYUaeScbFXDIZEF2DvKNDtDmWZVsYDDJ06E7Cj3C7sfyLeq4ZDIAuwdxc5QijEKP2mE7CjihD2fEdRwSGQBJkc5VttiYyi727qRxeETJ0J2lC+F3a8zFaKjZAl6Rzlu3DLdNScbyqbOrmRx+MSJcB2lQAhPO2jOe4GOkiUojpIvp/LTthANZVFTd7I4fELE7v6UAK2sdTE9vYW9ZxA7SdM8kkxER8k/9+USy5AjjMeS0ekjUbTKgfQXsRIzR5ko7D2Y2Ema5pFksgJO0OxEuuYsBigOnxCJmaP8yO9cfoi5FB0lO2i0Dvabhxw6SsKIl6M0qOJ3fofcSZrmkeRx2E2zKwhDDh0l0/B2MTw6yiXCzp2IajgkMpwqskego2QaoTrKP/l9Pyer4ZDIcMz+kFp4ZwvDVn/SvvuHMCJMR8kRZmw5g6yGQyLDMdjJQdjQ1LzVn7TP3iHMCNNR+vO7fmejhkMiw9HsZN87l3YyZ1xCR8kYQnSU3OX8rhfbqOGQyHA0Oykg5HBDR8kYQnSUK/k959ip4ZDIcCRDGSrly0JHyVzCc5RqqwBKiWmI0VGyAFjzWNdfnd499iGNwydi9NPKhucowrtkC87ZAAAgAElEQVQcY2zVcEhkOMLssvaZq9FRkotpWtnQHCV/NcCyfOImdJQswTE/indZHD4RYplWNjRH+RtA6lR7NRwSWQA6SqZBmFY2LEfpsAfgPgc1HBJZADpKZkGcVjYkR2nyB+mFHp0EDoksAB0loyBPKxuOo9T9H8BPthPtoKNkCegomYTdtLJhOEreTIDN9gm50FGyBHSUDMJ2WtkwHOUFgL2nOKvhkMgCVEdptX6ucQs6StLwM60sATpHuQegxMFQ0FGyBdVRLKCjJAXbLyb+vqpQOcq1AFtOSNtJmuaRZIKOknxi4CinVsLaVuk7SdM8kkwGjbBM6MVigOLwCZEYOMpLsDPNLAnoKNkLOkrCiIGj3AYwKSd9J2maRzIGdJRkstLmIrmaVpYAjaPUnA8wNS+dGg6J7AQdJZmYg+9l3E0rS4DGUbj6PwNMq5lGDYdEVuNrAODwCZ9viIbiclpZAlSOwh26FGBeHWc1HBJZDTpKwphEMhS308oSoHMUrmgFwMe5jmo4JLIadJSE0aPS4ifup5UlQOkoXOONAI85quGQyGrQUZLGjSY/2T/BMlcoDbSOwp1eBXCtkxoOiawGHSVxjNLPOHtwyuH+1KgdhXsAoLyHgxoOiawGHSV5NBq/Q7KTAzOGH+lXjN5Rqn0FsO0wezUcElkNOkoiKeoyYOAZbWowUKJ3FO4E/r7nbXs1HBJZDTpKluPBUbiX+R3Pt1XDIZHVoKNkOV4cpcl+gHXEqBR0lKwHHSXL8eIo3CP8npPt1HBIZDXoKFmOJ0dpXgVQ1cFGDYdEVoOOkuV4chTuEyAnxEdHyXrQUbIcb47Sh9+1ijDzMTpK1oOOkuV4c5TcDfy+L5DVcEhkNegoWY43R+Ge5fctb0JUwyGR1aCjZDkeHeUCYedJRDUcEtkJuMdRI8QuIwHg0VFql/E776pOUsMhkZ2goyACHh2F+1zYuw9JDYdE4Pg5xwXdLhk6om/HBux6I4OOggh4dZS/C3u/RlLDIRE4ns9x09FzyuRP9ezTWfaIQ0dBJLw6yrnC3n+a31VERwkFj+e4cFKp/nM932Oyc2fUAeClNRw+yceroxwhDpOLCGo4JALH0zmuN96c9Xy+5TkYA+QB4K01HD7Jx6ujcFuF3d8kqOGQCBwP5zhv5E7r3cczgfQNvLeGwyf5eHaUmcLuJaYJwdBRQoH+HNebZf2EA+wIpG/gvTUcPsnHs6NMFkeJaZogdJRQoD7HzZaSPuIAhBcp/PcNvLeGwyf5eHaUkeIguc6qhkMicGjPcd1l5I+45TkYk76B99Zw+CQfz45ypThITO/2oKOEAuU5zp1u8xGHjkH0zZb0reHwST6eHeV0cZAss6rhkAgcynN8i91HvMrHRE/2ffPRGg6f5OPZUY4RR0mqvkUNh0Tg0J3jmpvsPuMzA+mbj9Zw+CQfz45SVxomvSxqOCQCh+4c235Fga6B9M1Hazh8ko9nR6kmDZObLWo4JAKH7hxPs/uITwumbz5aw+GTfDw7CndQHCePWtRwSAQO3Tm2+4gXBxWF7701HD7Jx7uj7BEHyrsWNRwSgcPEUXa3TV/VU998tIbDJ/l4d5Rt4kj53qKGQyJwWDjKps5B9c1Hazh8ko93R1knDpWtFjUcEoHDwFEWNQ2sbz5aw+GTfLw7ymppsBSY1XBIBI5vRykZHUAkCoPWcPgkH++OIkc5tDGr4ZAIHJfnmPh1gQyTTvlvDYdP8vHuKHL+i25mNRwSgYOOgsQWz45SSx4dZ5rVcEgEDjoKEls8O0oLeXQYslejo4QCOgoSWzw7Sk95dFxmVsMhETjUT2aD6gjr1nD4JB/PjnKN7CiDzWo4JAIHHQWJLZ4dZZzsKIYXe9BRQgEdBYktnh3lTdlR7jKr4ZAIHHQUJLZ4dpQfZUe5x6yGQyJw0FGQ2OLVUXL24HeUyEBHQWKLV0dprvwSiM9RwgcdBYktXh3lfMVRBprVcEgEDjoKElu8OspoxVHONqvhkAgcdBSEDNPz503Mq6O8rjhKB7MaDonAQUdByCTYURYrjtLIrIZDInDQURAyyXWUvDLZUMoNMx+jo4QCOgpCJrmO0lb5ilJsUcMhETjoKAiZ5DpKf8VRvrCo4ZAIHHQUhExyHWW84ijGiY/RUUIBHQUhk1xH+UBxFEMQPjpKOKCjIGSS6yirFEcxBLiho4QDOgpCJrGOUqtKcRTjZLaAIAii4dJRTlIrFKGjIAhih0tHGaTsv89YHmHPEQSJHy4d5XFl/6UERyHWOOyhEnNby/5xosvmMgT35zetUCTNBt8axRBESDA9f97EdNeQ4nLOVFxhulWNpNHgOSHGdsvUWy/964A7Jv2imsobR3jocmJBR3FRGR3FD4l1lI2KJUy2qhE0ev/BF/94hhqw3+HxUrn+nyPyPHQ6oaCjuKiMjuKHpDpKQ/VLxgirmkUjZzJfuHGQ4QWg1nMVhUXZ8zUFHcVFZXQUPyTVUXqojnKJVc2skfMSX/ZIbbPGGEViZRP6XicTdBQXldFR/JBUR7lZdZSOVjWThmgoEwgioxSN4qb64mqjl+/7YYC7fiQMdBQXldFR/JBUR3lGdZSGVjWTxq18yes5HIGJishv9XWl74hFI911JFmgo7iojI7ih6Q6ypeKF+whqBk1Wu4DmFedqFJjuSLzjFbYSyopz8SnK+goLiqjo/ghqY6ihpYsIagZNeYA7DvURqaLEstfdYpa9oBcdKG7niQKX5e7oNslQ0f07dhAEvLerF4nCNBRvMLi0BPqKE3Um56PCWoGDSFcf4qt0DTVmdTfkNFRSDQdPUdJmjf7dB+OYtIJAnQUr2Sxo/RWHeUpgppBYwq/3s1WqJcqpL7CfJa0Xna4u+4nCq+Xu3BSKeiY39Cjo1h0PPXGbWseK6Oj+NNIpKPcpQ7KOwhqeo0awv1RQ67uqC+2bHz3aotQzkpF6DO17G1xHZ/MqtQbvxeMzPfkKAQd8vMtf6CjeCWLHWWqOib7EtT0Gifyq1XVrpKfu7xb16z0mCJUqX4nqTZq2d7vL6M9jETg5QrljdwJBKibJeo8k74yNegoXsliR/lRHZKdCGp6jQuF9enq7p+blS5WN40wb8pAPFyherNIfkLvKGSdHbTdcdman8roKP40Euko2rdn8524ebTfYhrC/U37F9mbTQZCf4WaLSUbCq2j2Om0puyPu9Z8VUZH8aeRREdprA7IP0lqeo0xphG81FzhD2XLNg99TxrUV6juMhtDoXUUO52L6PrjsjVfldFR/Gkk0VHOUAfk/0hqeo0rTSO4spapgjo1IWTB2z20Vyh3OthB2awdHdPXpgUdxSvZ6yjXqwPyI5IagiCIjBtHeVDd+0l0FARBHHDjKK+qe1t+oImw5wiCxA83jvK5uvcl5k0WjSeM8r+aK6iJlyzhtxmIy/OrMA1smMboOco0uu67bs1XZXyO4k8jic9R/qcOSUvmaYujHFlhGMP/MlfQnsy+6qHzCYPyCq0EMsX0Ufg2OnTdd92ar8roKP40kugoa9UxeQhJzajxmn4M7yoyV1inbnvLQ+cTBuUVMgfNy+xuS/+moI1OEKCjeCV7HWWrOiaJakaNVlt1g3iopcI+dZv9G8oZA+UV+oZoBJs6e3j32EYnCNBRvJK9jqJGpS0mqpk0jlV3Tz2Ra97/SG2EP6CV1nTf/URBeYUmkYxgUVOOiaMsapq+oifQUbySvY6iTrfzIVHNrNFSfh7wx1lWqb7aEB8uF9V8fCv8PoyYRjLpUF6hHpUWHygZXUsSomzWRicI0FG8Qjj0CRPOo9VIoqMsVMblZMsmkqNw1fo999mrd/ayvHjMM0Eb5FfIRZ+Jaw+57X+SoL1CN5p8YP+EQxQhymZtdIIAHcUrhEMHmEirkURHUV9jvZ2oRtML7YdoOE4q6SOtVTajUEkK1Fdo1H6dDxycomZ8oHYUG50gQEfxCtFRHqTVSKKjvKuMTUs4Cq2j5GpzIW+Wix6y1Y4QRteJXqbR+B3S6TgwY/iReiHKZm10giAbHYVNr4mOMjaKnvgS8+AoLyou0JWoRtGL07S/nK/JRffJ65T3j8ESmaPwFHUZMPCMNjVMQvTNknSCAB3FuwqhaHQUPfEl5sFR/k9xAeudCaWjPKU5yjVy0V+k1X2N3KsET5SOQhaKpNngW0NHMReZ866G0hNfYh4cRfkaAflENfe9yFEnZIcqdX6e54TV1A2uRcIAHSWk1tBRzEW3Mu3JHVQGFZqjDJRdwJJvidZRTtW+ouh+iB7y398/I/zQHCXoKCG1ho5iLrqRaU/CGDgeHKWD7AJryGrue6G76enuulIUoKOE1Bo6irnoWqY9iamj1JSnAjRPKMhROkr9PaqhLHBbJxrQUUJqDR3FXHQl057E1FG4YskGvierue7F3dpXFPMsHTEDHSWk1tBRzEWU88wk1FE+kmzgR7Ka217kqy/8QLHlhZ94gY4SUmvoKOaii5n2JK6OIsfOrySrIQiCyLhylKukfTehoyAI4ogrR+ko7bsHHQVBEEdcOUq1P8V9U9aUA+41GmrT8L7vqkKUuD2ocGTi/RzFF66HD7VsAKqs9YnPUbox7Ulcn6NwH0tWUIeo5k5jimoo+4LK/cMOdJSQQEcxF1Fm2iP3pHDC7bZNUIu5qEXvKCMkLziKqOZK4zgtm9BIt12NDnSUkEBHMRedwKInbWCFbRPUYi5q0TuKHDXbm6jmRqPaAtVQluS57mtkoKOEBDqKuagNi54QHaVw2LGexFx0gd5RcraLZnALUc2NxgOqoRxo77qr0YGOEhLoKOaio330ZFGp7BlWR6lz1WcV0INGjKYL9I4iJ12yTFLq1lFO1e55hrjuaYSgo4QEOoq5iDKXoaEnK5RvOCZHyb/gbTGpX5wc5SbRDWYQ1dJr1PtdNZRkzNKDjhIS6CjmosOEfwpada7noSdER8k57TnlZ9Y4OUprsUfFRLX0Gq+rhvKbyxMVMegoIYGOYi5qyNUc9q1wWtZOP5O2JyRHmbhe/fDFylG4JcLOFZYcg64cRXtDcEsw09oxBx0lJNBRzEV12i9RPy4fWH9cFSjodsnQEX07NrD0hOQoeugcRd9MmlpeHGW02CVLVhM3jtIvlTRDQUcJC3QUc1Eb4RZFeey4y2opTUfPKZO3zj49OEcxNZOmlhdHaS7agiWUxIWjdDmQOENBRwkLdBRz0RJY1L8wt/Vo6VPzs2m6zcJJpXqLmN/QtaPsfaXYvaNYmklTy4ujSJPyTiOpOWs036L0a3NiDAUdJSzQUSzC70qPFjqVix+aR/Vb643fa/zSAfMdHCW/t+ooVV9cXZv70q2jEJqp7lzLk6MME/beRlJz1GiyUunVL61dtxU56CghgY5iLlquPKscJ35qlmvb8kZqr8bp0fbQOUpxn6klIH8+l49qIhS6dBRiM8841/LkKIUVwu5mV0jnKEf+pvTpA9KkpXEFHSUk0FHMRf2VRSnNe0q94ainTu2Z1lGKxihb+C8BT54kb3XnKORmdjjX8uQo0vzEgwlqDhot18o9qro3UVOlo6OEBDqKuegUZbG59MlRfkJuttTGUMyOUnTT3Ep1C4D2zosrR7FrxuEGw7OjXC7s/h5BzV6j9Qa5P7tiNWNgetBRQgIdxVyk/rojz7/ZUlqru8zOUAyO0lOzE9lRtK2uHMWumYsca3lzlDzh+8a+WlY1W40em+XufNzYfTOxAB0lJNBRzEVqxpB7xI+OfLuRO93WUDSRDpssW6gdxY6OzrWsi264leBVDn1AECT7oHCUgh38/lPRURAEsYXCUbj7+f13GrObRN19BEFiBY2jHCq8Em3MukTWKBwn5VOB9YNiPjGPDZQnRsY5oNGfEE11r81GAO0QdC8bgCprfdJzlN/khSHild95pLQ2ze7jO03tiaF4K6yuaWnC8hyFNF5tmnE+DK/PUTjuSb7CRxY1s8bxz8px9xvuMsUQJwYvIyZdQKM/IRoBdJTkOoocPV9bfMia6iMXrwQyxdofLa1wzcTObeEXaxMmRyGPV5tmnA/Du6McWQZQ1cKsZtBoNkp5dXLBgASkf7SBfsSkD2j0J0QjgY6SXEdZJf37lHjRH1CKzZ99md1ttZ5odsIJMbPpHMVuvNo043wY3h1FjAx+zKym1yiSX1jc8M+T6ZTjBfWJcRHQ6E+IRgMdJbmOIt31XCmcl8phavE3xDGxqTNncJRUpfJTLMlR8n7UOYrteLVpxvkwfDhKjWKAEn1IimW037L4wIpPHuycqAhZK7Qnxk1Aoz8hGhF0lOQ6ygbh/x2EB5Z7dFGhk0hDYlFTfU8q5w1r/Iv2Xo/ZUbo8tU2XzcB+vNo043wYPhyFO5uv8jeTWmKGr3soD8pVQKM/oQB7HyWRO8qECV7CuYNzFCGircFqXn/l8briHpWWAVEyupahJ0X8f3aOcvTYVWIdxVEcxqtNM86H4cdRuLf5O5oCo1pihq976A7KVUCjPyGHkEW/vY+UyB0FYGKg+s4q1qJyjiuYx8u/apxt70bTeNg/4RBCT4h5ZhvdrM5sIzuK/TB7yK4Z58Pw5ShH/Alwn1EtMcPXPXQHdYu9odCdG1uhqrR/KLz3PlJi4CgPBqrvrEIoqlObN5R9g8wbRu3XDYeDUw4n9oTkKNMPavVkR3EYZnbNOB+GL0fhhgPs1RpCR+G4mubXKbw6ir3QzOB6Hy0xcJSxgeqbMeaIJQj34+9IFhOm6mo0foc0Fg7MuOsSX3lmHYeZrpnhR7o7JL+OUm0mwAsGtcQMX/dQHZTTVxSqc2Mv1DW43kdLDBxldKD6Biw5YgnCKYCnbcK4iroMGHjG6ff6zTObbpiJzbSxJKm3xa+jcPV/hSr1oTE6iquARr9CAfY+WmLgKHcEqq/DTSQ0X76rL52GS0dZN/EX2VFYDTNdn/05Cte6BDYp9z3oKK4CGv0KBdj7aImBo9waqL6Ku0hogIXNKTXcOMqWf3bPUSPcWA0zrc9+HYX7awXMz9P12FtH4gzVQbkIaPQrFGDvoyUGjnJjoPoybiOhUxPtA82p8swKjnKsdH53vdSrmlCoOAqrYabAwFGELNb/p0kkZvi6h+qgXAQ0+hUKsPfREgNHuTZQfQnXkdC9CZXTaNg4ynHjlvFbYP9bFyl57BVHYTXMFFg4ivDawQs1FInEDF/3UB2Ui4BGv0J0JOiSxMBRrgxUX4RFJLTrPLM8+YOVLQNra1sVR2E1zBSYOAo3KgXfNuHQUQRcBDT6FaIjQZckBo5yWaD6AiwioV3mmeUdJf/cl0uI8oqjsBpmCmwchbtoL3zGoaOIuAto9CNER4IuSQwc5eJA9TnHkGoGGvpo6hVwgmYnto7CapgpMHIUrsO62Zz5924EQbIc79Z02Hh0FARBjHh3FImo+48gSIzwaygZCqMzE9EJxuvq/gwAdAtU3zmk2r+GvksGUgvvbGEUST9fDxIY6CjJhsZRvMRh0Jxhp5Bq/xr6LmkchA3WX4PRUSIEHSXZ0DjKCYHqO4dU+9fQd0lm3zuXdlIyLulBR4kQdJRkQ+MobQLVdw6p9q+h75JsJwW6HG560FEiBB0l2dA4ytGB6juHVPvX0HeJZ6iUXxEdJW6goyQbGkdpFqi+c0i1fw2tS2se6/qr5d1jPegoEYKO4p5m9xVRFIcDjaMcJvxT0KpzvUD0OceQav8aKidxpMzVerqe08B9pxG2oKO4peXz5dDedXFY0DhKQ67msG+FT+na6Wey1xewzxHrX8OANT8KEiW6FKA+PpPGRKIZ7ijHTK3gG7NYh01xeNA4Sp32S9SP6gdH2e/p48La5oj1pmGbABYdJUYYU4B6/UxaEolm9AON9m9WiYfa3lVxmNA4Shshj5HynGKXjaX4vrDkHLEeNJwSwKKjxAZz+k5vVuCcBDTjaLf04QFzrdZhUxwqNI6yBBb1L8xtPfqAeNF+JmWNZnNh3eSZ9Qc6Skywpu/0MmLSJQHNSI4oJ1qHTXFo0DgKvCv91e9ULl60Ry27sLmw7vLM+gMdJRa4TQHqSSXTHYUrJluHTXFY0DjKcuU2Ypx4wZabdmBzYdkMsnSgo8QB1ylAPalkvKN8TbYOm+KwoHGU/sriqeIFSxkzwrO5sGwGWVpUR2m1fi5jacQtLFKAuksCmpnMJVuHTXFY0DjKKcpic+mKGX5CZnNh2Qyy9Kzw9EoBwhIWKUBdJgHNTGaSrcOmOCxoHEX9dec06Yq11G1lc2HZDDIXoKNEhe0wobvmjGQSzadAtA6bYkZQnPh0lwSgjqJ6j1i8g06fTScZnZdBIzxO4oX4hNG1Dn/IxI/EO0qZqirdmrxAp8+mk4GdKSQcGF1rHDIZ4Cg7FdHeYmmqHZ0+m04GdqaQcGB0rXHIZICjbJQ1c6VY/E8p9dl0MrAzhYSLbfpOqovMeq77RBGJo6TF/fWD3+SFIeIl26l/ZcYpQyyLPLOuJZCkYJu+k8pRWM91nygS7yhyKFjtTcIlS/XRb3PKEMsiz6xrCSQp2KbvpHIU1nPdJ4rEO8oq6d+nxGv2gGGbU4ZYFnlmkYzDNn0nlaOwnus+USTeUaS7niuFS1Y5zLjNKUMsizyzSMZhm76TylFYz3WfKBLvKBuE/3cQ8hntOc+0zSlDLIs8s0jGYZu+k8pRWM91nygCdpQJE8wfc1dQOIoQ0dZgNV9h5fHmbU4ZYlnkmUUyD7v0nVSOwnque390GXzvyAGNQmsuYEcBmOitmmtHKee4gnn8/q/WsW50yBDLIs9sRESaATjjsUnfSeco7pKAhkHOsGKxDxXvNw+pxcAd5UFv1SiyQtbmDWXfIOJW+wyxLPLMRkLEGYAzH3L6TkpHcZUENASK5kDp3zvV7/E+/xHpF06TgTvKWG/V3DtKv2UAi4+12WxzYSnHR0yGBxeDDMBZASF9J62jkFXCpu5PsKWruHQbQOWAUNoM3FFGe6vm3lFSAE+TUkEqkC4s/fiIwfCIRQbgbMWDo8SAaQCXy4uv87frobzZHrij3OGtGkVWyF19A9SPE3HIAJytJHLEnAawPFdeblgK8FNeCI0G7ii3eqvm3lEWenjklMjxIRJ1BuBsJZEjZj7AXerKK/whXB1Co4E7yo3eqrm9fqmJXnw3keNDIuIMwNlKEkdML77T2uPYs/i1xSG0OoNv5zjXxdQAXOutmtvr19uLfCLHh0zEGYCzlSSOmKf5Tmuh3YVgWA2MOXwznVwXUwNwpbdqwV6/JI4PmYgzAGcrSRwxX/CdbqatCr9Xjgy+1QV8M39xXewIKT4W4DIvvUJHsSXiDMAZCrgn6q66Zz3f25O1VeHb7ceBN5q7lW9miNtiZ0jxsQAXE/dkgGNPMnB8yET8xlWGkokjpiAF+uco3Itgnc2KOY1fFc5RyVl5rorTQIqPBSC910Nx/Txd2UwcHwroKEGQiSMmXwiGHKGt38evbgm2yRn7lLNUsa1d2uK0kOJjAXoR92SAY08yb3wooKMEQUaOGCFX2GRtdQK/Wma/dwwhxccC9CTuyQDHnmTg+JBBR4mEJA6Vj/hOr9XuM6bwq+sj7A49pPhYgG7epPDJrA3oKJGQxBHzsPAnUwtqExImz4+wO/SQ4mM9/gKOjmILOkokJHHENBEeXyzLUVZ/4tdeibI/1JDiYwFO8CaFjmIDOkokJHLEjBK+pNwvLeded4BfGRdpf2ghxceCt5l80VFsQUeJhESOmOrLBUt5rjHHNbhosfjY8Jqou0QFKT4W4GhvUugoNqCjREIyR8wh/xF9pPg3qHpNeDBbemjUPaKCFB9rCAOmkUJHsQEdJRLCHzG5Lc8dMfLCNvn+VG4Wk0LufKONOKdDsh6jEONjAQ4T/ilo1bkenVQGOUrzc2+/46/MMgejo0RC2I6SM2Q7bwSbAUpu85nUpEGvC4W8g82ECNpTmPQtNEjxsQANuZrDvhV8cu30MymkMsZRWn8oBb4sYjRjGDpKJITsKG2+hd23FvF2MGg7rOjIQvFOYQyyEAoRUnwsQJ32S9Rwsg+Oci2lv34F3S4ZOqJvxwb+uqdXCW98XHVQOfh9bJ6KoaNEQriOUrcYNhwhLR62BTYU+lestS5xz2XJ8bEAbXbyh6JMebPLpaXorl/T0XPK5NqzT/fcN5NKaOOj90HYvfCz9VLLZ7FQREeJhHAd5XWAHsryQIC5OU47u+J+/gDe960SMqT4WIAlsKh/YW7r0QfED9XPTjmm9dXk61c4qVQfMz/f2+zlFpWwxkeLvVtvELJdtxGnOv3V51M2EXQUdhROuN3trqE6SkeAdeqK8MKf75TTzfYDrKnvVyVsSPGx/IV4V0og36lc/DQ/6lJKvH71xpunMZ9fnb5fBJWwxsfrS+UkuLkfA6MHY+go7GgDK9zuGqqj3ATwhbb2K31iEQv/ATjYxa9I6JDiYwGWKzNSjBM/zO4SNIjXL2/kTrDwDG2viCohjY8Tt6rTIzfezbd5EwNNdBR2xNVRXgLYmauu8Y7yiE/BsXz3h/vUiADSlzOA/sriqeIHOeXqvkW4fvVmkYxgB2WnyCohjY/jdGnwPgCPWbxNsMoAnMUsKpUnjIuro7zPt6b+wNMw5TFZs8YVAOWDffYpCkjxsbpv+s2lT7Krn5D5/ZotJTtBa6o+2amEH+H2ANDn2STBKgNwFrNC+dMXV0eZyLc2W/mScj5AWRNfcheWwdbu/nsVPqT4WAD1153TpE9yS3dSsMzGCS6i6VJdO5XwHWUkwAr/j+y9ZQBGDBAcxXaYRDJwhIkwYLy88rwhbRI91ScDLI52bl2vkOJjAeooi/eI12OHVMoAx57EaXxITNEmjPSDpwzAiIHYOwr3C99OlfTUjf+K8nVt70q1rlwMm+8uYNSvkCHFx+rS0En3Hy9IezLAsSexGh8COathKgMZbxmAEQPxd5TuYlzkP/mr3HEnfEf1AouOpv3vnqHu64MAAAzmSURBVLobVt8U8Wzd3iHFx8JOZWtvsTTVTtqTAY49idX4ELgIvvT/h8JrBmDEQPwdhfub2NQXDU4qgec9f0O54O0nb+ndMjf9jnGFFB8LG+WNuZLXfCrvyQDHnsRrfHBcs+1fJPSbZwYS+yezPPeKo7N413aq54YZBik+Fn6TNw4Ri3aSnxCRYlrJTKPp0DQmKizovgGm0f1IhQSH0VHyXU10G7ajcNdLf5mT9ioOU4AQH6v8Eai9SShI9SHVI8e0EimmisJfyUTFP61fEGZOqZhcLdxmERt0jlLcZ2qJK6sI3VG4C8S/y5XW3M3ZAyk+FlZJBU+JBQ8QatnFtJLYTZcRwGxU3lT8Mmxxldzwm2gpsUBxlKIx0nVxUyd8R7mrSnq39TkWb4MlE1J8rHzXc6Vot8MIlWxjWglsosyr/w0TFb+0OPvej7dJTT8RbssIGdFRim6aqzzxc1MnbEep+Tq810QawDM8vMuWGZDiY2GDsNphP7+yhzRfqX1Mq5VFTQkCTkxiosKC/FHCGYDyKNpGzKyAnpqdxNNR6n4HM/K46v8W+/dutn63JcXHihFtDVbzyyuPJ1RxiGk1UzK6Fm2HelSyUGFD8/8KzeOXlBjQYZNpULipFK6j5M2C3WLGpQfFDrp7YT/zIMXHQjnHFczjl1+tQ6iRO93OPx4yre+fcIiHHt3IRIXjLn/4Yd+5JQqFO58f/aogPun8SLFlsLmp595R3lyj8i+vvXxGnZ9zuNDBg54mlEg+pPhY3mVq84aybxCxxi12hlJVS7pNkDk45XBvXWKjcnIFgP8XI67gu7DLtwriD8Jg22+7sy6RqGtHOVmn7D6xspG2VVBZJC/fJQi95VEo4ZDiYwH68Tc2i48lVqhp/vqpMpPjGo3fIS0fmDHc+8eZhUqB8Cu0f0fJ287LJDYgOlMwj7S9b11qE3poTCTq2lE+1rR/8trJ1wC+VFeEeXb2snjHNHmQ4mN5XwF42iYVpO1XFOgqbi/qMmDgGW38fgh9qzwDTByFewWk59RIhBiG2VZYbZel1Bx06dZROukqeX4zdK1+Zp38FeDyjf2MgxQfy/+7q69dhfjEtDpxHjBylPsBPvOvgvhCG2RrJnZuC7+Q97IGXbp1lA9hYAsFr2/U1EoZHsZeB7o81lkFKT4WYGFz2wpxiWl1pHBLxWY2jnI3wOP+VRBfaHbCCTGzREexCbp0I98h9QODTu4CeF1baw3CW/3ZCCk+NjXR4b37eMS0pmEajPmSjaO8DnC2fxXEF8LfukolbRfZUeyCLt3Iv0+XEcyGuQA6Y2oIsJqBaAIhxcc6voUVj5hWZ66Hr6qxcZScVTCdQYcQX1TOG9b4F+29HoKj2AZdulA/LrWYxTPUOwH2a9Pa9pSzCmUf6eJjLcQnptWWo/f+2YJj4yjDoNTtlIpIYAg/yjo6in3QpQv1t+GLXgx+zstfAvCcuvYMrPc5nWZSSRMfayVOMa1kqi2AqzjvjtLi4SfU+5x2e2EUu44hPggs41Jb4Z3QfR/daM23TEmXA1B1gbx8AVRma15h5/hYEqxiWgPjPjG2yLOj/MBX/F76unb9vtTdLHuGeCcwR3lD2edfPjLDihz7I6QmHcovNJhcue6CtLtnKM7xsUTYxLQGxskV6wWL8+ooOX+Ix7XqtYfeXgNrbH9ER0ImKEc5pkrdaZXfCfzyH/oTYO28danyCdmb/M8xPtYGNpGxAVGwsup04V/P31FO3SAPsMqFt2btK+nxIyhHOWfqrCV75L0qxvp+Ybh5n7/f2699No8bx/hYe9hExgbBs/LskN6fzOaecfN9j4258YIsfbIWUxzyzPoOuszr/sByqQa+Z+4bcIqPTSDnw09S+ixG8ShITHBwFBZBl7k3bBGqpE5j1uFsxTE+NnkUbjkgDzx0lMzC5Cj623Q2QZd1XxMqrfb7eDbrcYyPTR7TYKi8hI6SWegd5bhxy/RPRhgFXeZOFapNYNXhbMXVLAWJYQh8rCyio2QWiqPkD7Y8a2UVdJn7Hl/vW0b9RTKBo/duVXLeoKNkGKKj5J/7cglYHIVZ0OUR+wEOZGt+WMRKtYVwvrqCjpJZrIATNDsxOgq7oEshr2l7Fr1FMoKx8LS2go6SUTRaB/sNrmHYyirosjHoZptBks15a0xQp+c7pgK++6/Kbn5wLOT/PT99RSTmHHbT7ArzfY1xD1ZBl/yXoF6+uorEhhnmIfMVrUJP0gM6GBJEZ5FQqSJcV8tOTIIuvwJo508BiQktLKOGeu5YdJRMxXxNUwvvbBFMSwtge0ZFU2QxE8ShUnpAJgVVR9BKtH5aj5Dl8lX+3+5B9BYJFYOdHIQNgWXjyd2nS3GCJJn8LfB5vyPUF6xq7YP5PhXxyWzmoNnJvncu7WSXuZoB7aAMb3oyg/6Vf9dn5usLQJrBnQZ0lMxBs5MC28zVTPgYbg9MGwmVOWMMq29Bld+0K+gomYNkKEOlnCOMHaVmu3x1+VqYlZ2zdmUeh3xoiFSstRfm+ZVER8kcYM1jXX+1f/fYDz12wZpzpcWcWw5sa8xQGokPl4D6wp9n0FEyh5O4NJmrvfOC8O1nds8a3KG9Z8GcWCVgR9jxpjYntWfQUTILh/wofugn3VEJE8aV3YG3PBlKzT0wx7cIOkpmEZCjcMPld4U2T27DUhaJExcD3OhbBB0lswjKUbiCfrc/PObqU/GV4wzmDagsjLoPSMwIzFGQjKfGHpgddR+QuIGOgnjlQoC/Rd0HJG6goyBeeQ0qGqXfC8kuVEdptX5utD1BEkaNP+HzqPuAxA7VURCEjgswAwFiBR0F8cirUHFo1H1AYsegEbbzeTW7jxAPWbPnsHsux7vnmFN45vA7elHnLaGj+m6YGWwLSEbR8vlya7bpvBv+EMLWyl70mMIaCYOOP0jRhesvDbKVPgDXBamPZBTHTBUy0JodpeZMqBzXrs19q2Fth0i6haQn/1EtefC0JsG1MxUOUkxXi2Q17d+UkomaHKXW5wAXCgtNNsP/t3d3IVKVcRzHd9eZ2TRfLsXS1g1RDAlRV8IUBM2yoMQojdSN8ma7SUkj1FREDcSI9kboxWAJUrvxJZdI9GpRLxJXCsrVirSL2t3ZVVltZnX33/PsOPvMPLs6Z8DnOYfj93N1foeZM3/Y4TdvZ5/zz5QwBkNpOwtX5msb7ephUt3S7OrYiJmnfv54xalhGuWoyKHclnrHe/ER/4OhtHl3pH3z4pq6hpaBStnv6nFeFHnL1bERQxOyQxpF1UimNrdZ2SayK4SpUErisjTm3pdUbRn49POKowf6WrJ8mYYyXLIbJfGryPf5sEGkl6VjI2iBfDa4vVE3SpObx0l2mScDEECL3SgNascH+TBHBZa3j6AdZ8xqNIlW9VdytHrwUpE1bo6MmDplN8pPascz+ZBSH4quj/I/FUo4W3ixz9fVn6zPzXez+yU7zsmBEVc/WI0yvl8kY1aj1qc8rPI/Fe6vsugCf9P0xx4nvZ9MyzEXx0V8HbcaZY3KV03cp+IX3odCWUaod5IdTo78vMhqJwdGbNmN8q3KrSZuU/G896FQnh55AAvBDudLyYx1cmDElt0of0rRs3OdXpeaU1KibZw4WhMpkZYjLo6LGLMb5aYMnt+mva0/ok/1PhXKsVDkPydnyk85cOA5F8dFjFmNMlI3yD6TBy6fUed/LJRhr8iOsGcAcqxGeUI3yE6Tl+jM61SkJa/IVX7hR0RYjTJbN8h6kwca5VX/YyG4epGVYc8A3GU1yjzdIPUmv6TzUv9jIbDUb8LSwYgMq1Em6wZ5x+RlOs/1PxYC2yJXxoc9A5BnNUqqX+WNJq/UjfKk/7EQ1LTMrdlhzwAMsn89/lfl3Sbq/xsUTnKKrpEX5M2wZwAMu1HOFf96vEnFrPehEFiT7Al7BKCA3ShHVD5o4qcqnvY+FIJaJ99Ulr4V4I3dKFtVPmHiYRW3eR8KAb3WdzxZ+laAP3aj1PSLdJiXvdbC1VIQMQszLZzahmixG6XiR7Xj6XxIZUTSVf6nQhBzrp1nOSREzJBG0b8Xv5cPdSo0+h8KQczqulh4NchJfKGCCGhWnTGjcEd1l8jhfNgscmOYa5giAmam/5hYEFf/EtokgHFSNcqsoj2bRLqr725fEvnI/0wIYGbnX7UmjWro/TC8WYBBp1WjzC/aM+KsyLu5zZdF2h4NYSiU9Ow1+W5vzieNnx/tlr5JYY8EVFRU6XNk1xbvm9op7ZP1Rm1aLk8c5k4I3ZKbYuG/BREBjzXpJ2PX4kTR3ul/y+8vJEfXd0gbL3yRtDxrFwrXEkX4mnvyT8fb7UVXDnz8q9vSe0c611ff664IVc+QQrk1JuyZgPuoeWP7+4vcXFQKAAAAAAAAAAAAAAAAAAAAAAAAAAAAAICHzv/4R/vjLwRhCAAAAABJRU5ErkJggg=="
}
},
"cell_type": "markdown",
"id": "d6e0a002",
"metadata": {},
"source": [
"Elliott Carter often bases his all-interval sets on the list generated by Bauer-Mendelberg and Ferentz and uses them as a \"tonic\" sonority. \n",
" Image from [commons.wikimedia.org](https://commons.wikimedia.org/wiki/File:Carter_all-interval_sets.png) \n",
""
]
},
{
"cell_type": "markdown",
"id": "933bccbf",
"metadata": {},
"source": [
"The problem of finding such a series can be easily formulated as an instance of a more general arithmetic problem.\n",
"Given a positive integer $n$, find a sequence $x = \\langle x_0, x_1, \\dots, x_{n-1} \\rangle$, such that:\n",
"- $x$ is a permutation of $\\{0,1,...,n-1\\}$; \n",
"- the interval sequence $y = \\langle |x_1-x_0|, |x_2-x_1|, ... |x_{n-1}-x_{n-2}| \\rangle$ is a permutation of $\\{1,2,...,n-1\\}$. \n",
"\n",
"A sequence satisfying these conditions is called an all-interval series of order $n$; the problem of finding such a series is the all-interval series problem of order $n$. "
]
},
{
"cell_type": "markdown",
"id": "5070544a",
"metadata": {},
"source": [
"For example, for $n=8$, a solution is: \n",
"```\n",
" 1 7 0 5 4 2 6 3\n",
"```"
]
},
{
"cell_type": "markdown",
"id": "f898fcd6",
"metadata": {},
"source": [
"To build a CSP (Constraint Satisfaction Problem) model, we need first to import the library PyCSP$^3$:"
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "1500590b",
"metadata": {},
"outputs": [],
"source": [
"from pycsp3 import *"
]
},
{
"cell_type": "markdown",
"id": "118b1507",
"metadata": {},
"source": [
"Then, we need some data. Actually, we just need an integer $n$. For example, the value 10."
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "55ecd7d9",
"metadata": {},
"outputs": [],
"source": [
"n = 10"
]
},
{
"cell_type": "markdown",
"id": "b021c396",
"metadata": {},
"source": [
"We start our CSP model by introducing an array $x$ of variables."
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "55dbebcb",
"metadata": {},
"outputs": [],
"source": [
"# x[i] is the ith note of the series\n",
"x = VarArray(size=n, dom=range(n))"
]
},
{
"cell_type": "markdown",
"id": "fb942a15",
"metadata": {},
"source": [
"We can display the structure of the array, as well as the domain of the first variable (note that all variables have the same domain)."
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "347b7e18",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Array x: [x[0], x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9]]\n",
"Domain of any variable: 0..9\n"
]
}
],
"source": [
"print(\"Array x: \", x)\n",
"print(\"Domain of any variable: \", x[0].dom)"
]
},
{
"cell_type": "markdown",
"id": "23daebc2",
"metadata": {},
"source": [
"Concerning the constraints, we have to post two constraints *AllDifferent*: the first one on $x$, and the second one on expressions representing successive distances."
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "f7cd740d",
"metadata": {},
"outputs": [],
"source": [
"satisfy(\n",
" # notes must occur once, and so form a permutation\n",
" AllDifferent(x),\n",
"\n",
" # intervals between neighbouring notes must form a permutation\n",
" AllDifferent(abs(x[i] - x[i + 1]) for i in range(n - 1))\n",
");"
]
},
{
"cell_type": "markdown",
"id": "9c60eb3b",
"metadata": {},
"source": [
"We can display the internal representation of the two posted constraints; this way, although a little bit technical, we can see that the arguments of the two constraints are correct."
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "474b0cef",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"allDifferent(list:[x[0], x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9]])\n",
"allDifferent(list:[dist(x[0],x[1]), dist(x[1],x[2]), dist(x[2],x[3]), dist(x[3],x[4]), dist(x[4],x[5]), dist(x[5],x[6]), dist(x[6],x[7]), dist(x[7],x[8]), dist(x[8],x[9])])\n"
]
}
],
"source": [
"print(posted())"
]
},
{
"cell_type": "markdown",
"id": "d5b9a806",
"metadata": {},
"source": [
"Interestingly, by calling the function *solve()*, we can check that the problem is satisfiable (SAT). We can also display the found solution. Here, we call the function *values()* that collects the values assigned to a specified list of variables."
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "91ad3a0e",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[5, 8, 0, 9, 2, 4, 3, 7, 1, 6]\n"
]
}
],
"source": [
"if solve() is SAT:\n",
" print(values(x))"
]
},
{
"cell_type": "markdown",
"id": "194c0323",
"metadata": {},
"source": [
"One way of breaking some symmetries is to post this constraint:"
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "93f7d876",
"metadata": {},
"outputs": [],
"source": [
"satisfy(\n",
" # tag(symmetry-breaking)\n",
" x[0] < x[n - 1]\n",
");"
]
},
{
"cell_type": "markdown",
"id": "3df9aa7f",
"metadata": {},
"source": [
"Now, we can check that 148 solutions exist, as follows."
]
},
{
"cell_type": "code",
"execution_count": 9,
"id": "f6236c2a",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Number of solutions: 148\n"
]
}
],
"source": [
"if solve(sols=ALL) is SAT:\n",
" print(\"Number of solutions: \", n_solutions())"
]
},
{
"cell_type": "markdown",
"id": "b64ee584",
"metadata": {},
"source": [
"Finally, we give below the model in one piece. Here the data is expected to be given by the user (in a command line)."
]
},
{
"cell_type": "raw",
"id": "30dc8f40",
"metadata": {
"raw_mimetype": "text/x-python"
},
"source": [
"from pycsp3 import *\n",
"\n",
"n = data\n",
"\n",
"# x[i] is the ith note of the series\n",
"x = VarArray(size=n, dom=range(n))\n",
"\n",
"satisfy(\n",
" # notes must occur once, and so form a permutation\n",
" AllDifferent(x),\n",
"\n",
" # intervals between neighbouring notes must form a permutation\n",
" AllDifferent(abs(x[i] - x[i + 1]) for i in range(n - 1)),\n",
" \n",
" # tag(symmetry-breaking)\n",
" x[0] < x[n - 1]\n",
")"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.7.12"
}
},
"nbformat": 4,
"nbformat_minor": 5
}