mapa conceptual unificacion y resolucion - Mauricio axel 20

Vista previa del material en texto

Es un proceso que consiste en
encontrar una asignación de variables
que 
haga idénticas a las fórmulas que se
desea unificar. Su resultado,
el unificador, 
se expresa como un conjunto de
pares substitución/variable para 
cada una de las variables asignadas
(este conjunto recibe también el
nombre 
de substitución). 
ConceptoEjemplo
El valor de substitución
para una variable puede
ser cualquier término 
del lenguaje lógico
utilizado (exceptuando
términos con la misma
variable)
Dos substitucionesValores de substitución
Por ejemplo, se pueden 
unificar las fórmulas 
 
 
padre(X, hermano(Y)) 
 
padre(juan, Z) 
 
 
F s = padre(pedro, 
hermano(Y)) 
 
Si F = padre(pedro, Z) se
obtiene el 
mismo resultado (ya que s es el
unificador de ambas fórmulas).
s1 y s2 se 
pueden aplicar
sucesivamente con el
mismo efecto que una
substitución única 
equivalente s que
corresponde a
la composición de s1 y s2: 
 
 
(Fs1) s2 = F s
Si los valores de substitución de s2 nohacen referencia a las variables
asignadas en s1, se puedecalcular la composición s de la siguiente manera: 
s1 = { a1 / X1, a2 / X2,..., an / Xn } 
s2 = { b1 / Y1, b2 / Y2,..., bm / Ym } 
Ninguna variable Xj aparece en algúntérmino bk. 
s = { a1s2 / X1, a2s2 / X2,..., ans2 / Xn, b1 / Y1, b2 / Y2,..., bm / Ym }
Esta operación realiza la unificación de los argumentos del
objetivo yde la cabecera de la cláusula elegidos en las dos
acciones anteriores. Comoresultado de esta operación se
indica, para cada camino en que finaliza conéxito la
unificación, el unificador más general (mgu). Téngase en
cuenta que elmgu es un entorno de vínculos y, por tanto,
se descompone en entornos locales(0,-) y en un entorno
global (0)
unifica(glj, hd) = mgu = {{0j, ..., 0NCA}> 0)
Durante la unificación de un
argumento se instancian los
vínculosexistentes en EAV y en el mgu
sobre las variables que aparecen en
los dostérminos Prolog. Si en el
proceso de instanciación no se
obtienen vínculos queson locales a
caminos del árbol de búsqueda, se
realiza una única unificaciónglobal para
todos los caminos actuales. Cuando
una variable no tiene vínculoslocales ni
un vínculo global (la variable es libre
en todos los caminos)también se
realiza una unificación global
Existe un algoritmo recursivo que
entrega como resultado el
unificadormás general de dos fórmulas
lógicas, o, si no se pueden unificar,
unaindicación de falla. Para simplificar
la especificación de este
algoritmoconviene reescribir las
fórmulas en una notación de "listas"
(alestilo LISP) aplicando
recursivamente las siguientes reglas
Términos simples (símbolos de constantes y
variables): no se modifican.
 
Términos
compuestos: a ( t1, t2,... tn) (at1t2... tn)
Ejemplo
Ejemplo: padre(X, hermano(Y))(padre X (hermano Y)) 
Para aplicar el algoritmo de unificación, se distinguen cuatro tipos
de términos: 
símbolos de constantes (incluyendo nombres de
predicados y funciones)
símbolos de variables
lista vacía
lista no vacía
Una lista no vacía se
puede descomponer en
la cabeza dela lista y
el resto de la lista (en lisp
el car yel cdr). La
recursividad del algoritmo
se basa en
estadescomposición. El
resto de una lista de un
sólo elemento es una lista
vacía.
ConceptoValor de substitución Durante Cálculo del unificadormás general Algoritmos
La consulta siempre se expresa
mediante una cláusula que sólo
contieneliterales negativos: 
Q1, Q2,... Qi, ... Qn.
Las únicas contradicciones que es posible derivar mediante
resolucióndeben originarse a partir de esta consulta, ya que la
teoría del universo nopuede ser inconsistente. Para aplicar
resolución se debe identificar entre lasreglas (o hechos)
pertenecientes a la teoría del universo, una regla de laforma 
QR1, R2,... Rm. 
tal que la cabeza Q de la regla sea unificable conalgún
subobjetivo Qi de la consulta. Si u esel unificador más general
para Q y Qi,entonces el resolvente de la regla es la cláusula 
 (Q1, Q2,... Qi-1, R1, R2,... Rm, Qi+1, ... Qn) u. 
que conserva la misma forma que la consulta negada y
constituye un nuevoobjetivo por satisfacer.
El algoritmo de resolución consiste en
iterar la aplicación dela regla de
resolución mientras el objetivo
resultante no sea vacío. Nunca
seresuelven las reglas o hechos de la
teoría del universo entre sí.
Siempreparticipa la cláusula de
consulta o una cláusula derivada de
ella.
La expresión anterior del algoritmo de
resolución es no determinística.Para
implementarlo en una máquina
secuencial se requiere precisar un
orden deevaluación, lo que se puede
lograr mediante los siguientes
criterios:
1. Satisfacer siempre primero el
primer subobjetivo de la consulta,
luego el primer subobjetivo de la
cláusula resultante, y así
sucesivamente.
2. Ordenar las reglas y hechos de la
teoría del universo y elegir siempre la
primera regla unificable para resolver.
Cada vez que se utiliza una regla o un
hecho, se reemplazan sus variables
por variables frescas creadas
dinámicamente.
3. Cuando ya no se puede seguir
resolviendo, volver al último punto de
decisión y elegir la siguiente regla para
resolver. Esto constituye
un backtracking que permite recorrer
todas las soluciones posibles (siempre
que no haya recursiones infinitas).
Estos son los criterios definidos en el lenguaje de
programación lógicaPROLOG. Además, cada vez que
se obtiene un resolvente vacío, se imprimen
losvalores asociados a las variables de la consulta,
componiendo todas lasunificaciones que fueron
necesarias para llegar a ese resultado.
function unify(t1, t2) { 
 if (t1 = t2) 
 return {} // unificadorvacío 
 elsif (t1 es unavariable) 
 if (t1 no aparece en t2) return {t2 / t1} // t1 se substituye por t2 
 else return FAIL //no se puede unificar 
 elsif (t2 es unavariable) 
 if (t2 no aparece en t1) return {t1 / t2} // t2 se substituye por t1 
 else return FAIL 
 elsif (t1 y t2 son listas no vacías) { 
 ct1 cabeza de t1 ; ct2 cabeza de t2 
 sc unify(ct1, ct2) ; if (sc =FAIL) return FAIL 
 rt1 (resto de t1) sc; rt2 (resto de t2) sc 
 sr unify(rt1, rt2) ; if (sr =FAIL) return FAIL 
 return composición de scseguido de sr 
 } 
 else return FAIL 
}
Algoritmo de resolución
con cláusulas de Horn
Composición de
sustituciones e identidad
La 
composición de las sus�tuciones σ1 y
σ2 es la sus�tución σ1 σ2 definida por x 
(σ1 σ2) = (x σ1) σ2, para toda variable
x. 
Si σ1 = [x /f (z, a), y /w] y σ2 = [x /b, z/g (w)],
entonces
– x σ1 σ2 = (x σ1) σ2 = f (z, a) σ2 = f (zσ2, aσ2) =
f (g 
(w), a)
– y σ1 σ2 = (y σ1) σ2 = w σ2 = w 
 
– zσ1 σ2 = (zσ1) σ2 = zσ2 = g (w) 
 
– w σ1 σ2 = (w σ1) σ2 = w σ2 = w 
 
Por tanto, σ1 σ2 = [x /f (g (w), a), y /w, z/g (w)]. 
La substitución identidad es la sustitución tal que,
para todo x, x = x. 
 
Propiedades: 
 
1. Asociativa: σ1 (σ2 σ3) = (σ1 σ2) σ3 2.
2. Neutro: σ = σ = σ
ConceptoEjemploPropiedades
Comparación de
sustituciones
Def.: La sustitución σ1 es más general
que la σ2 si existe una sustitución σ3
tal que σ2 = σ1 σ3. Se representa por
σ2 ≤ σ1.
Def.: Las sustituciones σ1 y σ2 son
equivalentes si σ1 ≤ σ2 y σ2 ≤ σ1. Se
representa por σ1 ≡ σ2. 
Sean σ1 = [x /g(z), y /z], σ2 = [x /g (y), z/y] y σ3 = [x /g(a), y
/a].
Entonces,
1. σ1 = σ2 [y /z] 
2. σ2 = σ1 [z/y] 
3. σ3 = σ1 [z/a] 
4. σ1 ≡ σ2 
5. σ3 ≤ σ1 
Ejemplo: [x /a, y /a] ≤ [y /x], ya que [x /a, y /a] = [y /x] [x /a,
y /a]. 
ConceptoEjemplo
Mapa conceptual: Unificación y
Resolución 
Integrantes del equipo: 
Carlos Alberto Cantú
Palacios
Salgado Gallardo Edgar
López Anselmo Mauricio
Axel
Abarca López Alberto
Josué
Silverio del Valle Gerardo
Unificación y Resolución
Unificadores
Unificador de máxima
generalidad
La sustitución σ es un
unificador de máxima
generalidad (UMG) de los
términos t1 y t2 si
– σ es un unificador de t1
y t2. 
– σ es más general que
cualquier unificador de t1
y t2.
1. [x /g(z), y /z] es un UMG de f (x, g(z)) y f (g (y),
x).
2. [x /g (y), z/y] es un UMG de f (x, g(z)) y f (g (y),
x).
3. [x /g(a),y /a] no es un UMG de f (x, g(z)) y f (g
(y), 
x).
Nota: La anterior definición se extienden a
conjuntos de 
términos y de literales.
DefiniciónEjemplos
Unificación de listas de
términos
Notación de lista:
(a1, . . ., an) representa una lista cuyos elementos
son a1, 
. . ., an.
(a|R) representa una lista cuyo primer elemento es
a y resto 
es R. 
() representa la lista vacía. 
NotaciónUnificadores de listas detérminos
Def.: σ es un unificador de (s1 . . ., sn) y (t1 . . .,
tn)
si s1 σ = t1 σ, . . ., sn σ = tn σ.
Def.: (s1 . . ., sn) y (t1 . . ., tn) son unificables si
tienen algún unificador.
Def.: σ es un unificador de máxima generalidad
(UMG) de (s1 . . ., sn) y (t1 . . ., tn) si σ es un
unificador de (s1 . . ., sn) y (t1 . . ., tn) más general
que cualquier otro.
Aplicación de una sustitución a una lista de
ecuaciones: (s1 = t1, . . ., sn = tn) σ = (s1 σ = t1
σ, . . ., sn σ = tn σ).
Entrada: Lista de ecuaciones L = (s1 =
t1, . . ., sn = tn) y sustitución σ. 
 
Salida: Un UMG de las listas (s1 . . .,
sn) σ y (t1 . . ., tn) σ, si son
unificables; “No unificables”, en caso
contrario.
Algoritmo de unificación
de lista de términos
Algoritmos
Algoritmo de unificación
de listas de términos
Procedimiento unif (L, σ): 
 
1. Si L = (), entonces unif (L, σ) = σ. 
 
2. Si L = (t = t|L), entonces unif (L, σ) = unif (L,
σ). 
 
3. Si L = (f (t1, . . ., tm) = f (t1 . . ., tm) |L),
entonces unif (L, σ) = unif ((t1 = t1, . . ., tm = tm
|L), σ). 
 
4. Si L = (x = t|L) (o L = (t = x |L)) y x no aparece
en t, entonces unif (L, σ) = unif (L [x /t], σ [x /t]). 
 
5. Si L = (x = t|L) (o L = (t = x |L)) y x aparece en
t, entonces unif (L, σ) = “No unificables”. 
 
6. Si L = (f (t1, . . ., tm) = g (t1 . . ., tm) |L),
entonces unif (L, σ) = “No unificables”. 
 
7. Si L = (f (t1, . . ., tm) = f (t1 . . ., tp) |L) y m =
p, entonces unif (L, σ) = “No unificables”
Entrada: Dos términos t1 y t2. 
Salida: Un UMG de t1 y t2, si son unificables; “No
unificables”, en caso contrario. 
 
Procedimiento: unif ((t1 = t2),). 
 
Ejemplo 1: Unificar f (x, g(z)) y f (g (y), x): 
= unif ((f (x, g(z)) = f (g (y), x)),) 
= unif ((x = g (y), g(z) = x),) por 3 
= unif((g(z) = x) [x /g (y)], [x /g (y)]) por 4 
= unif((g(z) = g (y)), [x /g (y)]) 
= unif ((z = y), [x /g (y)]) por 3 
= unif ((), [x /g (y)] [z/y]) por 4 
= unif ((), [x /g (y), z/y]) = [x /g (y), z/y] por 1
Algoritmo de unificación
de dos términos
 7T3Zcts4tl/DKvnBLi5aH23Z6ZmpdCbLdKZzX27BJCwzTZFqLo6Vrx/sBAFQohaKksNUJRFBYj04+8GB5c2Xr7+lYPX8exLAyHLt4NXy7i3XnU4dF/2HS9a0xJ14Y1qySMOAljllwZfwJ2SFNistwgBmlQ/zJInycFUt9JM4hn5eKQNpmvyofvaURNVeV2DBerTLgi8+iKD22X/DIH9mE3MnZfk/YLh45j074xl9swT8Y9Zw9gyC5IdU5D1Y3jxNkpz+Wr7OYYRXj68Lrfeu5q0YWArjvEmF1dev6TT98C/3/7/99d9v0x9/vb58uHantJkXEBVsxmy0+ZovAQzQirDHJM2fk0USg+ihLL1LkyIOIO7HRk/lN++TZIUKHVT4Heb5moEXFHmCip7zZcTeZnma/CUWGJc8JXH+DizDCG+crzANQAxYMWsFbS3vDr6G+Z+435sRe/rGGsC/71/ZkMjDmj3QCeJZ1a4kK8qSIvXhpuUbsi0J0gXMN304ERBHuAKTJczTNaqYwgjk4Ut1JIDt2YX4rgQr+sEguwOUvUkP1BaASklZV0Adj3qgtgDUsdcpUGc9UNsAaqfkdzrtgdoCUKedYqoj5Lrzh+r4gqDqOLNOwepdDlu9KLB6w04lYPuy9ZxjgmzSVGfpFBHdmQaxhww9FzGed5r4MEvQr7/RS6L9Z2GW458wJv+gkjwFKakAyPjCRQz80Jp71p2HvwkgaT0NwWMEM97UOEJLcveYVrbG+O8Ca+kEKtcZAcst+sBxV68ENvw9+rXA/z+DBaDzQ73dzuI89AHuARdG5NcTHUe6LOgznUYGybgyCMi4wydUL71Bv78UZN2zIspBgKY9x3NESzgGS7Tx7uLHDP/HagRJSr44ylTIkODrCnUOyEIvEw4EtMTfizhP+FrizZipY8qKxywP80Ja+Xd80dVvUQPgSMNGqwAE7Mno6DrL8KZbIiDlA0h3jzSnFPrhIySIsnwMGSTZuttxsnxMj7VdAm0ltFW7ulE/0chXlTj9eA5z+GUFCCn4kQLSKrdA4Q8WaEEy9jsCjzC6A/5fC9LIPInQFvLu4yTGVC/7C+b+M/uUUjD+heV6Q8+9H03wbMMokson47E95aTMQOFAhFYflfiIgMEUtxyD1X+Sj0lICBqnjVKLT+SPgThKBJbRDJjm8HUzpdTpGqvgThmvYCbLIX/+Udr/3CEre5Zsf6Lw+NxLp4W/Kvfi5uPtxplpl9xrONIgNk9iH64waTFA7j3GwOpqawiCdzUi79Ete7EMg4ACFiIiQwgqBe0K4xCZ0ejOGt0bAFIDt1rsYdZ11oclGctLCG7YubW4Zt9MbMepoNs1e2wMJ9Y4JRxSy1zrZu1Obhyv2kjy9JShLaSCWozyAOh7XaAngkS6lnQB/PiNy//4odQGyBNXBy7VUNCYFAzdTknBRBdkv8PlKvq1KMGwxlpT4uvImRyG+gzTvRvvZJju6f6zh4g+Yymcip4GGdimsi4TUEuB2F4VkNaBuLpfgOjvIiS/cyqCpsswTo4meOKxRjBeFOA7EZLpABehT6T8PIzQdsIKBxKQXzH3KkBMHuXBZHRbEBkb/bMMs6U8qateUm1JUr127e2iqjM+qag6vHBRtWOeNnSb8rROxduRbk67J3SgJHUII7Nfi8FtE3VHU86X1pUeD5R0R0jStaU/VXEa9TvzZtKf6alY48i9bErQBVaPagj+ibDa0yD2FcsxxFpWJ8n8Qhg+qtEjShHWGVWQ72i67KyK1NMbLiqfQJfV0fgjEW0hV2LmFrNcE9k1lmVTKmZyS7ZVY/1Wv29SsgJBCgd/0t6fYboEcTL4dnXVvO53JMvS6v/XqJZe8s6au9atndH/8NqQH7T5FQzSRLHDM+/AbqP9EtJm323pBk+DjgfDInnMQxgT432kt4lldGrjFi4Fe7DGUjt2RMizIrhP1ATZu0CpAVg+6uDElupe3m9H3h+NG5im7ZPK+6NOYlt+NVPXcNpUgOg0JHGoW0Myh9KRNaMqbkmjNLLM2IcNVhFjF1nhI3HgBSwxKgozAyFHnITBJ8TLS08wNaiYLC7k122MWta7hn8XqJeI9CJTP+5dThGhXCUxpXrU0EHe+8lylWRh2Q0pDXgj2tyxOWYfTjN4lzlX1RUUfEBwoZ7stkR2h4qZZWo3NLOIwuOTXd2o/KsqVwfrTGah+3qoMFtHRPzxRig1ZvVKgN6mKVhLnzENpr6nseJxduyhcpRj69iUGugHHcVxNXpH23RIOEXUMKGhFdtURdsQ6OCqJXHyjGhUTAD4BNF28EMgqO6mEA6ieVQbd1TlBCmcPhJSqSZCKLtCv9UW1AIWSoIbDRdFyNgSEudhCozUHY9BCdzAC2dbkzv1BdA/RfBUiv6kc1Jqaqtoqok+mt/c3JjqaxM31dc/mtwbJqyPpW7Cj00m/M004ccmE/5WP+HHZZP6+kemCX8I44XqxlFW7ru24JjQ+SJcDUQLJp0oTp7qoP+6MSz3DtvLAJrGG6xZ3U1brFkLsQlaF7lPemmsHWls5m6XxoRiXJHGVP59vFM7fXRxVQFtoql2Gl3Mh1mJLs4xEU9WiJXLQksKAfaCc77PzGBaJDEVgtCsC6ysJlQOioglDkEtfMEq6roUH3yE0z5MpfBUXEj877dOkRXkGUZwEQYJl26YAEQLgM99bDbAKBpi4QvHCs+TZSLb9UjzsGZyRDQK44BoxXNLxCWw+FkfUEZEu6fa8FMY8wXB6jjhV68hUcFrFohHK1dNiEs6VzyBBcTyE/5isFwU2IJo/4cF3C5AJtikX6CVBWIgMEIfk7lZLCIZL3wai0m/kDbuYyTykSVbsymS7nNAwnyFfBjAjEiDsRRETlrLCHDxifBsgPB8fn1Fm6IfKf0uouSRTsTu4x5aYwHjYZ1qJvEA78QauR74wLb7YBF9Z36KAO8dKqHRvVtKa5M7m33FRRHb/jC/pSInlS6Yccjut9YJt5bXdGu1ZmIf6x64tyBdbBUlxl5DUWI8bAzmE53iHmoQuy9SQI0FG6UIwk6EEFEyaMS+sSEkFoJGhbfBV3z4CTUvJIWH268yl6IWc0JxsoQcXDEYUyhXZappLGSOhMkcasjfxxRh54KcTgor/ZSHs4LK4OXJxmJuzFEZG/g1GlBG4wop+7WoGYgKJaWAReWI9DGJeJePVJvOUAMBkHh8KcpRhV12CWggEayciUR5EjBZIKsMAvh5gUdHZC8eH6nFdZIJc5dsZaLl5OKQ7wD5g4pUESnNknpRSEFKFtE4zCvlDJNxNQx7knfcc5vjcpvzOVo01hWhX4O5ND0FO56eGXOZ6Fb4twCxfYwN46Zu8YndJcTGhkMCr+y4csHsv0ka5iwkxy/SjNoLmJ4b5ylcSKdvZe1e0auNSjXhiZQrqOeOy4B//IgZJdeJwwqXFr75MpZrThkHNR5ogswTiCKAWeJHyj2zcLmKpDAwwrtW0DeLQew0rlgXP4lfGO9MIVLU0/AxTK26w9RsoIDMINdbFwoVOw4RIViATC3F7BYz5jwkPPj9P798vLJ4cALl8hxWIj6B9i9cQxn5ZkFKexbaisKm6mtnwFInl5Vt7Yj0eGI3pcedhilNTOZ66lgrIjUIJwp5yX8UBYiQNILjg4zK60ukgyTCA46TUmArI2S2x1LZuqLnskryukwCQghj4eFDEyt7lgr1AQbhy/ZQIlTT8N0us8XGUaSPYcs28XNXvXtqwUAtyE3uuVx43pTy+EprEORO7tZ+23jN3gYZjuBTfk5EuEGAlLCjncYlN7nwc2jHpMpNXXKTTs+UTQwuuZpz0tuxVgbBOSLwEeSoY+CtFnjWNLJx2hbeTnvttoqOTRIhdqrdTgzaLcNbXVCoO7YzIC9Q2Z9YnGIv0E/jGRmmUpZh4kQJlpVoZks3OaKpsxdpfDhsi7mVQZ5S8+yqlN6q5u5NgdubpKjtguEgjP2oWEOqUdK8UuLLVQoDothzEfKpiKnbf7PQs2UAktW/USNEQSb1fNoc2LEigWXD2r3A1r7Aph4kcgSRl4OoTCeJ2nOgT3Wt7A9iw6ndRJJpypIDOFJuA4o0vQSH3fzUSgMYyR2tGUmpfpRi5ac+HphXHtCeQ/Ta1AohWNWiteGrICVRMO+BZGUKAxBY3OklUzuyDI+AJOijbjg0FL4cUnQzbpFkJ2FT4WRSHn7phcxorYhaGSF3SLJoG7lOCZP+7F9rKpYqqg27P4Qy/UUDE6ZNAxOm5xaY4OrHhmrT0vVK1nEwVxg+1spzZzqWp2vaX7fkq+r3Rit749qzz21z8KgrU+xSvwta2QXDs9sDBjZBHcsRi0gKmsVz9xvmJHa77nfMbHwxkt8Z3JrQWICcjbqUFqc6K7jlauc+EQ09cjdBbsc7P+y+4FsCzwDdHZ6Tbzu+d3pPlWO//bzV4+OCdjZqCFm2B7oD7QUfUT02zJqG/s46PaI604Xw9+zQJQn/xFMN4XKViptjymtaljAI2XETaqpVT5ay+2YkEy++MAeHWEaIb6f8QAJc4InW+L8+kZAeknzok8sCeehTWB5kowVxbxhuyzDsTNTz8E0jIFsTFxxbv/3ilyU2s8YMotML0vg4K9QG04DyjBTL856nIAjLw+csRh3/xM4meiwpgGn4QlzzEiVCtCmJSqNiAB+JswrpE4swBmnGk6uhZc5DYYxkJ9dLqocpy7qkYYSc5RBhnXALCuMEQqyMetWrafXDmF8YhkYmBamXEQXKWDmFxWMmK4kqimB2Ep9PRpLxYG97kBBk858T7Km3VxjDY+iLqHDQbORzQcBJy3xNIvCUpEtDHrtPn01hlp9dc5jl56UhoUxOjgxIa2t2mX6q94TyoVauMaP7wsf4y3PdWMTSXKZHUDoI63vgm4EfPlSuQVMLYNYw+wC7gGzzRNemkc6xdzT2y2ypZAO9sGMB+trQc3sGzmwIMlHyz7z1Z3vwybSJP9Vs4k/htXHP74YIpg4RWO8c6Ui+8lqPUS4M6FTeTwjTF4H1/I4MhsYVdCvFOyx+BTwggQQNhXmxFg76uIAviZRdhOa1yBCzyJ6QIJX2MldrMpeWJYDn39saPyPS87Ygdemhkw/GwDiduan3ZxIdIOVbkrLF6jGqSGNKeqtLzO5SIGiitFfZETZKHtk5iEooSYJp+4ci9iknwd9DTE8tfshKsNqS01Yo7RaRgDNtFh9HOQnRpoj44Ycrgayq7iRi+Bialue99S+xGBSISpCeieux8jSa0NiAlEZNqL0QGce+4EStZ2E6bXzBtN3pmTLHnl0UXDuCUacnTBynx7124Op0bNzW8+0QUyk1iEoSCc+UZ5nCaGukGGoJpR+g2suQ5ry7z/D9NTfMckCOguIQWZBGIl8eFQqYpvl3EdLU9BCnsfNDonCyPCzkij8W7++HGbu2HIsWKT11H0CI56aeZYjKJAGVUOgoWaSq9SVKtKPpfhqS5aDm3V4qOY1UYswoZhZLWjsd6fCLik7s6duDoJ0HhztUtmBVlTzuztSb3YzLP5PqRpk4prdbss8fK9k7m3OFqDqGW+htQ9EXYYOwZCfVKg2XMBVZS+ijpVgBbd3Mx4hdARc71FVUMVnhJBZkupKEklvKRSNvRkU7s1NHzlA1m4zOgRTqwsNFSYlHpXOHyueXSOf04CYXm4P+jWUv6dI6YXBaW/sYnOihMrgIqzSRVKXUTLaoVbwmLAEhcymkJNEgtSq9wJ9VCZBd2WypbqOES5Rk4JWUiPioLvgJqDtGzQlJbcpyyRMaBvMFppBdvREwmdhZojH3JPSk0uRZkNA++ncXKnuwtnyBVNbRnRNeJWPqWhzxraiyGUQKq/DI4yRwASNfL4QY4inwJLB3t1EeElV+VcTlAdcA69SSQl+hxNpdPpxiGojuAz01q3nilDtDEKHKU/RPGC/Ud5RSr7AVgXVG7pbDA8kTSktZCjlihGAhFiyugmaaEpyDtkVW7BmspYPCrFYYP4VxmL+lGznPjBi7tn2OxFiP2n/I6IUUPJty1fiDMQRvFemiCSK8RDBeFOC7CGBYpdistKw4AqX8kR8///v9v3/DeHIbwDK8AqOqXyOtlJfUFnGJaxQPS0+gJK2ESyIqsVmUN46BLPFDliYDCCSSxZY6rZKmDGBkRUZCkT2kEuf0VCAFljjfIVIYcftZSSsiRFSIwEgjPJg5kabq7HGwJYFIzT1WSkjdJR+b6iolTtySh4nGLfA2Ww9Ydjw7d8kFEZNKJj9p04xZblK8ptcZWVScSNCxV69kOccid+l+0UPhk5Z3L6+5wI4MtZNBHvqcwrxIDZfZ0Wu7bHLD1ztLjheTaVEnU4ZR1gg0PDkHp3yXCqJGkyWij3KTHt2VzcCNs08aLnezUU/VjaB3ncnH5IkcyC4Vci90wdEGo+zKtFbvbv/5fvcO8OLp8nyZP/qcEEnbCW8ZkbTJGhHJ2QGRzPczYmxQEEnruhaRnAtd8CaIdEYbX4Pc2gymhCW1InnS1UxcWbdCy+7Ptq9PnIe5s+x/Bqln5458fSGVXi6HXdiZrxZS0dXnsqvPhNdWiBbuHTV9jzGoIWHqENn2WN5U33GDSpo2QpAxFPZsXtuKSvPuFQfyhaxYlpo3ZMo3ZNrqhkzf9oZsMiH99nSWP8onVtvy9tHsdOKerdzRfVoWexrW/3Zulz7ImIRHdGRjkmrQNd0mYj7W0V7uDf0s7W2jAx2WEgQjrKD/SNI+o1tr2Vsm4+1b6LTZWxwe0HKpES6d+2sbn+HuNrun4057uLYD107zcDme3cO1Hbh2muFFDLSSjrdGpi5YSlbmjizTEJCs4D03byc/qzM8u2RsjtsHrCoMtxGqe92yZj0qg6uD2YoGX25VCJ0be5Vzi4YdhTG85juOKowTCzMq9p7UfmLgwO+FSoqQxhti/R3gm6NDrZx8S2IuQJxdZzAl9g9FC31fSVbxjhfX2QRYWJNCxaz5O2vqORYNyqJPZHOI9BiiRtleWamswCJYSOAWcSC8Gkc30OpSCxH2Ugxey7av5MbnlnwHOD2lLi7gfjUciRD3mFDI7n2TSU+jm9FoV9HaG5/7bpFGX/ix76PS6MY5Et1uj3C7prvQKTKviDWFol1JC3/Pkg84g0ukk0eclkimVITEWKM7QmTcd0+Y4PyktAVclUeS0Ksf1uheI4hq/UdaBbXwboGb+nFFauGyMhORoEMrS7ljqUKYHlwLIcLMo1TTSF63UEj2Xp1U3QcyYQUaHSYfLWqpaN0tXDtDCK+ZGOruS7XevFTrzUv1w1y245y3fCWN9ueGof7cMM6fagHfbe0N9cfmhf1xBgsr37xrkNuMrgSt3Y800AGQSPX5xkkrdEPAwEg9DIShuYyy6bbgty/QHBzbehRxRr2czSTOGANa27vS3PEu3IR8VHmmsXnJ69Yc7OlnbvbmlptYpIFWyITiPdXjtDuFZPvVZo1PyklZKmM7UTS5DClxCZV15lzkIVR2B1VuE5ncshr17OSYvXxMk1UIA3wLoOEW1uP2aOCAiPzl12EcEOTCtodrZ4pNF3W7qq3FOGBojkjmiGkJlkuBr7QULlmWbCx0pMmSDFc0Y1PLjVTBMS5AHWRot41WZefJyiYiRFMpT8XvY4b+lQ+EBWqyyfxkqrrR/GReP9UUtVmU2nPOG8f1wriIySxmWhXHXb3q47wlR5IQlQesGyHdDSTxjvzyJCOU2UBFP0O/3JstW6FzvNk6wl9ss24LIbqIzfwBFviKbGkjl7qJ+fEYm7TXL1rRL2bunvpFi4dWXV1U7S8mbX0nOGcYq6SHuz18xylK+n1wOif3OewDPTRC1mn6vdDWXpgOz24veBfuTOs6HsprnMfV69YBN3R6uLYCV4rT3Rki9YglHOcGUrAtzq0n8+2QeTSRs4tr83SWf1Hk4KioPW5MsrtNqe6Zrobd08dwD59uqI3h/dbQL2KMMV7iJN2lUxraMhyOgQhxJt2JWNu+Z1VcDro7VrHRkURmX+hBnFUKM5wG3OKBaFJl7OSeWbfDsgnZVrYx8kBeml0C6ejBbZxgHAGI5/3OlNgUbVzuAd6VdYM5azmDNy+ePEjJMtrM0Lizo6FnOS2xnL3D9Fq0Ow1NYbm/KM/hS99AnHS7VRNMwQj7xulBoMQUUxIvIm4Wg5/VCJufItKuPkyHhN6sr8pYnLUa1OcZu1KCeQCL3allETtP90EEB86bsh5KsNX1Kac+uqsszI4OXbnMvTEtatnz6K5cygMCurwbExTUbsChsxkq66YzsIOaHymz0BntQYvEja7U5SO2KND2p9q32A6vAk+k21q3tcQxotLG3rLIpt566eGypAf1ykWT9HDqGxc9PWC891q1vhPO0GvF92LvtTrhPhDJls9oHzS4+B5DbFW7AH4Sx9DPyekyUm7vujCuQiivDctidO+LwqOvi74qv4MVy8WMqWWBRFUiaPzBky5Xs7V/VvOb7JRHZ1yb30eBDA62qeKftuUxxNAAo1v2YhkGAVEBTYhcRfVaXK5g62bE3kkr3IJem3awvrm2bZ7WQs9NZ7JUBT0ObtOUrC1bJwmENUuma9wNVOm9l2xkWDFeduCtD5Mqto8UOFC1X7vXQWtGVKxpp+X7IXQP7z8Rxi1SwEyW9DodbMdcUZ2kTiAvIrUkCnnJHF/OiFu7jR4RbuAg8DnqgF4dgR4+ggjne5dPzpWV9ea+gGgBSCj5byCKQEp+PgSLMrntlgbeU3q2Imnxb+MMRiSl0++gSEM0Dlz4iufdqLHbR5CSy7KrrYqZ/ivJCmIunzWdXhi94AsCxOp/RbPEOtxv+G7wINnYDCqUIbGV0FaFFE7tJPmEFSmRdG2Q4x1Eqxra0gL5NSP7WOfsrkkFclqjzsZcFDumNajjz7sJA70mvkXuHvNntiZOe9tUkUDd7s/jD3vfcrkWjX3Lw259y5PJRcGo63Cg5nCddBsONNRl+j/EXRt91E+LJhM1uPMMon6GPZLvgORu85C/bkM5R6azxxcE56MS5mlToI26JcyjTm6Fv1Rc3AWuw24Zrh6kVzJci0XesmC613CJrQgsnq7PLtkqP56d38GbUR8RpZDjRgjudku4XQPQ9gwR2hx7i9eW3o1F/gmth3fW7dyaOk1piT344/ffrviH1B6bU8Nkugxj+swDWXMCp7BpqJKcRmqX4Ur9ibCQHYNyLi19Z/1SbQiq9gsQ/V2E5L7inRazN851peFN7YYcRRS2QJ0u/PzeUVlKYwVu1LECd8RkmDSEdFtIrUSpEYvg5IRkvGO5mnDFK1atzITH42xfr44bK1sforo1zveoM6lJldHOBD0VVIaQZIvdAHjYLFU2e6JJf0hyIB0ywg7mNGTcC+eQlkUecp8TfMWXlAfkVkwWs/K9iPOE36ejzkMVZtZC1sEXroMIZjXbtOeJ7fBETz14YuKJ5oSK7YWOctVCIq/36v7rN8SJhCRTLPGp1W7dkc4iSHt/SHuUQZwsO5+NMJ5dlGx8RBvsduGZh7808HCOG2+GE8nTfMdcAFzd48J1Lz1pB1B3G6QwvRz/5WXBddqt/jvRBTRDQBoT7Nm96NT+VZX/e97dEu8+w6Rlk7fpO2mA1c1Dj4bnxpgn9SGsOxgXGtj/3Zo4V2yRMNMUKdL9QNvHAcPb2c9R19AAONQsdFP+JTdYxFeWkv2DJmiha4DdDmtiSYERXEJmeaGJTViLOx0HqhueNqqWzVFHAEl3IxgAazL/3ABuGNXTcElcRhx+FjMdAmYdQ/Xz5EhQJA1/3pTJ/+LRSFv1SF70F+ATAeQe7HGdwVnt515yaklyUi+YOQd76ER3Nyl8sd8OJxKkz8AINr3g6NESLkfSmBtHGU66vc16sinKEAr9uNeWu0DyM3R5TExnsg5OHblL3Ncgc3R1JIu5y3qQG17n8cbrInceeRbWiWmyjJY58tRI2zTQipcZ9KosNtQpy07ibS/hsvdaM1WvCsTHqMxkid3z1DsfLehZbiPQ2w8O2W8TNo2V3DsL1gErH+44F9LV3gOtG+L+M6+fWsMoxwTxg85icW5XkcncXJu9VtfAyfcQTYglit35Kjh9H5W0p5bkMEpT3lwlCgfHpGP7p4UjbbUdbtRQH+6V4W4FI/U2pObKcHu3rU5dTTJ6iPMUBDxyrQa9cfIPBdV2wta1ma4o8oIeGV+WfCGsiydzsiqRgRGR+oX4v4EtCWTfwp9kokF4Va2oQBCSx7zPPyTmr9j7e36ROkZ2kOGP/QSvfxpiZrAzKr5V/JNIzDFQcajG6c1M+U1OnCB62iCj269iiZh6TS0RlIB1F5Oh+2Fvo0WShvkyKaWoDc58q7dOnJIJD9WUno1PrbRogrzgjDEk0AcxrLUU6YMfv7FxkIcy1oc88WCfrgOEpo1DCSiWH0BkWFUlE9710BvNbsbDiT2aTl2Pn4ctd+YNe+HOho4zqTbfcpo8Zza8qE3YzcaYdct9ZtOLgtHlIPxs0q1UobsohVTRCwftCQdn6J+cXU6ilGOT4ZnbGF0P5c8Hwkg3ouymBPQ+yo4R/Qy0gJmuSX5MEx8G4TJkoWx4D2Ez1Xv5UqCrjUmKyxJyMvoLNl1Jlrsrbn/id/XU9VG9vKaRgc41dZiLn7k1mb/fuX/z60bj8UzjIY3VGC3zZdmv+K7mo0PmQtu1NtlP82X5xbLa3y5LMDQtwasGEnuQ1EHtlXfOjbi4gBzRBhj/fGImjklb+0NWOhWeK1dgaS+bTXzUzsQPnXNjM3GjSY4P2eCLFjb4cac3aQd/V9L0CGBLVFu1NuE9WPtb5efHNu2rIacm0/6JLyVxZro+V/Gy3W/LTYURBC2ig4G4yfFVSWd1Wl+VGJ/0syrAkBEbmZ6LSctVTSPieiPbEVe3SENMrd3ynVBxSfRT5cSmhiQCojRFRl3fWMlfKvVoThrOVlgb7BZaz9jaYKDVMWSGEYzS8KbsYdikB1bxamODddP+KZpZb25g45xJUxvq02KeCGfb/Da3VsmpI1Hzrcl3aJdOT82Pq52pgRKNSXiLgRKzy0mWcHQ7zKSxHabbg9QzPftbYztMYGLBvf2lJQzfO3fgHvYX9JgmOO6tdI8hYD3/nuC7hryH/wE=