YES Problem: b(a(x)) -> c(c(x)) c(c(x)) -> a(b(x)) c(a(x)) -> c(c(x)) b(c(x)) -> a(b(x)) a(c(x)) -> a(b(x)) c(b(x)) -> a(c(x)) b(c(x)) -> b(b(x)) b(b(x)) -> b(a(x)) a(c(x)) -> c(a(x)) Proof: Church Rosser Transformation Processor (no redundant rules): strict: weak: critical peaks: 31 c(a(x)) <-0|[]- a(c(x)) -4|[]-> a(b(x)) c(c(a(x164))) <-0|0[]- c(a(c(x164))) -6|[]-> c(c(c(x164))) b(c(a(x165))) <-0|0[]- b(a(c(x165))) -8|[]-> c(c(c(x165))) b(b(a(x166))) <-1|0[]- b(b(b(x166))) -1|[]-> b(a(b(x166))) c(b(a(x167))) <-1|0[]- c(b(b(x167))) -3|[]-> a(c(b(x167))) b(b(b(x168))) <-2|0[]- b(b(c(x168))) -1|[]-> b(a(c(x168))) c(b(b(x169))) <-2|0[]- c(b(c(x169))) -3|[]-> a(c(c(x169))) b(b(x)) <-2|[]- b(c(x)) -5|[]-> a(b(x)) a(a(c(x171))) <-3|0[]- a(c(b(x171))) -0|[]-> c(a(b(x171))) b(a(c(x172))) <-3|0[]- b(c(b(x172))) -2|[]-> b(b(b(x172))) a(a(c(x173))) <-3|0[]- a(c(b(x173))) -4|[]-> a(b(b(x173))) b(a(c(x174))) <-3|0[]- b(c(b(x174))) -5|[]-> a(b(b(x174))) c(a(c(x175))) <-3|0[]- c(c(b(x175))) -7|[]-> a(b(b(x175))) a(b(x)) <-4|[]- a(c(x)) -0|[]-> c(a(x)) c(a(b(x177))) <-4|0[]- c(a(c(x177))) -6|[]-> c(c(c(x177))) b(a(b(x178))) <-4|0[]- b(a(c(x178))) -8|[]-> c(c(c(x178))) b(a(b(x179))) <-5|0[]- b(b(c(x179))) -1|[]-> b(a(c(x179))) a(b(x)) <-5|[]- b(c(x)) -2|[]-> b(b(x)) c(a(b(x181))) <-5|0[]- c(b(c(x181))) -3|[]-> a(c(c(x181))) a(c(c(x182))) <-6|0[]- a(c(a(x182))) -0|[]-> c(a(a(x182))) b(c(c(x183))) <-6|0[]- b(c(a(x183))) -2|[]-> b(b(a(x183))) a(c(c(x184))) <-6|0[]- a(c(a(x184))) -4|[]-> a(b(a(x184))) b(c(c(x185))) <-6|0[]- b(c(a(x185))) -5|[]-> a(b(a(x185))) c(c(c(x186))) <-6|0[]- c(c(a(x186))) -7|[]-> a(b(a(x186))) a(a(b(x187))) <-7|0[]- a(c(c(x187))) -0|[]-> c(a(c(x187))) b(a(b(x188))) <-7|0[]- b(c(c(x188))) -2|[]-> b(b(c(x188))) a(a(b(x189))) <-7|0[]- a(c(c(x189))) -4|[]-> a(b(c(x189))) b(a(b(x190))) <-7|0[]- b(c(c(x190))) -5|[]-> a(b(c(x190))) c(a(b(x191))) <-7|0[]- c(c(c(x191))) -7|[]-> a(b(c(x191))) b(c(c(x192))) <-8|0[]- b(b(a(x192))) -1|[]-> b(a(a(x192))) c(c(c(x193))) <-8|0[]- c(b(a(x193))) -3|[]-> a(c(a(x193))) Redundant Rules Transformation: a(c(x)) -> c(a(x)) b(b(x)) -> b(a(x)) b(c(x)) -> b(b(x)) c(b(x)) -> a(c(x)) a(c(x)) -> a(b(x)) b(c(x)) -> a(b(x)) c(a(x)) -> c(c(x)) c(c(x)) -> a(b(x)) b(a(x)) -> c(c(x)) a(c(x)) -> c(c(x)) b(b(x)) -> c(c(x)) b(c(x)) -> b(a(x)) c(b(x)) -> c(a(x)) c(b(x)) -> a(b(x)) c(a(x)) -> a(b(x)) b(a(x)) -> a(b(x)) Church Rosser Transformation Processor (no redundant rules): strict: weak: critical peaks: 113 c(a(b(x706))) <-0|0[]- c(b(a(x706))) -2|[]-> a(b(a(x706))) c(a(b(x707))) <-0|0[]- c(b(a(x707))) -3|[]-> c(a(a(x707))) b(a(b(x708))) <-0|0[]- b(b(a(x708))) -5|[]-> c(c(a(x708))) a(b(x)) <-0|[]- b(a(x)) -7|[]-> c(c(x)) c(a(b(x710))) <-0|0[]- c(b(a(x710))) -12|[]-> a(c(a(x710))) b(a(b(x711))) <-0|0[]- b(b(a(x711))) -14|[]-> b(a(a(x711))) b(a(b(x712))) <-1|0[]- b(c(a(x712))) -4|[]-> b(a(a(x712))) a(a(b(x713))) <-1|0[]- a(c(a(x713))) -6|[]-> c(c(a(x713))) c(a(b(x714))) <-1|0[]- c(c(a(x714))) -8|[]-> a(b(a(x714))) a(b(x)) <-1|[]- c(a(x)) -9|[]-> c(c(x)) b(a(b(x716))) <-1|0[]- b(c(a(x716))) -10|[]-> a(b(a(x716))) a(a(b(x717))) <-1|0[]- a(c(a(x717))) -11|[]-> a(b(a(x717))) b(a(b(x718))) <-1|0[]- b(c(a(x718))) -13|[]-> b(b(a(x718))) a(a(b(x719))) <-1|0[]- a(c(a(x719))) -15|[]-> c(a(a(x719))) a(b(x)) <-2|[]- c(b(x)) -3|[]-> c(a(x)) b(a(b(x721))) <-2|0[]- b(c(b(x721))) -4|[]-> b(a(b(x721))) a(a(b(x722))) <-2|0[]- a(c(b(x722))) -6|[]-> c(c(b(x722))) c(a(b(x723))) <-2|0[]- c(c(b(x723))) -8|[]-> a(b(b(x723))) b(a(b(x724))) <-2|0[]- b(c(b(x724))) -10|[]-> a(b(b(x724))) a(a(b(x725))) <-2|0[]- a(c(b(x725))) -11|[]-> a(b(b(x725))) a(b(x)) <-2|[]- c(b(x)) -12|[]-> a(c(x)) b(a(b(x727))) <-2|0[]- b(c(b(x727))) -13|[]-> b(b(b(x727))) a(a(b(x728))) <-2|0[]- a(c(b(x728))) -15|[]-> c(a(b(x728))) c(a(x)) <-3|[]- c(b(x)) -2|[]-> a(b(x)) b(c(a(x730))) <-3|0[]- b(c(b(x730))) -4|[]-> b(a(b(x730))) a(c(a(x731))) <-3|0[]- a(c(b(x731))) -6|[]-> c(c(b(x731))) c(c(a(x732))) <-3|0[]- c(c(b(x732))) -8|[]-> a(b(b(x732))) b(c(a(x733))) <-3|0[]- b(c(b(x733))) -10|[]-> a(b(b(x733))) a(c(a(x734))) <-3|0[]- a(c(b(x734))) -11|[]-> a(b(b(x734))) c(a(x)) <-3|[]- c(b(x)) -12|[]-> a(c(x)) b(c(a(x736))) <-3|0[]- b(c(b(x736))) -13|[]-> b(b(b(x736))) a(c(a(x737))) <-3|0[]- a(c(b(x737))) -15|[]-> c(a(b(x737))) c(b(a(x738))) <-4|0[]- c(b(c(x738))) -2|[]-> a(b(c(x738))) c(b(a(x739))) <-4|0[]- c(b(c(x739))) -3|[]-> c(a(c(x739))) b(b(a(x740))) <-4|0[]- b(b(c(x740))) -5|[]-> c(c(c(x740))) b(a(x)) <-4|[]- b(c(x)) -10|[]-> a(b(x)) c(b(a(x742))) <-4|0[]- c(b(c(x742))) -12|[]-> a(c(c(x742))) b(a(x)) <-4|[]- b(c(x)) -13|[]-> b(b(x)) b(b(a(x744))) <-4|0[]- b(b(c(x744))) -14|[]-> b(a(c(x744))) c(c(c(x745))) <-5|0[]- c(b(b(x745))) -2|[]-> a(b(b(x745))) c(c(c(x746))) <-5|0[]- c(b(b(x746))) -3|[]-> c(a(b(x746))) b(c(c(x747))) <-5|0[]- b(b(b(x747))) -5|[]-> c(c(b(x747))) c(c(c(x748))) <-5|0[]- c(b(b(x748))) -12|[]-> a(c(b(x748))) c(c(x)) <-5|[]- b(b(x)) -14|[]-> b(a(x)) b(c(c(x750))) <-5|0[]- b(b(b(x750))) -14|[]-> b(a(b(x750))) b(c(c(x751))) <-6|0[]- b(a(c(x751))) -0|[]-> a(b(c(x751))) c(c(c(x752))) <-6|0[]- c(a(c(x752))) -1|[]-> a(b(c(x752))) b(c(c(x753))) <-6|0[]- b(a(c(x753))) -7|[]-> c(c(c(x753))) c(c(c(x754))) <-6|0[]- c(a(c(x754))) -9|[]-> c(c(c(x754))) c(c(x)) <-6|[]- a(c(x)) -11|[]-> a(b(x)) c(c(x)) <-6|[]- a(c(x)) -15|[]-> c(a(x)) c(c(x)) <-7|[]- b(a(x)) -0|[]-> a(b(x)) c(c(c(x758))) <-7|0[]- c(b(a(x758))) -2|[]-> a(b(a(x758))) c(c(c(x759))) <-7|0[]- c(b(a(x759))) -3|[]-> c(a(a(x759))) b(c(c(x760))) <-7|0[]- b(b(a(x760))) -5|[]-> c(c(a(x760))) c(c(c(x761))) <-7|0[]- c(b(a(x761))) -12|[]-> a(c(a(x761))) b(c(c(x762))) <-7|0[]- b(b(a(x762))) -14|[]-> b(a(a(x762))) b(a(b(x763))) <-8|0[]- b(c(c(x763))) -4|[]-> b(a(c(x763))) a(a(b(x764))) <-8|0[]- a(c(c(x764))) -6|[]-> c(c(c(x764))) c(a(b(x765))) <-8|0[]- c(c(c(x765))) -8|[]-> a(b(c(x765))) b(a(b(x766))) <-8|0[]- b(c(c(x766))) -10|[]-> a(b(c(x766))) a(a(b(x767))) <-8|0[]- a(c(c(x767))) -11|[]-> a(b(c(x767))) b(a(b(x768))) <-8|0[]- b(c(c(x768))) -13|[]-> b(b(c(x768))) a(a(b(x769))) <-8|0[]- a(c(c(x769))) -15|[]-> c(a(c(x769))) c(c(x)) <-9|[]- c(a(x)) -1|[]-> a(b(x)) b(c(c(x771))) <-9|0[]- b(c(a(x771))) -4|[]-> b(a(a(x771))) a(c(c(x772))) <-9|0[]- a(c(a(x772))) -6|[]-> c(c(a(x772))) c(c(c(x773))) <-9|0[]- c(c(a(x773))) -8|[]-> a(b(a(x773))) b(c(c(x774))) <-9|0[]- b(c(a(x774))) -10|[]-> a(b(a(x774))) a(c(c(x775))) <-9|0[]- a(c(a(x775))) -11|[]-> a(b(a(x775))) b(c(c(x776))) <-9|0[]- b(c(a(x776))) -13|[]-> b(b(a(x776))) a(c(c(x777))) <-9|0[]- a(c(a(x777))) -15|[]-> c(a(a(x777))) c(a(b(x778))) <-10|0[]- c(b(c(x778))) -2|[]-> a(b(c(x778))) c(a(b(x779))) <-10|0[]- c(b(c(x779))) -3|[]-> c(a(c(x779))) a(b(x)) <-10|[]- b(c(x)) -4|[]-> b(a(x)) b(a(b(x781))) <-10|0[]- b(b(c(x781))) -5|[]-> c(c(c(x781))) c(a(b(x782))) <-10|0[]- c(b(c(x782))) -12|[]-> a(c(c(x782))) a(b(x)) <-10|[]- b(c(x)) -13|[]-> b(b(x)) b(a(b(x784))) <-10|0[]- b(b(c(x784))) -14|[]-> b(a(c(x784))) b(a(b(x785))) <-11|0[]- b(a(c(x785))) -0|[]-> a(b(c(x785))) c(a(b(x786))) <-11|0[]- c(a(c(x786))) -1|[]-> a(b(c(x786))) a(b(x)) <-11|[]- a(c(x)) -6|[]-> c(c(x)) b(a(b(x788))) <-11|0[]- b(a(c(x788))) -7|[]-> c(c(c(x788))) c(a(b(x789))) <-11|0[]- c(a(c(x789))) -9|[]-> c(c(c(x789))) a(b(x)) <-11|[]- a(c(x)) -15|[]-> c(a(x)) a(c(x)) <-12|[]- c(b(x)) -2|[]-> a(b(x)) a(c(x)) <-12|[]- c(b(x)) -3|[]-> c(a(x)) b(a(c(x793))) <-12|0[]- b(c(b(x793))) -4|[]-> b(a(b(x793))) a(a(c(x794))) <-12|0[]- a(c(b(x794))) -6|[]-> c(c(b(x794))) c(a(c(x795))) <-12|0[]- c(c(b(x795))) -8|[]-> a(b(b(x795))) b(a(c(x796))) <-12|0[]- b(c(b(x796))) -10|[]-> a(b(b(x796))) a(a(c(x797))) <-12|0[]- a(c(b(x797))) -11|[]-> a(b(b(x797))) b(a(c(x798))) <-12|0[]- b(c(b(x798))) -13|[]-> b(b(b(x798))) a(a(c(x799))) <-12|0[]- a(c(b(x799))) -15|[]-> c(a(b(x799))) c(b(b(x800))) <-13|0[]- c(b(c(x800))) -2|[]-> a(b(c(x800))) c(b(b(x801))) <-13|0[]- c(b(c(x801))) -3|[]-> c(a(c(x801))) b(b(x)) <-13|[]- b(c(x)) -4|[]-> b(a(x)) b(b(b(x803))) <-13|0[]- b(b(c(x803))) -5|[]-> c(c(c(x803))) b(b(x)) <-13|[]- b(c(x)) -10|[]-> a(b(x)) c(b(b(x805))) <-13|0[]- c(b(c(x805))) -12|[]-> a(c(c(x805))) b(b(b(x806))) <-13|0[]- b(b(c(x806))) -14|[]-> b(a(c(x806))) c(b(a(x807))) <-14|0[]- c(b(b(x807))) -2|[]-> a(b(b(x807))) c(b(a(x808))) <-14|0[]- c(b(b(x808))) -3|[]-> c(a(b(x808))) b(a(x)) <-14|[]- b(b(x)) -5|[]-> c(c(x)) b(b(a(x810))) <-14|0[]- b(b(b(x810))) -5|[]-> c(c(b(x810))) c(b(a(x811))) <-14|0[]- c(b(b(x811))) -12|[]-> a(c(b(x811))) b(b(a(x812))) <-14|0[]- b(b(b(x812))) -14|[]-> b(a(b(x812))) b(c(a(x813))) <-15|0[]- b(a(c(x813))) -0|[]-> a(b(c(x813))) c(c(a(x814))) <-15|0[]- c(a(c(x814))) -1|[]-> a(b(c(x814))) c(a(x)) <-15|[]- a(c(x)) -6|[]-> c(c(x)) b(c(a(x816))) <-15|0[]- b(a(c(x816))) -7|[]-> c(c(c(x816))) c(c(a(x817))) <-15|0[]- c(a(c(x817))) -9|[]-> c(c(c(x817))) c(a(x)) <-15|[]- a(c(x)) -11|[]-> a(b(x)) Redundant Rules Transformation: b(a(x)) -> a(b(x)) c(a(x)) -> a(b(x)) c(b(x)) -> a(b(x)) c(b(x)) -> c(a(x)) b(c(x)) -> b(a(x)) b(b(x)) -> c(c(x)) a(c(x)) -> c(c(x)) b(a(x)) -> c(c(x)) c(c(x)) -> a(b(x)) c(a(x)) -> c(c(x)) b(c(x)) -> a(b(x)) a(c(x)) -> a(b(x)) c(b(x)) -> a(c(x)) b(c(x)) -> b(b(x)) b(b(x)) -> b(a(x)) a(c(x)) -> c(a(x)) c(b(x)) -> c(c(x)) b(c(x)) -> c(c(x)) b(b(x)) -> a(b(x)) Church Rosser Transformation Processor (dup): strict: weak: b(a(x)) -> a(b(x)) c(a(x)) -> a(b(x)) c(b(x)) -> a(b(x)) c(b(x)) -> c(a(x)) b(c(x)) -> b(a(x)) b(b(x)) -> c(c(x)) a(c(x)) -> c(c(x)) b(a(x)) -> c(c(x)) c(c(x)) -> a(b(x)) c(a(x)) -> c(c(x)) b(c(x)) -> a(b(x)) a(c(x)) -> a(b(x)) c(b(x)) -> a(c(x)) b(c(x)) -> b(b(x)) b(b(x)) -> b(a(x)) a(c(x)) -> c(a(x)) c(b(x)) -> c(c(x)) b(c(x)) -> c(c(x)) b(b(x)) -> a(b(x)) critical peaks: 171 c(a(b(x1541))) <-0|0[]- c(b(a(x1541))) -2|[]-> a(b(a(x1541))) c(a(b(x1542))) <-0|0[]- c(b(a(x1542))) -3|[]-> c(a(a(x1542))) b(a(b(x1543))) <-0|0[]- b(b(a(x1543))) -5|[]-> c(c(a(x1543))) a(b(x)) <-0|[]- b(a(x)) -7|[]-> c(c(x)) c(a(b(x1545))) <-0|0[]- c(b(a(x1545))) -12|[]-> a(c(a(x1545))) b(a(b(x1546))) <-0|0[]- b(b(a(x1546))) -14|[]-> b(a(a(x1546))) c(a(b(x1547))) <-0|0[]- c(b(a(x1547))) -16|[]-> c(c(a(x1547))) b(a(b(x1548))) <-0|0[]- b(b(a(x1548))) -18|[]-> a(b(a(x1548))) b(a(b(x1549))) <-1|0[]- b(c(a(x1549))) -4|[]-> b(a(a(x1549))) a(a(b(x1550))) <-1|0[]- a(c(a(x1550))) -6|[]-> c(c(a(x1550))) c(a(b(x1551))) <-1|0[]- c(c(a(x1551))) -8|[]-> a(b(a(x1551))) a(b(x)) <-1|[]- c(a(x)) -9|[]-> c(c(x)) b(a(b(x1553))) <-1|0[]- b(c(a(x1553))) -10|[]-> a(b(a(x1553))) a(a(b(x1554))) <-1|0[]- a(c(a(x1554))) -11|[]-> a(b(a(x1554))) b(a(b(x1555))) <-1|0[]- b(c(a(x1555))) -13|[]-> b(b(a(x1555))) a(a(b(x1556))) <-1|0[]- a(c(a(x1556))) -15|[]-> c(a(a(x1556))) b(a(b(x1557))) <-1|0[]- b(c(a(x1557))) -17|[]-> c(c(a(x1557))) a(b(x)) <-2|[]- c(b(x)) -3|[]-> c(a(x)) b(a(b(x1559))) <-2|0[]- b(c(b(x1559))) -4|[]-> b(a(b(x1559))) a(a(b(x1560))) <-2|0[]- a(c(b(x1560))) -6|[]-> c(c(b(x1560))) c(a(b(x1561))) <-2|0[]- c(c(b(x1561))) -8|[]-> a(b(b(x1561))) b(a(b(x1562))) <-2|0[]- b(c(b(x1562))) -10|[]-> a(b(b(x1562))) a(a(b(x1563))) <-2|0[]- a(c(b(x1563))) -11|[]-> a(b(b(x1563))) a(b(x)) <-2|[]- c(b(x)) -12|[]-> a(c(x)) b(a(b(x1565))) <-2|0[]- b(c(b(x1565))) -13|[]-> b(b(b(x1565))) a(a(b(x1566))) <-2|0[]- a(c(b(x1566))) -15|[]-> c(a(b(x1566))) a(b(x)) <-2|[]- c(b(x)) -16|[]-> c(c(x)) b(a(b(x1568))) <-2|0[]- b(c(b(x1568))) -17|[]-> c(c(b(x1568))) c(a(x)) <-3|[]- c(b(x)) -2|[]-> a(b(x)) b(c(a(x1570))) <-3|0[]- b(c(b(x1570))) -4|[]-> b(a(b(x1570))) a(c(a(x1571))) <-3|0[]- a(c(b(x1571))) -6|[]-> c(c(b(x1571))) c(c(a(x1572))) <-3|0[]- c(c(b(x1572))) -8|[]-> a(b(b(x1572))) b(c(a(x1573))) <-3|0[]- b(c(b(x1573))) -10|[]-> a(b(b(x1573))) a(c(a(x1574))) <-3|0[]- a(c(b(x1574))) -11|[]-> a(b(b(x1574))) c(a(x)) <-3|[]- c(b(x)) -12|[]-> a(c(x)) b(c(a(x1576))) <-3|0[]- b(c(b(x1576))) -13|[]-> b(b(b(x1576))) a(c(a(x1577))) <-3|0[]- a(c(b(x1577))) -15|[]-> c(a(b(x1577))) c(a(x)) <-3|[]- c(b(x)) -16|[]-> c(c(x)) b(c(a(x1579))) <-3|0[]- b(c(b(x1579))) -17|[]-> c(c(b(x1579))) c(b(a(x1580))) <-4|0[]- c(b(c(x1580))) -2|[]-> a(b(c(x1580))) c(b(a(x1581))) <-4|0[]- c(b(c(x1581))) -3|[]-> c(a(c(x1581))) b(b(a(x1582))) <-4|0[]- b(b(c(x1582))) -5|[]-> c(c(c(x1582))) b(a(x)) <-4|[]- b(c(x)) -10|[]-> a(b(x)) c(b(a(x1584))) <-4|0[]- c(b(c(x1584))) -12|[]-> a(c(c(x1584))) b(a(x)) <-4|[]- b(c(x)) -13|[]-> b(b(x)) b(b(a(x1586))) <-4|0[]- b(b(c(x1586))) -14|[]-> b(a(c(x1586))) c(b(a(x1587))) <-4|0[]- c(b(c(x1587))) -16|[]-> c(c(c(x1587))) b(a(x)) <-4|[]- b(c(x)) -17|[]-> c(c(x)) b(b(a(x1589))) <-4|0[]- b(b(c(x1589))) -18|[]-> a(b(c(x1589))) c(c(c(x1590))) <-5|0[]- c(b(b(x1590))) -2|[]-> a(b(b(x1590))) c(c(c(x1591))) <-5|0[]- c(b(b(x1591))) -3|[]-> c(a(b(x1591))) b(c(c(x1592))) <-5|0[]- b(b(b(x1592))) -5|[]-> c(c(b(x1592))) c(c(c(x1593))) <-5|0[]- c(b(b(x1593))) -12|[]-> a(c(b(x1593))) c(c(x)) <-5|[]- b(b(x)) -14|[]-> b(a(x)) b(c(c(x1595))) <-5|0[]- b(b(b(x1595))) -14|[]-> b(a(b(x1595))) c(c(c(x1596))) <-5|0[]- c(b(b(x1596))) -16|[]-> c(c(b(x1596))) c(c(x)) <-5|[]- b(b(x)) -18|[]-> a(b(x)) b(c(c(x1598))) <-5|0[]- b(b(b(x1598))) -18|[]-> a(b(b(x1598))) b(c(c(x1599))) <-6|0[]- b(a(c(x1599))) -0|[]-> a(b(c(x1599))) c(c(c(x1600))) <-6|0[]- c(a(c(x1600))) -1|[]-> a(b(c(x1600))) b(c(c(x1601))) <-6|0[]- b(a(c(x1601))) -7|[]-> c(c(c(x1601))) c(c(c(x1602))) <-6|0[]- c(a(c(x1602))) -9|[]-> c(c(c(x1602))) c(c(x)) <-6|[]- a(c(x)) -11|[]-> a(b(x)) c(c(x)) <-6|[]- a(c(x)) -15|[]-> c(a(x)) c(c(x)) <-7|[]- b(a(x)) -0|[]-> a(b(x)) c(c(c(x1606))) <-7|0[]- c(b(a(x1606))) -2|[]-> a(b(a(x1606))) c(c(c(x1607))) <-7|0[]- c(b(a(x1607))) -3|[]-> c(a(a(x1607))) b(c(c(x1608))) <-7|0[]- b(b(a(x1608))) -5|[]-> c(c(a(x1608))) c(c(c(x1609))) <-7|0[]- c(b(a(x1609))) -12|[]-> a(c(a(x1609))) b(c(c(x1610))) <-7|0[]- b(b(a(x1610))) -14|[]-> b(a(a(x1610))) c(c(c(x1611))) <-7|0[]- c(b(a(x1611))) -16|[]-> c(c(a(x1611))) b(c(c(x1612))) <-7|0[]- b(b(a(x1612))) -18|[]-> a(b(a(x1612))) b(a(b(x1613))) <-8|0[]- b(c(c(x1613))) -4|[]-> b(a(c(x1613))) a(a(b(x1614))) <-8|0[]- a(c(c(x1614))) -6|[]-> c(c(c(x1614))) c(a(b(x1615))) <-8|0[]- c(c(c(x1615))) -8|[]-> a(b(c(x1615))) b(a(b(x1616))) <-8|0[]- b(c(c(x1616))) -10|[]-> a(b(c(x1616))) a(a(b(x1617))) <-8|0[]- a(c(c(x1617))) -11|[]-> a(b(c(x1617))) b(a(b(x1618))) <-8|0[]- b(c(c(x1618))) -13|[]-> b(b(c(x1618))) a(a(b(x1619))) <-8|0[]- a(c(c(x1619))) -15|[]-> c(a(c(x1619))) b(a(b(x1620))) <-8|0[]- b(c(c(x1620))) -17|[]-> c(c(c(x1620))) c(c(x)) <-9|[]- c(a(x)) -1|[]-> a(b(x)) b(c(c(x1622))) <-9|0[]- b(c(a(x1622))) -4|[]-> b(a(a(x1622))) a(c(c(x1623))) <-9|0[]- a(c(a(x1623))) -6|[]-> c(c(a(x1623))) c(c(c(x1624))) <-9|0[]- c(c(a(x1624))) -8|[]-> a(b(a(x1624))) b(c(c(x1625))) <-9|0[]- b(c(a(x1625))) -10|[]-> a(b(a(x1625))) a(c(c(x1626))) <-9|0[]- a(c(a(x1626))) -11|[]-> a(b(a(x1626))) b(c(c(x1627))) <-9|0[]- b(c(a(x1627))) -13|[]-> b(b(a(x1627))) a(c(c(x1628))) <-9|0[]- a(c(a(x1628))) -15|[]-> c(a(a(x1628))) b(c(c(x1629))) <-9|0[]- b(c(a(x1629))) -17|[]-> c(c(a(x1629))) c(a(b(x1630))) <-10|0[]- c(b(c(x1630))) -2|[]-> a(b(c(x1630))) c(a(b(x1631))) <-10|0[]- c(b(c(x1631))) -3|[]-> c(a(c(x1631))) a(b(x)) <-10|[]- b(c(x)) -4|[]-> b(a(x)) b(a(b(x1633))) <-10|0[]- b(b(c(x1633))) -5|[]-> c(c(c(x1633))) c(a(b(x1634))) <-10|0[]- c(b(c(x1634))) -12|[]-> a(c(c(x1634))) a(b(x)) <-10|[]- b(c(x)) -13|[]-> b(b(x)) b(a(b(x1636))) <-10|0[]- b(b(c(x1636))) -14|[]-> b(a(c(x1636))) c(a(b(x1637))) <-10|0[]- c(b(c(x1637))) -16|[]-> c(c(c(x1637))) a(b(x)) <-10|[]- b(c(x)) -17|[]-> c(c(x)) b(a(b(x1639))) <-10|0[]- b(b(c(x1639))) -18|[]-> a(b(c(x1639))) b(a(b(x1640))) <-11|0[]- b(a(c(x1640))) -0|[]-> a(b(c(x1640))) c(a(b(x1641))) <-11|0[]- c(a(c(x1641))) -1|[]-> a(b(c(x1641))) a(b(x)) <-11|[]- a(c(x)) -6|[]-> c(c(x)) b(a(b(x1643))) <-11|0[]- b(a(c(x1643))) -7|[]-> c(c(c(x1643))) c(a(b(x1644))) <-11|0[]- c(a(c(x1644))) -9|[]-> c(c(c(x1644))) a(b(x)) <-11|[]- a(c(x)) -15|[]-> c(a(x)) a(c(x)) <-12|[]- c(b(x)) -2|[]-> a(b(x)) a(c(x)) <-12|[]- c(b(x)) -3|[]-> c(a(x)) b(a(c(x1648))) <-12|0[]- b(c(b(x1648))) -4|[]-> b(a(b(x1648))) a(a(c(x1649))) <-12|0[]- a(c(b(x1649))) -6|[]-> c(c(b(x1649))) c(a(c(x1650))) <-12|0[]- c(c(b(x1650))) -8|[]-> a(b(b(x1650))) b(a(c(x1651))) <-12|0[]- b(c(b(x1651))) -10|[]-> a(b(b(x1651))) a(a(c(x1652))) <-12|0[]- a(c(b(x1652))) -11|[]-> a(b(b(x1652))) b(a(c(x1653))) <-12|0[]- b(c(b(x1653))) -13|[]-> b(b(b(x1653))) a(a(c(x1654))) <-12|0[]- a(c(b(x1654))) -15|[]-> c(a(b(x1654))) a(c(x)) <-12|[]- c(b(x)) -16|[]-> c(c(x)) b(a(c(x1656))) <-12|0[]- b(c(b(x1656))) -17|[]-> c(c(b(x1656))) c(b(b(x1657))) <-13|0[]- c(b(c(x1657))) -2|[]-> a(b(c(x1657))) c(b(b(x1658))) <-13|0[]- c(b(c(x1658))) -3|[]-> c(a(c(x1658))) b(b(x)) <-13|[]- b(c(x)) -4|[]-> b(a(x)) b(b(b(x1660))) <-13|0[]- b(b(c(x1660))) -5|[]-> c(c(c(x1660))) b(b(x)) <-13|[]- b(c(x)) -10|[]-> a(b(x)) c(b(b(x1662))) <-13|0[]- c(b(c(x1662))) -12|[]-> a(c(c(x1662))) b(b(b(x1663))) <-13|0[]- b(b(c(x1663))) -14|[]-> b(a(c(x1663))) c(b(b(x1664))) <-13|0[]- c(b(c(x1664))) -16|[]-> c(c(c(x1664))) b(b(x)) <-13|[]- b(c(x)) -17|[]-> c(c(x)) b(b(b(x1666))) <-13|0[]- b(b(c(x1666))) -18|[]-> a(b(c(x1666))) c(b(a(x1667))) <-14|0[]- c(b(b(x1667))) -2|[]-> a(b(b(x1667))) c(b(a(x1668))) <-14|0[]- c(b(b(x1668))) -3|[]-> c(a(b(x1668))) b(a(x)) <-14|[]- b(b(x)) -5|[]-> c(c(x)) b(b(a(x1670))) <-14|0[]- b(b(b(x1670))) -5|[]-> c(c(b(x1670))) c(b(a(x1671))) <-14|0[]- c(b(b(x1671))) -12|[]-> a(c(b(x1671))) b(b(a(x1672))) <-14|0[]- b(b(b(x1672))) -14|[]-> b(a(b(x1672))) c(b(a(x1673))) <-14|0[]- c(b(b(x1673))) -16|[]-> c(c(b(x1673))) b(a(x)) <-14|[]- b(b(x)) -18|[]-> a(b(x)) b(b(a(x1675))) <-14|0[]- b(b(b(x1675))) -18|[]-> a(b(b(x1675))) b(c(a(x1676))) <-15|0[]- b(a(c(x1676))) -0|[]-> a(b(c(x1676))) c(c(a(x1677))) <-15|0[]- c(a(c(x1677))) -1|[]-> a(b(c(x1677))) c(a(x)) <-15|[]- a(c(x)) -6|[]-> c(c(x)) b(c(a(x1679))) <-15|0[]- b(a(c(x1679))) -7|[]-> c(c(c(x1679))) c(c(a(x1680))) <-15|0[]- c(a(c(x1680))) -9|[]-> c(c(c(x1680))) c(a(x)) <-15|[]- a(c(x)) -11|[]-> a(b(x)) c(c(x)) <-16|[]- c(b(x)) -2|[]-> a(b(x)) c(c(x)) <-16|[]- c(b(x)) -3|[]-> c(a(x)) b(c(c(x1684))) <-16|0[]- b(c(b(x1684))) -4|[]-> b(a(b(x1684))) a(c(c(x1685))) <-16|0[]- a(c(b(x1685))) -6|[]-> c(c(b(x1685))) c(c(c(x1686))) <-16|0[]- c(c(b(x1686))) -8|[]-> a(b(b(x1686))) b(c(c(x1687))) <-16|0[]- b(c(b(x1687))) -10|[]-> a(b(b(x1687))) a(c(c(x1688))) <-16|0[]- a(c(b(x1688))) -11|[]-> a(b(b(x1688))) c(c(x)) <-16|[]- c(b(x)) -12|[]-> a(c(x)) b(c(c(x1690))) <-16|0[]- b(c(b(x1690))) -13|[]-> b(b(b(x1690))) a(c(c(x1691))) <-16|0[]- a(c(b(x1691))) -15|[]-> c(a(b(x1691))) b(c(c(x1692))) <-16|0[]- b(c(b(x1692))) -17|[]-> c(c(b(x1692))) c(c(c(x1693))) <-17|0[]- c(b(c(x1693))) -2|[]-> a(b(c(x1693))) c(c(c(x1694))) <-17|0[]- c(b(c(x1694))) -3|[]-> c(a(c(x1694))) c(c(x)) <-17|[]- b(c(x)) -4|[]-> b(a(x)) b(c(c(x1696))) <-17|0[]- b(b(c(x1696))) -5|[]-> c(c(c(x1696))) c(c(x)) <-17|[]- b(c(x)) -10|[]-> a(b(x)) c(c(c(x1698))) <-17|0[]- c(b(c(x1698))) -12|[]-> a(c(c(x1698))) c(c(x)) <-17|[]- b(c(x)) -13|[]-> b(b(x)) b(c(c(x1700))) <-17|0[]- b(b(c(x1700))) -14|[]-> b(a(c(x1700))) c(c(c(x1701))) <-17|0[]- c(b(c(x1701))) -16|[]-> c(c(c(x1701))) b(c(c(x1702))) <-17|0[]- b(b(c(x1702))) -18|[]-> a(b(c(x1702))) c(a(b(x1703))) <-18|0[]- c(b(b(x1703))) -2|[]-> a(b(b(x1703))) c(a(b(x1704))) <-18|0[]- c(b(b(x1704))) -3|[]-> c(a(b(x1704))) a(b(x)) <-18|[]- b(b(x)) -5|[]-> c(c(x)) b(a(b(x1706))) <-18|0[]- b(b(b(x1706))) -5|[]-> c(c(b(x1706))) c(a(b(x1707))) <-18|0[]- c(b(b(x1707))) -12|[]-> a(c(b(x1707))) a(b(x)) <-18|[]- b(b(x)) -14|[]-> b(a(x)) b(a(b(x1709))) <-18|0[]- b(b(b(x1709))) -14|[]-> b(a(b(x1709))) c(a(b(x1710))) <-18|0[]- c(b(b(x1710))) -16|[]-> c(c(b(x1710))) b(a(b(x1711))) <-18|0[]- b(b(b(x1711))) -18|[]-> a(b(b(x1711))) Shift Processor (no label): strict: weak: Shift Processor lab=left (dd): strict: c(b(a(x1541))) -> c(a(b(x1541))) c(b(a(x1541))) -> a(b(a(x1541))) c(a(b(x1541))) -> a(b(b(x1541))) a(b(b(x1541))) -> a(c(c(x1541))) a(b(a(x1541))) -> a(c(c(x1541))) c(a(b(x1541))) -> a(b(b(x1541))) a(b(b(x1541))) -> a(b(a(x1541))) c(a(b(x1541))) -> a(b(b(x1541))) a(b(b(x1541))) -> a(a(b(x1541))) a(b(a(x1541))) -> a(a(b(x1541))) c(a(b(x1541))) -> a(b(b(x1541))) a(b(b(x1541))) -> a(a(b(x1541))) a(b(a(x1541))) -> a(c(c(x1541))) a(c(c(x1541))) -> a(a(b(x1541))) c(a(b(x1541))) -> c(c(b(x1541))) c(c(b(x1541))) -> c(a(c(x1541))) a(b(a(x1541))) -> a(c(c(x1541))) a(c(c(x1541))) -> c(a(c(x1541))) c(a(b(x1541))) -> c(c(b(x1541))) c(c(b(x1541))) -> c(c(c(x1541))) a(b(a(x1541))) -> a(c(c(x1541))) a(c(c(x1541))) -> c(c(c(x1541))) c(b(a(x1542))) -> c(a(b(x1542))) c(b(a(x1542))) -> c(a(a(x1542))) c(a(a(x1542))) -> c(c(a(x1542))) c(c(a(x1542))) -> c(a(b(x1542))) c(a(b(x1542))) -> a(b(b(x1542))) a(b(b(x1542))) -> a(c(c(x1542))) c(a(a(x1542))) -> a(b(a(x1542))) a(b(a(x1542))) -> a(c(c(x1542))) c(a(b(x1542))) -> a(b(b(x1542))) a(b(b(x1542))) -> a(b(a(x1542))) c(a(a(x1542))) -> a(b(a(x1542))) c(a(b(x1542))) -> a(b(b(x1542))) a(b(b(x1542))) -> a(b(a(x1542))) c(a(a(x1542))) -> c(c(a(x1542))) c(c(a(x1542))) -> a(b(a(x1542))) c(a(b(x1542))) -> a(b(b(x1542))) a(b(b(x1542))) -> a(a(b(x1542))) c(a(a(x1542))) -> a(b(a(x1542))) a(b(a(x1542))) -> a(a(b(x1542))) c(a(b(x1542))) -> c(c(b(x1542))) c(c(b(x1542))) -> c(c(a(x1542))) c(a(a(x1542))) -> c(c(a(x1542))) c(a(b(x1542))) -> c(c(b(x1542))) c(c(b(x1542))) -> c(c(c(x1542))) c(a(a(x1542))) -> c(c(a(x1542))) c(c(a(x1542))) -> c(c(c(x1542))) b(b(a(x1543))) -> b(a(b(x1543))) b(b(a(x1543))) -> c(c(a(x1543))) b(a(b(x1543))) -> a(b(b(x1543))) c(c(a(x1543))) -> c(a(b(x1543))) c(a(b(x1543))) -> a(b(b(x1543))) b(a(b(x1543))) -> c(c(b(x1543))) c(c(b(x1543))) -> a(b(b(x1543))) c(c(a(x1543))) -> c(a(b(x1543))) c(a(b(x1543))) -> a(b(b(x1543))) b(a(b(x1543))) -> c(c(b(x1543))) c(c(a(x1543))) -> c(a(b(x1543))) c(a(b(x1543))) -> c(c(b(x1543))) b(a(b(x1543))) -> a(b(b(x1543))) a(b(b(x1543))) -> a(c(c(x1543))) c(c(a(x1543))) -> a(b(a(x1543))) a(b(a(x1543))) -> a(c(c(x1543))) b(a(b(x1543))) -> a(b(b(x1543))) a(b(b(x1543))) -> a(b(a(x1543))) c(c(a(x1543))) -> a(b(a(x1543))) b(a(b(x1543))) -> a(b(b(x1543))) a(b(b(x1543))) -> a(a(b(x1543))) c(c(a(x1543))) -> a(b(a(x1543))) a(b(a(x1543))) -> a(a(b(x1543))) b(a(b(x1543))) -> c(c(b(x1543))) c(c(b(x1543))) -> c(a(b(x1543))) c(c(a(x1543))) -> c(a(b(x1543))) b(a(b(x1543))) -> c(c(b(x1543))) c(c(b(x1543))) -> c(a(b(x1543))) c(c(a(x1543))) -> c(c(c(x1543))) c(c(c(x1543))) -> c(a(b(x1543))) b(a(b(x1543))) -> c(c(b(x1543))) c(c(b(x1543))) -> c(c(a(x1543))) b(a(b(x1543))) -> c(c(b(x1543))) c(c(b(x1543))) -> c(c(c(x1543))) c(c(a(x1543))) -> c(c(c(x1543))) b(a(x)) -> a(b(x)) b(a(x)) -> c(c(x)) c(c(x)) -> a(b(x)) c(b(a(x1545))) -> c(a(b(x1545))) c(b(a(x1545))) -> a(c(a(x1545))) a(c(a(x1545))) -> c(c(a(x1545))) c(c(a(x1545))) -> c(a(b(x1545))) c(a(b(x1545))) -> a(b(b(x1545))) a(b(b(x1545))) -> a(c(c(x1545))) a(c(a(x1545))) -> a(c(c(x1545))) c(a(b(x1545))) -> a(b(b(x1545))) a(b(b(x1545))) -> a(c(c(x1545))) a(c(a(x1545))) -> a(b(a(x1545))) a(b(a(x1545))) -> a(c(c(x1545))) c(a(b(x1545))) -> a(b(b(x1545))) a(b(b(x1545))) -> a(b(a(x1545))) a(c(a(x1545))) -> a(b(a(x1545))) c(a(b(x1545))) -> a(b(b(x1545))) a(b(b(x1545))) -> a(b(a(x1545))) a(c(a(x1545))) -> c(c(a(x1545))) c(c(a(x1545))) -> a(b(a(x1545))) c(a(b(x1545))) -> a(b(b(x1545))) a(b(b(x1545))) -> a(b(a(x1545))) a(c(a(x1545))) -> c(a(a(x1545))) c(a(a(x1545))) -> a(b(a(x1545))) c(a(b(x1545))) -> a(b(b(x1545))) a(b(b(x1545))) -> a(a(b(x1545))) a(c(a(x1545))) -> a(a(b(x1545))) c(a(b(x1545))) -> a(b(b(x1545))) a(b(b(x1545))) -> a(a(b(x1545))) a(c(a(x1545))) -> a(c(c(x1545))) a(c(c(x1545))) -> a(a(b(x1545))) c(a(b(x1545))) -> a(b(b(x1545))) a(b(b(x1545))) -> a(a(b(x1545))) a(c(a(x1545))) -> a(b(a(x1545))) a(b(a(x1545))) -> a(a(b(x1545))) c(a(b(x1545))) -> c(c(b(x1545))) c(c(b(x1545))) -> c(c(a(x1545))) a(c(a(x1545))) -> c(c(a(x1545))) c(a(b(x1545))) -> c(c(b(x1545))) c(c(b(x1545))) -> c(c(a(x1545))) a(c(a(x1545))) -> c(a(a(x1545))) c(a(a(x1545))) -> c(c(a(x1545))) c(a(b(x1545))) -> c(c(b(x1545))) c(c(b(x1545))) -> c(a(c(x1545))) a(c(a(x1545))) -> a(c(c(x1545))) a(c(c(x1545))) -> c(a(c(x1545))) c(a(b(x1545))) -> c(c(b(x1545))) c(c(b(x1545))) -> c(c(c(x1545))) a(c(a(x1545))) -> c(c(a(x1545))) c(c(a(x1545))) -> c(c(c(x1545))) c(a(b(x1545))) -> c(c(b(x1545))) c(c(b(x1545))) -> c(c(c(x1545))) a(c(a(x1545))) -> a(c(c(x1545))) a(c(c(x1545))) -> c(c(c(x1545))) b(b(a(x1546))) -> b(a(b(x1546))) b(b(a(x1546))) -> b(a(a(x1546))) b(a(b(x1546))) -> a(b(b(x1546))) a(b(b(x1546))) -> a(c(c(x1546))) b(a(a(x1546))) -> a(b(a(x1546))) a(b(a(x1546))) -> a(c(c(x1546))) b(a(b(x1546))) -> a(b(b(x1546))) a(b(b(x1546))) -> a(b(a(x1546))) b(a(a(x1546))) -> a(b(a(x1546))) b(a(b(x1546))) -> a(b(b(x1546))) a(b(b(x1546))) -> a(b(a(x1546))) b(a(a(x1546))) -> c(c(a(x1546))) c(c(a(x1546))) -> a(b(a(x1546))) b(a(b(x1546))) -> a(b(b(x1546))) a(b(b(x1546))) -> a(a(b(x1546))) b(a(a(x1546))) -> a(b(a(x1546))) a(b(a(x1546))) -> a(a(b(x1546))) b(a(b(x1546))) -> c(c(b(x1546))) c(c(b(x1546))) -> c(a(b(x1546))) b(a(a(x1546))) -> c(c(a(x1546))) c(c(a(x1546))) -> c(a(b(x1546))) b(a(b(x1546))) -> c(c(b(x1546))) c(c(b(x1546))) -> c(c(a(x1546))) b(a(a(x1546))) -> c(c(a(x1546))) b(a(b(x1546))) -> c(c(b(x1546))) c(c(b(x1546))) -> c(c(c(x1546))) b(a(a(x1546))) -> c(c(a(x1546))) c(c(a(x1546))) -> c(c(c(x1546))) c(b(a(x1547))) -> c(a(b(x1547))) c(b(a(x1547))) -> c(c(a(x1547))) c(c(a(x1547))) -> c(a(b(x1547))) b(b(a(x1548))) -> b(a(b(x1548))) b(b(a(x1548))) -> a(b(a(x1548))) b(a(b(x1548))) -> a(b(b(x1548))) a(b(b(x1548))) -> a(c(c(x1548))) a(b(a(x1548))) -> a(c(c(x1548))) b(a(b(x1548))) -> a(b(b(x1548))) a(b(b(x1548))) -> a(b(a(x1548))) b(a(b(x1548))) -> a(b(b(x1548))) a(b(b(x1548))) -> a(a(b(x1548))) a(b(a(x1548))) -> a(a(b(x1548))) b(a(b(x1548))) -> a(b(b(x1548))) a(b(b(x1548))) -> a(a(b(x1548))) a(b(a(x1548))) -> a(c(c(x1548))) a(c(c(x1548))) -> a(a(b(x1548))) b(a(b(x1548))) -> c(c(b(x1548))) c(c(b(x1548))) -> c(a(c(x1548))) a(b(a(x1548))) -> a(c(c(x1548))) a(c(c(x1548))) -> c(a(c(x1548))) b(a(b(x1548))) -> c(c(b(x1548))) c(c(b(x1548))) -> c(c(c(x1548))) a(b(a(x1548))) -> a(c(c(x1548))) a(c(c(x1548))) -> c(c(c(x1548))) b(c(a(x1549))) -> b(a(b(x1549))) b(c(a(x1549))) -> b(a(a(x1549))) b(a(b(x1549))) -> a(b(b(x1549))) a(b(b(x1549))) -> a(c(c(x1549))) b(a(a(x1549))) -> a(b(a(x1549))) a(b(a(x1549))) -> a(c(c(x1549))) b(a(b(x1549))) -> a(b(b(x1549))) a(b(b(x1549))) -> a(b(a(x1549))) b(a(a(x1549))) -> a(b(a(x1549))) b(a(b(x1549))) -> a(b(b(x1549))) a(b(b(x1549))) -> a(b(a(x1549))) b(a(a(x1549))) -> c(c(a(x1549))) c(c(a(x1549))) -> a(b(a(x1549))) b(a(b(x1549))) -> a(b(b(x1549))) a(b(b(x1549))) -> a(a(b(x1549))) b(a(a(x1549))) -> a(b(a(x1549))) a(b(a(x1549))) -> a(a(b(x1549))) b(a(b(x1549))) -> c(c(b(x1549))) c(c(b(x1549))) -> c(a(b(x1549))) b(a(a(x1549))) -> c(c(a(x1549))) c(c(a(x1549))) -> c(a(b(x1549))) b(a(b(x1549))) -> c(c(b(x1549))) c(c(b(x1549))) -> c(c(a(x1549))) b(a(a(x1549))) -> c(c(a(x1549))) b(a(b(x1549))) -> c(c(b(x1549))) c(c(b(x1549))) -> c(c(c(x1549))) b(a(a(x1549))) -> c(c(a(x1549))) c(c(a(x1549))) -> c(c(c(x1549))) a(c(a(x1550))) -> a(a(b(x1550))) a(c(a(x1550))) -> c(c(a(x1550))) c(c(a(x1550))) -> a(b(a(x1550))) a(b(a(x1550))) -> a(a(b(x1550))) c(c(a(x1551))) -> c(a(b(x1551))) c(c(a(x1551))) -> a(b(a(x1551))) c(a(b(x1551))) -> a(b(b(x1551))) a(b(b(x1551))) -> a(c(c(x1551))) a(b(a(x1551))) -> a(c(c(x1551))) c(a(b(x1551))) -> a(b(b(x1551))) a(b(b(x1551))) -> a(b(a(x1551))) c(a(b(x1551))) -> a(b(b(x1551))) a(b(b(x1551))) -> a(a(b(x1551))) a(b(a(x1551))) -> a(a(b(x1551))) c(a(b(x1551))) -> a(b(b(x1551))) a(b(b(x1551))) -> a(a(b(x1551))) a(b(a(x1551))) -> a(c(c(x1551))) a(c(c(x1551))) -> a(a(b(x1551))) c(a(b(x1551))) -> c(c(b(x1551))) c(c(b(x1551))) -> c(a(c(x1551))) a(b(a(x1551))) -> a(c(c(x1551))) a(c(c(x1551))) -> c(a(c(x1551))) c(a(b(x1551))) -> c(c(b(x1551))) c(c(b(x1551))) -> c(c(c(x1551))) a(b(a(x1551))) -> a(c(c(x1551))) a(c(c(x1551))) -> c(c(c(x1551))) c(a(x)) -> a(b(x)) c(a(x)) -> c(c(x)) c(c(x)) -> a(b(x)) b(c(a(x1553))) -> b(a(b(x1553))) b(c(a(x1553))) -> a(b(a(x1553))) b(a(b(x1553))) -> a(b(b(x1553))) a(b(b(x1553))) -> a(c(c(x1553))) a(b(a(x1553))) -> a(c(c(x1553))) b(a(b(x1553))) -> a(b(b(x1553))) a(b(b(x1553))) -> a(b(a(x1553))) b(a(b(x1553))) -> a(b(b(x1553))) a(b(b(x1553))) -> a(a(b(x1553))) a(b(a(x1553))) -> a(a(b(x1553))) b(a(b(x1553))) -> a(b(b(x1553))) a(b(b(x1553))) -> a(a(b(x1553))) a(b(a(x1553))) -> a(c(c(x1553))) a(c(c(x1553))) -> a(a(b(x1553))) b(a(b(x1553))) -> c(c(b(x1553))) c(c(b(x1553))) -> c(a(c(x1553))) a(b(a(x1553))) -> a(c(c(x1553))) a(c(c(x1553))) -> c(a(c(x1553))) b(a(b(x1553))) -> c(c(b(x1553))) c(c(b(x1553))) -> c(c(c(x1553))) a(b(a(x1553))) -> a(c(c(x1553))) a(c(c(x1553))) -> c(c(c(x1553))) a(c(a(x1554))) -> a(a(b(x1554))) a(c(a(x1554))) -> a(b(a(x1554))) a(b(a(x1554))) -> a(a(b(x1554))) b(c(a(x1555))) -> b(a(b(x1555))) b(c(a(x1555))) -> b(b(a(x1555))) b(b(a(x1555))) -> b(a(b(x1555))) a(c(a(x1556))) -> a(a(b(x1556))) a(c(a(x1556))) -> c(a(a(x1556))) c(a(a(x1556))) -> a(b(a(x1556))) a(b(a(x1556))) -> a(a(b(x1556))) b(c(a(x1557))) -> b(a(b(x1557))) b(c(a(x1557))) -> c(c(a(x1557))) b(a(b(x1557))) -> a(b(b(x1557))) c(c(a(x1557))) -> c(a(b(x1557))) c(a(b(x1557))) -> a(b(b(x1557))) b(a(b(x1557))) -> c(c(b(x1557))) c(c(b(x1557))) -> a(b(b(x1557))) c(c(a(x1557))) -> c(a(b(x1557))) c(a(b(x1557))) -> a(b(b(x1557))) b(a(b(x1557))) -> c(c(b(x1557))) c(c(a(x1557))) -> c(a(b(x1557))) c(a(b(x1557))) -> c(c(b(x1557))) b(a(b(x1557))) -> a(b(b(x1557))) a(b(b(x1557))) -> a(c(c(x1557))) c(c(a(x1557))) -> a(b(a(x1557))) a(b(a(x1557))) -> a(c(c(x1557))) b(a(b(x1557))) -> a(b(b(x1557))) a(b(b(x1557))) -> a(b(a(x1557))) c(c(a(x1557))) -> a(b(a(x1557))) b(a(b(x1557))) -> a(b(b(x1557))) a(b(b(x1557))) -> a(a(b(x1557))) c(c(a(x1557))) -> a(b(a(x1557))) a(b(a(x1557))) -> a(a(b(x1557))) b(a(b(x1557))) -> c(c(b(x1557))) c(c(b(x1557))) -> c(a(b(x1557))) c(c(a(x1557))) -> c(a(b(x1557))) b(a(b(x1557))) -> c(c(b(x1557))) c(c(b(x1557))) -> c(a(b(x1557))) c(c(a(x1557))) -> c(c(c(x1557))) c(c(c(x1557))) -> c(a(b(x1557))) b(a(b(x1557))) -> c(c(b(x1557))) c(c(b(x1557))) -> c(c(a(x1557))) b(a(b(x1557))) -> c(c(b(x1557))) c(c(b(x1557))) -> c(c(c(x1557))) c(c(a(x1557))) -> c(c(c(x1557))) c(b(x)) -> a(b(x)) c(b(x)) -> c(a(x)) c(a(x)) -> a(b(x)) b(c(b(x1559))) -> b(a(b(x1559))) b(c(b(x1559))) -> b(a(b(x1559))) a(c(b(x1560))) -> a(a(b(x1560))) a(c(b(x1560))) -> c(c(b(x1560))) c(c(b(x1560))) -> a(b(b(x1560))) a(b(b(x1560))) -> a(a(b(x1560))) c(c(b(x1561))) -> c(a(b(x1561))) c(c(b(x1561))) -> a(b(b(x1561))) c(a(b(x1561))) -> a(b(b(x1561))) b(c(b(x1562))) -> b(a(b(x1562))) b(c(b(x1562))) -> a(b(b(x1562))) b(a(b(x1562))) -> a(b(b(x1562))) a(c(b(x1563))) -> a(a(b(x1563))) a(c(b(x1563))) -> a(b(b(x1563))) a(b(b(x1563))) -> a(a(b(x1563))) c(b(x)) -> a(b(x)) c(b(x)) -> a(c(x)) a(c(x)) -> a(b(x)) b(c(b(x1565))) -> b(a(b(x1565))) b(c(b(x1565))) -> b(b(b(x1565))) b(b(b(x1565))) -> b(a(b(x1565))) b(a(b(x1565))) -> a(b(b(x1565))) b(b(b(x1565))) -> a(b(b(x1565))) b(a(b(x1565))) -> c(c(b(x1565))) b(b(b(x1565))) -> c(c(b(x1565))) a(c(b(x1566))) -> a(a(b(x1566))) a(c(b(x1566))) -> c(a(b(x1566))) c(a(b(x1566))) -> a(b(b(x1566))) a(b(b(x1566))) -> a(a(b(x1566))) c(b(x)) -> a(b(x)) c(b(x)) -> c(c(x)) c(c(x)) -> a(b(x)) b(c(b(x1568))) -> b(a(b(x1568))) b(c(b(x1568))) -> c(c(b(x1568))) b(a(b(x1568))) -> a(b(b(x1568))) c(c(b(x1568))) -> a(b(b(x1568))) b(a(b(x1568))) -> c(c(b(x1568))) c(b(x)) -> c(a(x)) c(b(x)) -> a(b(x)) c(a(x)) -> a(b(x)) b(c(b(x1570))) -> b(c(a(x1570))) b(c(b(x1570))) -> b(a(b(x1570))) b(c(a(x1570))) -> b(a(b(x1570))) a(c(b(x1571))) -> a(c(a(x1571))) a(c(b(x1571))) -> c(c(b(x1571))) a(c(a(x1571))) -> c(c(a(x1571))) c(c(b(x1571))) -> c(c(a(x1571))) c(c(b(x1572))) -> c(c(a(x1572))) c(c(b(x1572))) -> a(b(b(x1572))) c(c(a(x1572))) -> a(b(a(x1572))) a(b(b(x1572))) -> a(b(a(x1572))) b(c(b(x1573))) -> b(c(a(x1573))) b(c(b(x1573))) -> a(b(b(x1573))) b(c(a(x1573))) -> a(b(a(x1573))) a(b(b(x1573))) -> a(b(a(x1573))) a(c(b(x1574))) -> a(c(a(x1574))) a(c(b(x1574))) -> a(b(b(x1574))) a(c(a(x1574))) -> a(a(b(x1574))) a(b(b(x1574))) -> a(a(b(x1574))) a(c(a(x1574))) -> a(c(c(x1574))) a(b(b(x1574))) -> a(c(c(x1574))) a(c(a(x1574))) -> a(b(a(x1574))) a(b(b(x1574))) -> a(b(a(x1574))) c(b(x)) -> c(a(x)) c(b(x)) -> a(c(x)) a(c(x)) -> c(a(x)) c(a(x)) -> a(b(x)) a(c(x)) -> a(b(x)) c(a(x)) -> c(c(x)) a(c(x)) -> c(c(x)) b(c(b(x1576))) -> b(c(a(x1576))) b(c(b(x1576))) -> b(b(b(x1576))) b(c(a(x1576))) -> b(a(b(x1576))) b(b(b(x1576))) -> b(a(b(x1576))) b(c(a(x1576))) -> b(c(c(x1576))) b(b(b(x1576))) -> b(c(c(x1576))) b(c(a(x1576))) -> b(b(a(x1576))) b(b(b(x1576))) -> b(b(a(x1576))) a(c(b(x1577))) -> a(c(a(x1577))) a(c(b(x1577))) -> c(a(b(x1577))) a(c(a(x1577))) -> a(a(b(x1577))) c(a(b(x1577))) -> a(b(b(x1577))) a(b(b(x1577))) -> a(a(b(x1577))) a(c(a(x1577))) -> a(c(c(x1577))) a(c(c(x1577))) -> a(a(b(x1577))) c(a(b(x1577))) -> a(b(b(x1577))) a(b(b(x1577))) -> a(a(b(x1577))) a(c(a(x1577))) -> a(b(a(x1577))) a(b(a(x1577))) -> a(a(b(x1577))) c(a(b(x1577))) -> a(b(b(x1577))) a(b(b(x1577))) -> a(a(b(x1577))) a(c(a(x1577))) -> c(c(a(x1577))) c(a(b(x1577))) -> c(c(b(x1577))) c(c(b(x1577))) -> c(c(a(x1577))) a(c(a(x1577))) -> c(a(a(x1577))) c(a(a(x1577))) -> c(c(a(x1577))) c(a(b(x1577))) -> c(c(b(x1577))) c(c(b(x1577))) -> c(c(a(x1577))) a(c(a(x1577))) -> a(c(c(x1577))) c(a(b(x1577))) -> a(b(b(x1577))) a(b(b(x1577))) -> a(c(c(x1577))) a(c(a(x1577))) -> a(b(a(x1577))) a(b(a(x1577))) -> a(c(c(x1577))) c(a(b(x1577))) -> a(b(b(x1577))) a(b(b(x1577))) -> a(c(c(x1577))) a(c(a(x1577))) -> a(b(a(x1577))) c(a(b(x1577))) -> a(b(b(x1577))) a(b(b(x1577))) -> a(b(a(x1577))) a(c(a(x1577))) -> c(c(a(x1577))) c(c(a(x1577))) -> a(b(a(x1577))) c(a(b(x1577))) -> a(b(b(x1577))) a(b(b(x1577))) -> a(b(a(x1577))) a(c(a(x1577))) -> c(a(a(x1577))) c(a(a(x1577))) -> a(b(a(x1577))) c(a(b(x1577))) -> a(b(b(x1577))) a(b(b(x1577))) -> a(b(a(x1577))) a(c(a(x1577))) -> c(c(a(x1577))) c(c(a(x1577))) -> c(a(b(x1577))) a(c(a(x1577))) -> c(c(a(x1577))) c(c(a(x1577))) -> c(c(c(x1577))) c(a(b(x1577))) -> c(c(b(x1577))) c(c(b(x1577))) -> c(c(c(x1577))) a(c(a(x1577))) -> a(c(c(x1577))) a(c(c(x1577))) -> c(c(c(x1577))) c(a(b(x1577))) -> c(c(b(x1577))) c(c(b(x1577))) -> c(c(c(x1577))) a(c(a(x1577))) -> a(c(c(x1577))) a(c(c(x1577))) -> c(a(c(x1577))) c(a(b(x1577))) -> c(c(b(x1577))) c(c(b(x1577))) -> c(a(c(x1577))) c(b(x)) -> c(a(x)) c(b(x)) -> c(c(x)) c(a(x)) -> a(b(x)) c(c(x)) -> a(b(x)) c(a(x)) -> c(c(x)) b(c(b(x1579))) -> b(c(a(x1579))) b(c(b(x1579))) -> c(c(b(x1579))) b(c(a(x1579))) -> c(c(a(x1579))) c(c(b(x1579))) -> c(c(a(x1579))) c(b(c(x1580))) -> c(b(a(x1580))) c(b(c(x1580))) -> a(b(c(x1580))) c(b(a(x1580))) -> a(b(a(x1580))) a(b(c(x1580))) -> a(b(a(x1580))) c(b(c(x1581))) -> c(b(a(x1581))) c(b(c(x1581))) -> c(a(c(x1581))) c(b(a(x1581))) -> c(a(b(x1581))) c(a(c(x1581))) -> c(a(b(x1581))) c(b(a(x1581))) -> c(c(c(x1581))) c(a(c(x1581))) -> c(c(c(x1581))) c(b(a(x1581))) -> c(c(a(x1581))) c(a(c(x1581))) -> c(c(a(x1581))) b(b(c(x1582))) -> b(b(a(x1582))) b(b(c(x1582))) -> c(c(c(x1582))) b(b(a(x1582))) -> a(b(a(x1582))) c(c(c(x1582))) -> a(b(c(x1582))) a(b(c(x1582))) -> a(b(a(x1582))) b(b(a(x1582))) -> c(c(a(x1582))) c(c(a(x1582))) -> a(b(a(x1582))) c(c(c(x1582))) -> a(b(c(x1582))) a(b(c(x1582))) -> a(b(a(x1582))) b(b(a(x1582))) -> b(a(a(x1582))) b(a(a(x1582))) -> a(b(a(x1582))) c(c(c(x1582))) -> a(b(c(x1582))) a(b(c(x1582))) -> a(b(a(x1582))) b(b(a(x1582))) -> b(a(b(x1582))) b(a(b(x1582))) -> a(b(b(x1582))) c(c(c(x1582))) -> c(a(b(x1582))) c(a(b(x1582))) -> a(b(b(x1582))) b(b(a(x1582))) -> b(a(b(x1582))) b(a(b(x1582))) -> a(b(b(x1582))) c(c(c(x1582))) -> a(b(c(x1582))) a(b(c(x1582))) -> a(b(b(x1582))) b(b(a(x1582))) -> b(a(b(x1582))) b(a(b(x1582))) -> c(c(b(x1582))) c(c(c(x1582))) -> c(a(b(x1582))) c(a(b(x1582))) -> c(c(b(x1582))) b(b(a(x1582))) -> c(c(a(x1582))) c(c(a(x1582))) -> c(a(b(x1582))) c(c(c(x1582))) -> c(a(b(x1582))) b(b(a(x1582))) -> c(c(a(x1582))) c(c(a(x1582))) -> c(c(c(x1582))) b(b(a(x1582))) -> b(c(c(x1582))) b(c(c(x1582))) -> c(c(c(x1582))) b(b(a(x1582))) -> b(c(c(x1582))) b(c(c(x1582))) -> a(b(c(x1582))) c(c(c(x1582))) -> a(b(c(x1582))) b(b(a(x1582))) -> a(b(a(x1582))) a(b(a(x1582))) -> a(a(b(x1582))) c(c(c(x1582))) -> a(b(c(x1582))) a(b(c(x1582))) -> a(a(b(x1582))) b(b(a(x1582))) -> a(b(a(x1582))) a(b(a(x1582))) -> a(c(c(x1582))) c(c(c(x1582))) -> a(b(c(x1582))) a(b(c(x1582))) -> a(c(c(x1582))) b(c(x)) -> b(a(x)) b(c(x)) -> a(b(x)) b(a(x)) -> a(b(x)) c(b(c(x1584))) -> c(b(a(x1584))) c(b(c(x1584))) -> a(c(c(x1584))) c(b(a(x1584))) -> c(c(c(x1584))) a(c(c(x1584))) -> c(c(c(x1584))) b(c(x)) -> b(a(x)) b(c(x)) -> b(b(x)) b(b(x)) -> b(a(x)) b(a(x)) -> a(b(x)) b(b(x)) -> a(b(x)) b(a(x)) -> c(c(x)) b(b(x)) -> c(c(x)) b(b(c(x1586))) -> b(b(a(x1586))) b(b(c(x1586))) -> b(a(c(x1586))) b(b(a(x1586))) -> b(a(b(x1586))) b(a(c(x1586))) -> b(a(b(x1586))) b(b(a(x1586))) -> b(c(c(x1586))) b(a(c(x1586))) -> b(c(c(x1586))) c(b(c(x1587))) -> c(b(a(x1587))) c(b(c(x1587))) -> c(c(c(x1587))) c(b(a(x1587))) -> c(a(b(x1587))) c(c(c(x1587))) -> c(a(b(x1587))) c(b(a(x1587))) -> c(c(c(x1587))) b(c(x)) -> b(a(x)) b(c(x)) -> c(c(x)) b(a(x)) -> a(b(x)) c(c(x)) -> a(b(x)) b(a(x)) -> c(c(x)) b(b(c(x1589))) -> b(b(a(x1589))) b(b(c(x1589))) -> a(b(c(x1589))) b(b(a(x1589))) -> a(b(a(x1589))) a(b(c(x1589))) -> a(b(a(x1589))) c(b(b(x1590))) -> c(c(c(x1590))) c(b(b(x1590))) -> a(b(b(x1590))) a(b(b(x1590))) -> a(c(c(x1590))) a(c(c(x1590))) -> c(c(c(x1590))) c(c(c(x1590))) -> a(b(c(x1590))) a(b(b(x1590))) -> a(c(c(x1590))) a(c(c(x1590))) -> a(b(c(x1590))) c(c(c(x1590))) -> c(a(b(x1590))) c(a(b(x1590))) -> a(b(b(x1590))) c(c(c(x1590))) -> a(b(c(x1590))) a(b(c(x1590))) -> a(b(b(x1590))) c(c(c(x1590))) -> a(b(c(x1590))) a(b(c(x1590))) -> a(b(a(x1590))) a(b(b(x1590))) -> a(b(a(x1590))) c(c(c(x1590))) -> a(b(c(x1590))) a(b(c(x1590))) -> a(a(b(x1590))) a(b(b(x1590))) -> a(a(b(x1590))) c(c(c(x1590))) -> a(b(c(x1590))) a(b(c(x1590))) -> a(a(b(x1590))) a(b(b(x1590))) -> a(c(c(x1590))) a(c(c(x1590))) -> a(a(b(x1590))) c(c(c(x1590))) -> a(b(c(x1590))) a(b(c(x1590))) -> a(a(b(x1590))) a(b(b(x1590))) -> a(b(a(x1590))) a(b(a(x1590))) -> a(a(b(x1590))) c(c(c(x1590))) -> a(b(c(x1590))) a(b(c(x1590))) -> a(c(c(x1590))) a(b(b(x1590))) -> a(c(c(x1590))) c(c(c(x1590))) -> a(b(c(x1590))) a(b(c(x1590))) -> a(c(c(x1590))) a(b(b(x1590))) -> a(b(a(x1590))) a(b(a(x1590))) -> a(c(c(x1590))) c(b(b(x1591))) -> c(c(c(x1591))) c(b(b(x1591))) -> c(a(b(x1591))) c(c(c(x1591))) -> c(a(b(x1591))) b(b(b(x1592))) -> b(c(c(x1592))) b(b(b(x1592))) -> c(c(b(x1592))) b(c(c(x1592))) -> c(c(c(x1592))) c(c(b(x1592))) -> c(c(c(x1592))) c(b(b(x1593))) -> c(c(c(x1593))) c(b(b(x1593))) -> a(c(b(x1593))) c(c(c(x1593))) -> c(a(b(x1593))) a(c(b(x1593))) -> c(a(b(x1593))) b(b(x)) -> c(c(x)) b(b(x)) -> b(a(x)) b(a(x)) -> c(c(x)) c(c(x)) -> a(b(x)) b(a(x)) -> a(b(x)) b(b(b(x1595))) -> b(c(c(x1595))) b(b(b(x1595))) -> b(a(b(x1595))) b(c(c(x1595))) -> b(a(b(x1595))) c(b(b(x1596))) -> c(c(c(x1596))) c(b(b(x1596))) -> c(c(b(x1596))) c(c(b(x1596))) -> c(c(c(x1596))) c(c(c(x1596))) -> c(a(b(x1596))) c(c(b(x1596))) -> c(a(b(x1596))) b(b(x)) -> c(c(x)) b(b(x)) -> a(b(x)) c(c(x)) -> a(b(x)) b(b(b(x1598))) -> b(c(c(x1598))) b(b(b(x1598))) -> a(b(b(x1598))) b(c(c(x1598))) -> a(b(c(x1598))) a(b(b(x1598))) -> a(c(c(x1598))) a(c(c(x1598))) -> a(b(c(x1598))) b(c(c(x1598))) -> b(a(c(x1598))) b(a(c(x1598))) -> a(b(c(x1598))) a(b(b(x1598))) -> a(c(c(x1598))) a(c(c(x1598))) -> a(b(c(x1598))) b(c(c(x1598))) -> b(b(c(x1598))) b(b(c(x1598))) -> a(b(c(x1598))) a(b(b(x1598))) -> a(c(c(x1598))) a(c(c(x1598))) -> a(b(c(x1598))) b(c(c(x1598))) -> c(c(c(x1598))) c(c(c(x1598))) -> a(b(c(x1598))) a(b(b(x1598))) -> a(c(c(x1598))) a(c(c(x1598))) -> a(b(c(x1598))) b(c(c(x1598))) -> c(c(c(x1598))) a(b(b(x1598))) -> a(c(c(x1598))) a(c(c(x1598))) -> c(c(c(x1598))) b(c(c(x1598))) -> b(a(c(x1598))) b(a(c(x1598))) -> c(c(c(x1598))) a(b(b(x1598))) -> a(c(c(x1598))) a(c(c(x1598))) -> c(c(c(x1598))) b(c(c(x1598))) -> b(b(c(x1598))) b(b(c(x1598))) -> c(c(c(x1598))) a(b(b(x1598))) -> a(c(c(x1598))) a(c(c(x1598))) -> c(c(c(x1598))) b(c(c(x1598))) -> b(a(b(x1598))) b(a(b(x1598))) -> a(b(b(x1598))) b(c(c(x1598))) -> a(b(c(x1598))) a(b(c(x1598))) -> a(b(b(x1598))) b(c(c(x1598))) -> a(b(c(x1598))) a(b(c(x1598))) -> a(b(a(x1598))) a(b(b(x1598))) -> a(b(a(x1598))) b(c(c(x1598))) -> a(b(c(x1598))) a(b(c(x1598))) -> a(a(b(x1598))) a(b(b(x1598))) -> a(a(b(x1598))) b(c(c(x1598))) -> a(b(c(x1598))) a(b(c(x1598))) -> a(a(b(x1598))) a(b(b(x1598))) -> a(c(c(x1598))) a(c(c(x1598))) -> a(a(b(x1598))) b(c(c(x1598))) -> a(b(c(x1598))) a(b(c(x1598))) -> a(a(b(x1598))) a(b(b(x1598))) -> a(b(a(x1598))) a(b(a(x1598))) -> a(a(b(x1598))) b(c(c(x1598))) -> a(b(c(x1598))) a(b(c(x1598))) -> a(c(c(x1598))) a(b(b(x1598))) -> a(c(c(x1598))) b(c(c(x1598))) -> a(b(c(x1598))) a(b(c(x1598))) -> a(c(c(x1598))) a(b(b(x1598))) -> a(b(a(x1598))) a(b(a(x1598))) -> a(c(c(x1598))) b(a(c(x1599))) -> b(c(c(x1599))) b(a(c(x1599))) -> a(b(c(x1599))) b(c(c(x1599))) -> a(b(c(x1599))) c(a(c(x1600))) -> c(c(c(x1600))) c(a(c(x1600))) -> a(b(c(x1600))) c(c(c(x1600))) -> a(b(c(x1600))) b(a(c(x1601))) -> b(c(c(x1601))) b(a(c(x1601))) -> c(c(c(x1601))) b(c(c(x1601))) -> a(b(c(x1601))) c(c(c(x1601))) -> a(b(c(x1601))) b(c(c(x1601))) -> c(c(c(x1601))) c(a(c(x1602))) -> c(c(c(x1602))) c(a(c(x1602))) -> c(c(c(x1602))) a(c(x)) -> c(c(x)) a(c(x)) -> a(b(x)) c(c(x)) -> a(b(x)) a(c(x)) -> c(c(x)) a(c(x)) -> c(a(x)) c(a(x)) -> c(c(x)) c(c(x)) -> a(b(x)) c(a(x)) -> a(b(x)) b(a(x)) -> c(c(x)) b(a(x)) -> a(b(x)) c(c(x)) -> a(b(x)) c(b(a(x1606))) -> c(c(c(x1606))) c(b(a(x1606))) -> a(b(a(x1606))) a(b(a(x1606))) -> a(c(c(x1606))) a(c(c(x1606))) -> c(c(c(x1606))) c(c(c(x1606))) -> a(b(c(x1606))) a(b(a(x1606))) -> a(c(c(x1606))) a(c(c(x1606))) -> a(b(c(x1606))) c(c(c(x1606))) -> a(b(c(x1606))) a(b(c(x1606))) -> a(b(a(x1606))) c(c(c(x1606))) -> a(b(c(x1606))) a(b(c(x1606))) -> a(a(b(x1606))) a(b(a(x1606))) -> a(a(b(x1606))) c(c(c(x1606))) -> a(b(c(x1606))) a(b(c(x1606))) -> a(a(b(x1606))) a(b(a(x1606))) -> a(c(c(x1606))) a(c(c(x1606))) -> a(a(b(x1606))) c(c(c(x1606))) -> a(b(c(x1606))) a(b(c(x1606))) -> a(c(c(x1606))) a(b(a(x1606))) -> a(c(c(x1606))) c(b(a(x1607))) -> c(c(c(x1607))) c(b(a(x1607))) -> c(a(a(x1607))) c(a(a(x1607))) -> c(c(a(x1607))) c(c(a(x1607))) -> c(c(c(x1607))) c(c(c(x1607))) -> c(a(b(x1607))) c(a(a(x1607))) -> c(c(a(x1607))) c(c(a(x1607))) -> c(a(b(x1607))) c(c(c(x1607))) -> a(b(c(x1607))) a(b(c(x1607))) -> a(b(a(x1607))) c(a(a(x1607))) -> a(b(a(x1607))) c(c(c(x1607))) -> a(b(c(x1607))) a(b(c(x1607))) -> a(b(a(x1607))) c(a(a(x1607))) -> c(c(a(x1607))) c(c(a(x1607))) -> a(b(a(x1607))) c(c(c(x1607))) -> a(b(c(x1607))) a(b(c(x1607))) -> a(a(b(x1607))) c(a(a(x1607))) -> a(b(a(x1607))) a(b(a(x1607))) -> a(a(b(x1607))) c(c(c(x1607))) -> a(b(c(x1607))) a(b(c(x1607))) -> a(c(c(x1607))) c(a(a(x1607))) -> a(b(a(x1607))) a(b(a(x1607))) -> a(c(c(x1607))) b(b(a(x1608))) -> b(c(c(x1608))) b(b(a(x1608))) -> c(c(a(x1608))) b(c(c(x1608))) -> c(c(c(x1608))) c(c(a(x1608))) -> c(c(c(x1608))) c(b(a(x1609))) -> c(c(c(x1609))) c(b(a(x1609))) -> a(c(a(x1609))) a(c(a(x1609))) -> c(c(a(x1609))) c(c(a(x1609))) -> c(c(c(x1609))) a(c(a(x1609))) -> a(c(c(x1609))) a(c(c(x1609))) -> c(c(c(x1609))) c(c(c(x1609))) -> c(a(b(x1609))) a(c(a(x1609))) -> c(c(a(x1609))) c(c(a(x1609))) -> c(a(b(x1609))) c(c(c(x1609))) -> a(b(c(x1609))) a(c(a(x1609))) -> a(c(c(x1609))) a(c(c(x1609))) -> a(b(c(x1609))) c(c(c(x1609))) -> a(b(c(x1609))) a(b(c(x1609))) -> a(b(a(x1609))) a(c(a(x1609))) -> a(b(a(x1609))) c(c(c(x1609))) -> a(b(c(x1609))) a(b(c(x1609))) -> a(b(a(x1609))) a(c(a(x1609))) -> c(c(a(x1609))) c(c(a(x1609))) -> a(b(a(x1609))) c(c(c(x1609))) -> a(b(c(x1609))) a(b(c(x1609))) -> a(b(a(x1609))) a(c(a(x1609))) -> c(a(a(x1609))) c(a(a(x1609))) -> a(b(a(x1609))) c(c(c(x1609))) -> a(b(c(x1609))) a(b(c(x1609))) -> a(a(b(x1609))) a(c(a(x1609))) -> a(a(b(x1609))) c(c(c(x1609))) -> a(b(c(x1609))) a(b(c(x1609))) -> a(a(b(x1609))) a(c(a(x1609))) -> a(c(c(x1609))) a(c(c(x1609))) -> a(a(b(x1609))) c(c(c(x1609))) -> a(b(c(x1609))) a(b(c(x1609))) -> a(a(b(x1609))) a(c(a(x1609))) -> a(b(a(x1609))) a(b(a(x1609))) -> a(a(b(x1609))) c(c(c(x1609))) -> a(b(c(x1609))) a(b(c(x1609))) -> a(c(c(x1609))) a(c(a(x1609))) -> a(c(c(x1609))) c(c(c(x1609))) -> a(b(c(x1609))) a(b(c(x1609))) -> a(c(c(x1609))) a(c(a(x1609))) -> a(b(a(x1609))) a(b(a(x1609))) -> a(c(c(x1609))) b(b(a(x1610))) -> b(c(c(x1610))) b(b(a(x1610))) -> b(a(a(x1610))) b(c(c(x1610))) -> c(c(c(x1610))) b(a(a(x1610))) -> c(c(a(x1610))) c(c(a(x1610))) -> c(c(c(x1610))) b(c(c(x1610))) -> b(a(c(x1610))) b(a(c(x1610))) -> c(c(c(x1610))) b(a(a(x1610))) -> c(c(a(x1610))) c(c(a(x1610))) -> c(c(c(x1610))) b(c(c(x1610))) -> b(b(c(x1610))) b(b(c(x1610))) -> c(c(c(x1610))) b(a(a(x1610))) -> c(c(a(x1610))) c(c(a(x1610))) -> c(c(c(x1610))) b(c(c(x1610))) -> a(b(c(x1610))) a(b(c(x1610))) -> a(b(a(x1610))) b(a(a(x1610))) -> a(b(a(x1610))) b(c(c(x1610))) -> a(b(c(x1610))) a(b(c(x1610))) -> a(b(a(x1610))) b(a(a(x1610))) -> c(c(a(x1610))) c(c(a(x1610))) -> a(b(a(x1610))) b(c(c(x1610))) -> a(b(c(x1610))) a(b(c(x1610))) -> a(a(b(x1610))) b(a(a(x1610))) -> a(b(a(x1610))) a(b(a(x1610))) -> a(a(b(x1610))) b(c(c(x1610))) -> a(b(c(x1610))) a(b(c(x1610))) -> a(c(c(x1610))) b(a(a(x1610))) -> a(b(a(x1610))) a(b(a(x1610))) -> a(c(c(x1610))) b(c(c(x1610))) -> c(c(c(x1610))) c(c(c(x1610))) -> c(a(b(x1610))) b(a(a(x1610))) -> c(c(a(x1610))) c(c(a(x1610))) -> c(a(b(x1610))) c(b(a(x1611))) -> c(c(c(x1611))) c(b(a(x1611))) -> c(c(a(x1611))) c(c(a(x1611))) -> c(c(c(x1611))) c(c(c(x1611))) -> c(a(b(x1611))) c(c(a(x1611))) -> c(a(b(x1611))) b(b(a(x1612))) -> b(c(c(x1612))) b(b(a(x1612))) -> a(b(a(x1612))) b(c(c(x1612))) -> a(b(c(x1612))) a(b(a(x1612))) -> a(c(c(x1612))) a(c(c(x1612))) -> a(b(c(x1612))) b(c(c(x1612))) -> b(a(c(x1612))) b(a(c(x1612))) -> a(b(c(x1612))) a(b(a(x1612))) -> a(c(c(x1612))) a(c(c(x1612))) -> a(b(c(x1612))) b(c(c(x1612))) -> b(b(c(x1612))) b(b(c(x1612))) -> a(b(c(x1612))) a(b(a(x1612))) -> a(c(c(x1612))) a(c(c(x1612))) -> a(b(c(x1612))) b(c(c(x1612))) -> c(c(c(x1612))) c(c(c(x1612))) -> a(b(c(x1612))) a(b(a(x1612))) -> a(c(c(x1612))) a(c(c(x1612))) -> a(b(c(x1612))) b(c(c(x1612))) -> c(c(c(x1612))) a(b(a(x1612))) -> a(c(c(x1612))) a(c(c(x1612))) -> c(c(c(x1612))) b(c(c(x1612))) -> b(a(c(x1612))) b(a(c(x1612))) -> c(c(c(x1612))) a(b(a(x1612))) -> a(c(c(x1612))) a(c(c(x1612))) -> c(c(c(x1612))) b(c(c(x1612))) -> b(b(c(x1612))) b(b(c(x1612))) -> c(c(c(x1612))) a(b(a(x1612))) -> a(c(c(x1612))) a(c(c(x1612))) -> c(c(c(x1612))) b(c(c(x1612))) -> a(b(c(x1612))) a(b(c(x1612))) -> a(b(a(x1612))) b(c(c(x1612))) -> a(b(c(x1612))) a(b(c(x1612))) -> a(a(b(x1612))) a(b(a(x1612))) -> a(a(b(x1612))) b(c(c(x1612))) -> a(b(c(x1612))) a(b(c(x1612))) -> a(a(b(x1612))) a(b(a(x1612))) -> a(c(c(x1612))) a(c(c(x1612))) -> a(a(b(x1612))) b(c(c(x1612))) -> a(b(c(x1612))) a(b(c(x1612))) -> a(c(c(x1612))) a(b(a(x1612))) -> a(c(c(x1612))) b(c(c(x1613))) -> b(a(b(x1613))) b(c(c(x1613))) -> b(a(c(x1613))) b(a(c(x1613))) -> b(a(b(x1613))) a(c(c(x1614))) -> a(a(b(x1614))) a(c(c(x1614))) -> c(c(c(x1614))) c(c(c(x1614))) -> a(b(c(x1614))) a(b(c(x1614))) -> a(a(b(x1614))) c(c(c(x1615))) -> c(a(b(x1615))) c(c(c(x1615))) -> a(b(c(x1615))) c(a(b(x1615))) -> a(b(b(x1615))) a(b(c(x1615))) -> a(b(b(x1615))) b(c(c(x1616))) -> b(a(b(x1616))) b(c(c(x1616))) -> a(b(c(x1616))) b(a(b(x1616))) -> a(b(b(x1616))) a(b(c(x1616))) -> a(b(b(x1616))) a(c(c(x1617))) -> a(a(b(x1617))) a(c(c(x1617))) -> a(b(c(x1617))) a(b(c(x1617))) -> a(a(b(x1617))) b(c(c(x1618))) -> b(a(b(x1618))) b(c(c(x1618))) -> b(b(c(x1618))) b(b(c(x1618))) -> b(a(b(x1618))) a(c(c(x1619))) -> a(a(b(x1619))) a(c(c(x1619))) -> c(a(c(x1619))) c(a(c(x1619))) -> a(b(c(x1619))) a(b(c(x1619))) -> a(a(b(x1619))) b(c(c(x1620))) -> b(a(b(x1620))) b(c(c(x1620))) -> c(c(c(x1620))) b(a(b(x1620))) -> a(b(b(x1620))) c(c(c(x1620))) -> c(a(b(x1620))) c(a(b(x1620))) -> a(b(b(x1620))) b(a(b(x1620))) -> a(b(b(x1620))) c(c(c(x1620))) -> a(b(c(x1620))) a(b(c(x1620))) -> a(b(b(x1620))) b(a(b(x1620))) -> c(c(b(x1620))) c(c(b(x1620))) -> a(b(b(x1620))) c(c(c(x1620))) -> c(a(b(x1620))) c(a(b(x1620))) -> a(b(b(x1620))) b(a(b(x1620))) -> c(c(b(x1620))) c(c(b(x1620))) -> a(b(b(x1620))) c(c(c(x1620))) -> a(b(c(x1620))) a(b(c(x1620))) -> a(b(b(x1620))) b(a(b(x1620))) -> c(c(b(x1620))) c(c(c(x1620))) -> c(a(b(x1620))) c(a(b(x1620))) -> c(c(b(x1620))) b(a(b(x1620))) -> a(b(b(x1620))) a(b(b(x1620))) -> a(c(c(x1620))) c(c(c(x1620))) -> a(b(c(x1620))) a(b(c(x1620))) -> a(c(c(x1620))) b(a(b(x1620))) -> a(b(b(x1620))) a(b(b(x1620))) -> a(b(a(x1620))) c(c(c(x1620))) -> a(b(c(x1620))) a(b(c(x1620))) -> a(b(a(x1620))) b(a(b(x1620))) -> a(b(b(x1620))) a(b(b(x1620))) -> a(a(b(x1620))) c(c(c(x1620))) -> a(b(c(x1620))) a(b(c(x1620))) -> a(a(b(x1620))) b(a(b(x1620))) -> c(c(b(x1620))) c(c(b(x1620))) -> c(a(b(x1620))) c(c(c(x1620))) -> c(a(b(x1620))) b(a(b(x1620))) -> c(c(b(x1620))) c(c(b(x1620))) -> c(c(c(x1620))) c(a(x)) -> c(c(x)) c(a(x)) -> a(b(x)) c(c(x)) -> a(b(x)) b(c(a(x1622))) -> b(c(c(x1622))) b(c(a(x1622))) -> b(a(a(x1622))) b(c(c(x1622))) -> c(c(c(x1622))) b(a(a(x1622))) -> c(c(a(x1622))) c(c(a(x1622))) -> c(c(c(x1622))) b(c(c(x1622))) -> b(a(c(x1622))) b(a(c(x1622))) -> c(c(c(x1622))) b(a(a(x1622))) -> c(c(a(x1622))) c(c(a(x1622))) -> c(c(c(x1622))) b(c(c(x1622))) -> b(b(c(x1622))) b(b(c(x1622))) -> c(c(c(x1622))) b(a(a(x1622))) -> c(c(a(x1622))) c(c(a(x1622))) -> c(c(c(x1622))) b(c(c(x1622))) -> a(b(c(x1622))) a(b(c(x1622))) -> a(b(a(x1622))) b(a(a(x1622))) -> a(b(a(x1622))) b(c(c(x1622))) -> a(b(c(x1622))) a(b(c(x1622))) -> a(b(a(x1622))) b(a(a(x1622))) -> c(c(a(x1622))) c(c(a(x1622))) -> a(b(a(x1622))) b(c(c(x1622))) -> a(b(c(x1622))) a(b(c(x1622))) -> a(a(b(x1622))) b(a(a(x1622))) -> a(b(a(x1622))) a(b(a(x1622))) -> a(a(b(x1622))) b(c(c(x1622))) -> a(b(c(x1622))) a(b(c(x1622))) -> a(c(c(x1622))) b(a(a(x1622))) -> a(b(a(x1622))) a(b(a(x1622))) -> a(c(c(x1622))) b(c(c(x1622))) -> c(c(c(x1622))) c(c(c(x1622))) -> c(a(b(x1622))) b(a(a(x1622))) -> c(c(a(x1622))) c(c(a(x1622))) -> c(a(b(x1622))) a(c(a(x1623))) -> a(c(c(x1623))) a(c(a(x1623))) -> c(c(a(x1623))) a(c(c(x1623))) -> c(c(c(x1623))) c(c(a(x1623))) -> c(c(c(x1623))) c(c(a(x1624))) -> c(c(c(x1624))) c(c(a(x1624))) -> a(b(a(x1624))) a(b(a(x1624))) -> a(c(c(x1624))) a(c(c(x1624))) -> c(c(c(x1624))) c(c(c(x1624))) -> a(b(c(x1624))) a(b(a(x1624))) -> a(c(c(x1624))) a(c(c(x1624))) -> a(b(c(x1624))) c(c(c(x1624))) -> a(b(c(x1624))) a(b(c(x1624))) -> a(b(a(x1624))) c(c(c(x1624))) -> a(b(c(x1624))) a(b(c(x1624))) -> a(a(b(x1624))) a(b(a(x1624))) -> a(a(b(x1624))) c(c(c(x1624))) -> a(b(c(x1624))) a(b(c(x1624))) -> a(a(b(x1624))) a(b(a(x1624))) -> a(c(c(x1624))) a(c(c(x1624))) -> a(a(b(x1624))) c(c(c(x1624))) -> a(b(c(x1624))) a(b(c(x1624))) -> a(c(c(x1624))) a(b(a(x1624))) -> a(c(c(x1624))) b(c(a(x1625))) -> b(c(c(x1625))) b(c(a(x1625))) -> a(b(a(x1625))) b(c(c(x1625))) -> a(b(c(x1625))) a(b(a(x1625))) -> a(c(c(x1625))) a(c(c(x1625))) -> a(b(c(x1625))) b(c(c(x1625))) -> b(a(c(x1625))) b(a(c(x1625))) -> a(b(c(x1625))) a(b(a(x1625))) -> a(c(c(x1625))) a(c(c(x1625))) -> a(b(c(x1625))) b(c(c(x1625))) -> b(b(c(x1625))) b(b(c(x1625))) -> a(b(c(x1625))) a(b(a(x1625))) -> a(c(c(x1625))) a(c(c(x1625))) -> a(b(c(x1625))) b(c(c(x1625))) -> c(c(c(x1625))) c(c(c(x1625))) -> a(b(c(x1625))) a(b(a(x1625))) -> a(c(c(x1625))) a(c(c(x1625))) -> a(b(c(x1625))) b(c(c(x1625))) -> c(c(c(x1625))) a(b(a(x1625))) -> a(c(c(x1625))) a(c(c(x1625))) -> c(c(c(x1625))) b(c(c(x1625))) -> b(a(c(x1625))) b(a(c(x1625))) -> c(c(c(x1625))) a(b(a(x1625))) -> a(c(c(x1625))) a(c(c(x1625))) -> c(c(c(x1625))) b(c(c(x1625))) -> b(b(c(x1625))) b(b(c(x1625))) -> c(c(c(x1625))) a(b(a(x1625))) -> a(c(c(x1625))) a(c(c(x1625))) -> c(c(c(x1625))) b(c(c(x1625))) -> a(b(c(x1625))) a(b(c(x1625))) -> a(b(a(x1625))) b(c(c(x1625))) -> a(b(c(x1625))) a(b(c(x1625))) -> a(a(b(x1625))) a(b(a(x1625))) -> a(a(b(x1625))) b(c(c(x1625))) -> a(b(c(x1625))) a(b(c(x1625))) -> a(a(b(x1625))) a(b(a(x1625))) -> a(c(c(x1625))) a(c(c(x1625))) -> a(a(b(x1625))) b(c(c(x1625))) -> a(b(c(x1625))) a(b(c(x1625))) -> a(c(c(x1625))) a(b(a(x1625))) -> a(c(c(x1625))) a(c(a(x1626))) -> a(c(c(x1626))) a(c(a(x1626))) -> a(b(a(x1626))) a(b(a(x1626))) -> a(c(c(x1626))) a(c(c(x1626))) -> a(a(b(x1626))) a(b(a(x1626))) -> a(a(b(x1626))) b(c(a(x1627))) -> b(c(c(x1627))) b(c(a(x1627))) -> b(b(a(x1627))) b(b(a(x1627))) -> b(c(c(x1627))) b(c(c(x1627))) -> b(a(b(x1627))) b(b(a(x1627))) -> b(a(b(x1627))) a(c(a(x1628))) -> a(c(c(x1628))) a(c(a(x1628))) -> c(a(a(x1628))) c(a(a(x1628))) -> a(b(a(x1628))) a(b(a(x1628))) -> a(c(c(x1628))) a(c(c(x1628))) -> c(c(c(x1628))) c(a(a(x1628))) -> c(c(a(x1628))) c(c(a(x1628))) -> c(c(c(x1628))) a(c(c(x1628))) -> c(a(c(x1628))) c(a(c(x1628))) -> c(c(c(x1628))) c(a(a(x1628))) -> c(c(a(x1628))) c(c(a(x1628))) -> c(c(c(x1628))) a(c(c(x1628))) -> a(a(b(x1628))) c(a(a(x1628))) -> a(b(a(x1628))) a(b(a(x1628))) -> a(a(b(x1628))) a(c(c(x1628))) -> a(b(c(x1628))) a(b(c(x1628))) -> a(a(b(x1628))) c(a(a(x1628))) -> a(b(a(x1628))) a(b(a(x1628))) -> a(a(b(x1628))) a(c(c(x1628))) -> c(c(c(x1628))) c(c(c(x1628))) -> c(a(b(x1628))) c(a(a(x1628))) -> c(c(a(x1628))) c(c(a(x1628))) -> c(a(b(x1628))) a(c(c(x1628))) -> c(a(c(x1628))) c(a(c(x1628))) -> c(a(b(x1628))) c(a(a(x1628))) -> c(c(a(x1628))) c(c(a(x1628))) -> c(a(b(x1628))) a(c(c(x1628))) -> a(b(c(x1628))) a(b(c(x1628))) -> a(b(a(x1628))) c(a(a(x1628))) -> a(b(a(x1628))) a(c(c(x1628))) -> a(b(c(x1628))) a(b(c(x1628))) -> a(b(a(x1628))) c(a(a(x1628))) -> c(c(a(x1628))) c(c(a(x1628))) -> a(b(a(x1628))) a(c(c(x1628))) -> c(a(c(x1628))) c(a(c(x1628))) -> c(c(a(x1628))) c(a(a(x1628))) -> c(c(a(x1628))) b(c(a(x1629))) -> b(c(c(x1629))) b(c(a(x1629))) -> c(c(a(x1629))) b(c(c(x1629))) -> c(c(c(x1629))) c(c(a(x1629))) -> c(c(c(x1629))) c(b(c(x1630))) -> c(a(b(x1630))) c(b(c(x1630))) -> a(b(c(x1630))) c(a(b(x1630))) -> a(b(b(x1630))) a(b(c(x1630))) -> a(b(b(x1630))) c(b(c(x1631))) -> c(a(b(x1631))) c(b(c(x1631))) -> c(a(c(x1631))) c(a(c(x1631))) -> c(a(b(x1631))) b(c(x)) -> a(b(x)) b(c(x)) -> b(a(x)) b(a(x)) -> a(b(x)) b(b(c(x1633))) -> b(a(b(x1633))) b(b(c(x1633))) -> c(c(c(x1633))) b(a(b(x1633))) -> a(b(b(x1633))) c(c(c(x1633))) -> c(a(b(x1633))) c(a(b(x1633))) -> a(b(b(x1633))) b(a(b(x1633))) -> a(b(b(x1633))) c(c(c(x1633))) -> a(b(c(x1633))) a(b(c(x1633))) -> a(b(b(x1633))) b(a(b(x1633))) -> c(c(b(x1633))) c(c(b(x1633))) -> a(b(b(x1633))) c(c(c(x1633))) -> c(a(b(x1633))) c(a(b(x1633))) -> a(b(b(x1633))) b(a(b(x1633))) -> c(c(b(x1633))) c(c(b(x1633))) -> a(b(b(x1633))) c(c(c(x1633))) -> a(b(c(x1633))) a(b(c(x1633))) -> a(b(b(x1633))) b(a(b(x1633))) -> c(c(b(x1633))) c(c(c(x1633))) -> c(a(b(x1633))) c(a(b(x1633))) -> c(c(b(x1633))) b(a(b(x1633))) -> a(b(b(x1633))) a(b(b(x1633))) -> a(c(c(x1633))) c(c(c(x1633))) -> a(b(c(x1633))) a(b(c(x1633))) -> a(c(c(x1633))) b(a(b(x1633))) -> a(b(b(x1633))) a(b(b(x1633))) -> a(b(a(x1633))) c(c(c(x1633))) -> a(b(c(x1633))) a(b(c(x1633))) -> a(b(a(x1633))) b(a(b(x1633))) -> a(b(b(x1633))) a(b(b(x1633))) -> a(a(b(x1633))) c(c(c(x1633))) -> a(b(c(x1633))) a(b(c(x1633))) -> a(a(b(x1633))) b(a(b(x1633))) -> c(c(b(x1633))) c(c(b(x1633))) -> c(a(b(x1633))) c(c(c(x1633))) -> c(a(b(x1633))) b(a(b(x1633))) -> c(c(b(x1633))) c(c(b(x1633))) -> c(c(c(x1633))) c(b(c(x1634))) -> c(a(b(x1634))) c(b(c(x1634))) -> a(c(c(x1634))) a(c(c(x1634))) -> c(c(c(x1634))) c(c(c(x1634))) -> c(a(b(x1634))) a(c(c(x1634))) -> c(a(c(x1634))) c(a(c(x1634))) -> c(a(b(x1634))) c(a(b(x1634))) -> a(b(b(x1634))) a(c(c(x1634))) -> a(b(c(x1634))) a(b(c(x1634))) -> a(b(b(x1634))) c(a(b(x1634))) -> c(c(b(x1634))) c(c(b(x1634))) -> a(b(b(x1634))) a(c(c(x1634))) -> a(b(c(x1634))) a(b(c(x1634))) -> a(b(b(x1634))) c(a(b(x1634))) -> a(b(b(x1634))) a(b(b(x1634))) -> a(c(c(x1634))) c(a(b(x1634))) -> a(b(b(x1634))) a(b(b(x1634))) -> a(b(a(x1634))) a(c(c(x1634))) -> a(b(c(x1634))) a(b(c(x1634))) -> a(b(a(x1634))) c(a(b(x1634))) -> a(b(b(x1634))) a(b(b(x1634))) -> a(a(b(x1634))) a(c(c(x1634))) -> a(a(b(x1634))) c(a(b(x1634))) -> a(b(b(x1634))) a(b(b(x1634))) -> a(a(b(x1634))) a(c(c(x1634))) -> a(b(c(x1634))) a(b(c(x1634))) -> a(a(b(x1634))) c(a(b(x1634))) -> c(c(b(x1634))) c(c(b(x1634))) -> c(c(a(x1634))) a(c(c(x1634))) -> c(a(c(x1634))) c(a(c(x1634))) -> c(c(a(x1634))) c(a(b(x1634))) -> c(c(b(x1634))) c(c(b(x1634))) -> c(a(c(x1634))) a(c(c(x1634))) -> c(a(c(x1634))) c(a(b(x1634))) -> c(c(b(x1634))) c(c(b(x1634))) -> c(c(c(x1634))) a(c(c(x1634))) -> c(c(c(x1634))) c(a(b(x1634))) -> c(c(b(x1634))) c(c(b(x1634))) -> c(c(c(x1634))) a(c(c(x1634))) -> c(a(c(x1634))) c(a(c(x1634))) -> c(c(c(x1634))) b(c(x)) -> a(b(x)) b(c(x)) -> b(b(x)) b(b(x)) -> a(b(x)) b(b(c(x1636))) -> b(a(b(x1636))) b(b(c(x1636))) -> b(a(c(x1636))) b(a(c(x1636))) -> b(a(b(x1636))) c(b(c(x1637))) -> c(a(b(x1637))) c(b(c(x1637))) -> c(c(c(x1637))) c(c(c(x1637))) -> c(a(b(x1637))) b(c(x)) -> a(b(x)) b(c(x)) -> c(c(x)) c(c(x)) -> a(b(x)) b(b(c(x1639))) -> b(a(b(x1639))) b(b(c(x1639))) -> a(b(c(x1639))) b(a(b(x1639))) -> a(b(b(x1639))) a(b(c(x1639))) -> a(b(b(x1639))) b(a(c(x1640))) -> b(a(b(x1640))) b(a(c(x1640))) -> a(b(c(x1640))) b(a(b(x1640))) -> a(b(b(x1640))) a(b(c(x1640))) -> a(b(b(x1640))) c(a(c(x1641))) -> c(a(b(x1641))) c(a(c(x1641))) -> a(b(c(x1641))) c(a(b(x1641))) -> a(b(b(x1641))) a(b(c(x1641))) -> a(b(b(x1641))) a(c(x)) -> a(b(x)) a(c(x)) -> c(c(x)) c(c(x)) -> a(b(x)) b(a(c(x1643))) -> b(a(b(x1643))) b(a(c(x1643))) -> c(c(c(x1643))) b(a(b(x1643))) -> a(b(b(x1643))) c(c(c(x1643))) -> c(a(b(x1643))) c(a(b(x1643))) -> a(b(b(x1643))) b(a(b(x1643))) -> a(b(b(x1643))) c(c(c(x1643))) -> a(b(c(x1643))) a(b(c(x1643))) -> a(b(b(x1643))) b(a(b(x1643))) -> c(c(b(x1643))) c(c(b(x1643))) -> a(b(b(x1643))) c(c(c(x1643))) -> c(a(b(x1643))) c(a(b(x1643))) -> a(b(b(x1643))) b(a(b(x1643))) -> c(c(b(x1643))) c(c(b(x1643))) -> a(b(b(x1643))) c(c(c(x1643))) -> a(b(c(x1643))) a(b(c(x1643))) -> a(b(b(x1643))) b(a(b(x1643))) -> c(c(b(x1643))) c(c(c(x1643))) -> c(a(b(x1643))) c(a(b(x1643))) -> c(c(b(x1643))) b(a(b(x1643))) -> a(b(b(x1643))) a(b(b(x1643))) -> a(c(c(x1643))) c(c(c(x1643))) -> a(b(c(x1643))) a(b(c(x1643))) -> a(c(c(x1643))) b(a(b(x1643))) -> a(b(b(x1643))) a(b(b(x1643))) -> a(b(a(x1643))) c(c(c(x1643))) -> a(b(c(x1643))) a(b(c(x1643))) -> a(b(a(x1643))) b(a(b(x1643))) -> a(b(b(x1643))) a(b(b(x1643))) -> a(a(b(x1643))) c(c(c(x1643))) -> a(b(c(x1643))) a(b(c(x1643))) -> a(a(b(x1643))) b(a(b(x1643))) -> c(c(b(x1643))) c(c(b(x1643))) -> c(a(b(x1643))) c(c(c(x1643))) -> c(a(b(x1643))) b(a(b(x1643))) -> c(c(b(x1643))) c(c(b(x1643))) -> c(c(c(x1643))) c(a(c(x1644))) -> c(a(b(x1644))) c(a(c(x1644))) -> c(c(c(x1644))) c(c(c(x1644))) -> c(a(b(x1644))) a(c(x)) -> a(b(x)) a(c(x)) -> c(a(x)) c(a(x)) -> a(b(x)) c(b(x)) -> a(c(x)) c(b(x)) -> a(b(x)) a(c(x)) -> a(b(x)) c(b(x)) -> a(c(x)) c(b(x)) -> c(a(x)) a(c(x)) -> c(c(x)) c(a(x)) -> c(c(x)) a(c(x)) -> a(b(x)) c(a(x)) -> a(b(x)) a(c(x)) -> c(a(x)) b(c(b(x1648))) -> b(a(c(x1648))) b(c(b(x1648))) -> b(a(b(x1648))) b(a(c(x1648))) -> b(a(b(x1648))) a(c(b(x1649))) -> a(a(c(x1649))) a(c(b(x1649))) -> c(c(b(x1649))) a(a(c(x1649))) -> a(c(c(x1649))) c(c(b(x1649))) -> a(b(b(x1649))) a(b(b(x1649))) -> a(c(c(x1649))) a(a(c(x1649))) -> a(c(a(x1649))) a(c(a(x1649))) -> a(c(c(x1649))) c(c(b(x1649))) -> a(b(b(x1649))) a(b(b(x1649))) -> a(c(c(x1649))) a(a(c(x1649))) -> a(a(b(x1649))) c(c(b(x1649))) -> a(b(b(x1649))) a(b(b(x1649))) -> a(a(b(x1649))) a(a(c(x1649))) -> a(c(c(x1649))) a(c(c(x1649))) -> a(a(b(x1649))) c(c(b(x1649))) -> a(b(b(x1649))) a(b(b(x1649))) -> a(a(b(x1649))) a(a(c(x1649))) -> a(c(a(x1649))) a(c(a(x1649))) -> a(a(b(x1649))) c(c(b(x1649))) -> a(b(b(x1649))) a(b(b(x1649))) -> a(a(b(x1649))) a(a(c(x1649))) -> a(c(c(x1649))) a(c(c(x1649))) -> c(c(c(x1649))) c(c(b(x1649))) -> c(c(c(x1649))) a(a(c(x1649))) -> a(c(c(x1649))) a(c(c(x1649))) -> c(c(c(x1649))) c(c(b(x1649))) -> c(c(a(x1649))) c(c(a(x1649))) -> c(c(c(x1649))) a(a(c(x1649))) -> a(c(c(x1649))) a(c(c(x1649))) -> c(c(c(x1649))) c(c(b(x1649))) -> c(a(c(x1649))) c(a(c(x1649))) -> c(c(c(x1649))) a(a(c(x1649))) -> a(c(c(x1649))) a(c(c(x1649))) -> a(b(c(x1649))) c(c(b(x1649))) -> c(a(c(x1649))) c(a(c(x1649))) -> a(b(c(x1649))) a(a(c(x1649))) -> a(c(c(x1649))) a(c(c(x1649))) -> a(b(c(x1649))) c(c(b(x1649))) -> c(c(c(x1649))) c(c(c(x1649))) -> a(b(c(x1649))) a(a(c(x1649))) -> a(c(c(x1649))) a(c(c(x1649))) -> c(a(c(x1649))) c(c(b(x1649))) -> c(a(c(x1649))) a(a(c(x1649))) -> a(c(a(x1649))) a(c(a(x1649))) -> c(c(a(x1649))) c(c(b(x1649))) -> c(c(a(x1649))) a(a(c(x1649))) -> a(c(a(x1649))) a(c(a(x1649))) -> c(c(a(x1649))) c(c(b(x1649))) -> c(a(c(x1649))) c(a(c(x1649))) -> c(c(a(x1649))) a(a(c(x1649))) -> a(c(a(x1649))) a(c(a(x1649))) -> a(b(a(x1649))) c(c(b(x1649))) -> c(c(a(x1649))) c(c(a(x1649))) -> a(b(a(x1649))) a(a(c(x1649))) -> a(c(a(x1649))) a(c(a(x1649))) -> a(b(a(x1649))) c(c(b(x1649))) -> a(b(b(x1649))) a(b(b(x1649))) -> a(b(a(x1649))) c(c(b(x1650))) -> c(a(c(x1650))) c(c(b(x1650))) -> a(b(b(x1650))) a(b(b(x1650))) -> a(c(c(x1650))) a(c(c(x1650))) -> c(a(c(x1650))) c(a(c(x1650))) -> a(b(c(x1650))) a(b(b(x1650))) -> a(c(c(x1650))) a(c(c(x1650))) -> a(b(c(x1650))) c(a(c(x1650))) -> c(c(c(x1650))) c(c(c(x1650))) -> a(b(c(x1650))) a(b(b(x1650))) -> a(c(c(x1650))) a(c(c(x1650))) -> a(b(c(x1650))) c(a(c(x1650))) -> c(c(c(x1650))) a(b(b(x1650))) -> a(c(c(x1650))) a(c(c(x1650))) -> c(c(c(x1650))) c(a(c(x1650))) -> c(c(a(x1650))) c(c(a(x1650))) -> c(c(c(x1650))) a(b(b(x1650))) -> a(c(c(x1650))) a(c(c(x1650))) -> c(c(c(x1650))) c(a(c(x1650))) -> a(b(c(x1650))) a(b(c(x1650))) -> a(b(a(x1650))) a(b(b(x1650))) -> a(b(a(x1650))) c(a(c(x1650))) -> c(c(a(x1650))) c(c(a(x1650))) -> a(b(a(x1650))) a(b(b(x1650))) -> a(b(a(x1650))) c(a(c(x1650))) -> a(b(c(x1650))) a(b(c(x1650))) -> a(a(b(x1650))) a(b(b(x1650))) -> a(a(b(x1650))) c(a(c(x1650))) -> a(b(c(x1650))) a(b(c(x1650))) -> a(a(b(x1650))) a(b(b(x1650))) -> a(c(c(x1650))) a(c(c(x1650))) -> a(a(b(x1650))) c(a(c(x1650))) -> a(b(c(x1650))) a(b(c(x1650))) -> a(a(b(x1650))) a(b(b(x1650))) -> a(b(a(x1650))) a(b(a(x1650))) -> a(a(b(x1650))) c(a(c(x1650))) -> a(b(c(x1650))) a(b(c(x1650))) -> a(b(b(x1650))) c(a(c(x1650))) -> c(a(b(x1650))) c(a(b(x1650))) -> a(b(b(x1650))) c(a(c(x1650))) -> a(b(c(x1650))) a(b(c(x1650))) -> a(c(c(x1650))) a(b(b(x1650))) -> a(c(c(x1650))) c(a(c(x1650))) -> a(b(c(x1650))) a(b(c(x1650))) -> a(c(c(x1650))) a(b(b(x1650))) -> a(b(a(x1650))) a(b(a(x1650))) -> a(c(c(x1650))) b(c(b(x1651))) -> b(a(c(x1651))) b(c(b(x1651))) -> a(b(b(x1651))) b(a(c(x1651))) -> a(b(c(x1651))) a(b(b(x1651))) -> a(c(c(x1651))) a(c(c(x1651))) -> a(b(c(x1651))) b(a(c(x1651))) -> b(c(c(x1651))) b(c(c(x1651))) -> a(b(c(x1651))) a(b(b(x1651))) -> a(c(c(x1651))) a(c(c(x1651))) -> a(b(c(x1651))) b(a(c(x1651))) -> c(c(c(x1651))) c(c(c(x1651))) -> a(b(c(x1651))) a(b(b(x1651))) -> a(c(c(x1651))) a(c(c(x1651))) -> a(b(c(x1651))) b(a(c(x1651))) -> c(c(c(x1651))) a(b(b(x1651))) -> a(c(c(x1651))) a(c(c(x1651))) -> c(c(c(x1651))) b(a(c(x1651))) -> b(c(c(x1651))) b(c(c(x1651))) -> c(c(c(x1651))) a(b(b(x1651))) -> a(c(c(x1651))) a(c(c(x1651))) -> c(c(c(x1651))) b(a(c(x1651))) -> a(b(c(x1651))) a(b(c(x1651))) -> a(b(a(x1651))) a(b(b(x1651))) -> a(b(a(x1651))) b(a(c(x1651))) -> b(c(a(x1651))) b(c(a(x1651))) -> a(b(a(x1651))) a(b(b(x1651))) -> a(b(a(x1651))) b(a(c(x1651))) -> a(b(c(x1651))) a(b(c(x1651))) -> a(a(b(x1651))) a(b(b(x1651))) -> a(a(b(x1651))) b(a(c(x1651))) -> a(b(c(x1651))) a(b(c(x1651))) -> a(a(b(x1651))) a(b(b(x1651))) -> a(c(c(x1651))) a(c(c(x1651))) -> a(a(b(x1651))) b(a(c(x1651))) -> a(b(c(x1651))) a(b(c(x1651))) -> a(a(b(x1651))) a(b(b(x1651))) -> a(b(a(x1651))) a(b(a(x1651))) -> a(a(b(x1651))) b(a(c(x1651))) -> a(b(c(x1651))) a(b(c(x1651))) -> a(b(b(x1651))) b(a(c(x1651))) -> b(a(b(x1651))) b(a(b(x1651))) -> a(b(b(x1651))) b(a(c(x1651))) -> a(b(c(x1651))) a(b(c(x1651))) -> a(c(c(x1651))) a(b(b(x1651))) -> a(c(c(x1651))) b(a(c(x1651))) -> a(b(c(x1651))) a(b(c(x1651))) -> a(c(c(x1651))) a(b(b(x1651))) -> a(b(a(x1651))) a(b(a(x1651))) -> a(c(c(x1651))) a(c(b(x1652))) -> a(a(c(x1652))) a(c(b(x1652))) -> a(b(b(x1652))) a(a(c(x1652))) -> a(c(c(x1652))) a(b(b(x1652))) -> a(c(c(x1652))) a(a(c(x1652))) -> a(a(b(x1652))) a(b(b(x1652))) -> a(a(b(x1652))) b(c(b(x1653))) -> b(a(c(x1653))) b(c(b(x1653))) -> b(b(b(x1653))) b(a(c(x1653))) -> b(c(c(x1653))) b(b(b(x1653))) -> b(c(c(x1653))) b(a(c(x1653))) -> b(a(b(x1653))) b(b(b(x1653))) -> b(a(b(x1653))) a(c(b(x1654))) -> a(a(c(x1654))) a(c(b(x1654))) -> c(a(b(x1654))) a(a(c(x1654))) -> a(c(c(x1654))) c(a(b(x1654))) -> a(b(b(x1654))) a(b(b(x1654))) -> a(c(c(x1654))) a(a(c(x1654))) -> a(c(a(x1654))) a(c(a(x1654))) -> a(c(c(x1654))) c(a(b(x1654))) -> a(b(b(x1654))) a(b(b(x1654))) -> a(c(c(x1654))) a(a(c(x1654))) -> a(a(b(x1654))) c(a(b(x1654))) -> a(b(b(x1654))) a(b(b(x1654))) -> a(a(b(x1654))) a(a(c(x1654))) -> a(c(c(x1654))) a(c(c(x1654))) -> a(a(b(x1654))) c(a(b(x1654))) -> a(b(b(x1654))) a(b(b(x1654))) -> a(a(b(x1654))) a(a(c(x1654))) -> a(c(a(x1654))) a(c(a(x1654))) -> a(a(b(x1654))) c(a(b(x1654))) -> a(b(b(x1654))) a(b(b(x1654))) -> a(a(b(x1654))) a(a(c(x1654))) -> a(c(c(x1654))) a(c(c(x1654))) -> c(c(c(x1654))) c(a(b(x1654))) -> c(c(b(x1654))) c(c(b(x1654))) -> c(c(c(x1654))) a(a(c(x1654))) -> a(c(c(x1654))) a(c(c(x1654))) -> c(a(c(x1654))) c(a(b(x1654))) -> c(c(b(x1654))) c(c(b(x1654))) -> c(a(c(x1654))) a(a(c(x1654))) -> a(c(a(x1654))) a(c(a(x1654))) -> c(c(a(x1654))) c(a(b(x1654))) -> c(c(b(x1654))) c(c(b(x1654))) -> c(c(a(x1654))) a(a(c(x1654))) -> a(c(a(x1654))) a(c(a(x1654))) -> a(b(a(x1654))) c(a(b(x1654))) -> a(b(b(x1654))) a(b(b(x1654))) -> a(b(a(x1654))) c(b(x)) -> a(c(x)) c(b(x)) -> c(c(x)) a(c(x)) -> c(c(x)) a(c(x)) -> a(b(x)) c(c(x)) -> a(b(x)) b(c(b(x1656))) -> b(a(c(x1656))) b(c(b(x1656))) -> c(c(b(x1656))) b(a(c(x1656))) -> c(c(c(x1656))) c(c(b(x1656))) -> c(c(c(x1656))) c(b(c(x1657))) -> c(b(b(x1657))) c(b(c(x1657))) -> a(b(c(x1657))) c(b(b(x1657))) -> a(b(b(x1657))) a(b(c(x1657))) -> a(b(b(x1657))) c(b(c(x1658))) -> c(b(b(x1658))) c(b(c(x1658))) -> c(a(c(x1658))) c(b(b(x1658))) -> c(a(b(x1658))) c(a(c(x1658))) -> c(a(b(x1658))) c(b(b(x1658))) -> c(c(c(x1658))) c(a(c(x1658))) -> c(c(c(x1658))) b(c(x)) -> b(b(x)) b(c(x)) -> b(a(x)) b(b(x)) -> c(c(x)) b(a(x)) -> c(c(x)) b(b(x)) -> b(a(x)) b(b(x)) -> a(b(x)) b(a(x)) -> a(b(x)) b(b(c(x1660))) -> b(b(b(x1660))) b(b(c(x1660))) -> c(c(c(x1660))) b(b(b(x1660))) -> c(c(b(x1660))) c(c(c(x1660))) -> c(a(b(x1660))) c(a(b(x1660))) -> c(c(b(x1660))) b(b(b(x1660))) -> b(a(b(x1660))) b(a(b(x1660))) -> c(c(b(x1660))) c(c(c(x1660))) -> c(a(b(x1660))) c(a(b(x1660))) -> c(c(b(x1660))) b(b(b(x1660))) -> a(b(b(x1660))) c(c(c(x1660))) -> c(a(b(x1660))) c(a(b(x1660))) -> a(b(b(x1660))) b(b(b(x1660))) -> a(b(b(x1660))) c(c(c(x1660))) -> a(b(c(x1660))) a(b(c(x1660))) -> a(b(b(x1660))) b(b(b(x1660))) -> c(c(b(x1660))) c(c(b(x1660))) -> a(b(b(x1660))) c(c(c(x1660))) -> c(a(b(x1660))) c(a(b(x1660))) -> a(b(b(x1660))) b(b(b(x1660))) -> c(c(b(x1660))) c(c(b(x1660))) -> a(b(b(x1660))) c(c(c(x1660))) -> a(b(c(x1660))) a(b(c(x1660))) -> a(b(b(x1660))) b(b(b(x1660))) -> b(a(b(x1660))) b(a(b(x1660))) -> a(b(b(x1660))) c(c(c(x1660))) -> c(a(b(x1660))) c(a(b(x1660))) -> a(b(b(x1660))) b(b(b(x1660))) -> b(a(b(x1660))) b(a(b(x1660))) -> a(b(b(x1660))) c(c(c(x1660))) -> a(b(c(x1660))) a(b(c(x1660))) -> a(b(b(x1660))) b(b(b(x1660))) -> b(c(c(x1660))) b(c(c(x1660))) -> a(b(c(x1660))) c(c(c(x1660))) -> a(b(c(x1660))) b(b(b(x1660))) -> b(c(c(x1660))) b(c(c(x1660))) -> c(c(c(x1660))) b(b(b(x1660))) -> c(c(b(x1660))) c(c(b(x1660))) -> c(c(c(x1660))) b(b(b(x1660))) -> c(c(b(x1660))) c(c(b(x1660))) -> c(a(b(x1660))) c(c(c(x1660))) -> c(a(b(x1660))) b(b(b(x1660))) -> b(b(a(x1660))) b(b(a(x1660))) -> a(b(a(x1660))) c(c(c(x1660))) -> a(b(c(x1660))) a(b(c(x1660))) -> a(b(a(x1660))) b(b(b(x1660))) -> a(b(b(x1660))) a(b(b(x1660))) -> a(b(a(x1660))) c(c(c(x1660))) -> a(b(c(x1660))) a(b(c(x1660))) -> a(b(a(x1660))) b(b(b(x1660))) -> a(b(b(x1660))) a(b(b(x1660))) -> a(c(c(x1660))) c(c(c(x1660))) -> a(b(c(x1660))) a(b(c(x1660))) -> a(c(c(x1660))) b(b(b(x1660))) -> a(b(b(x1660))) a(b(b(x1660))) -> a(a(b(x1660))) c(c(c(x1660))) -> a(b(c(x1660))) a(b(c(x1660))) -> a(a(b(x1660))) b(c(x)) -> b(b(x)) b(c(x)) -> a(b(x)) b(b(x)) -> a(b(x)) c(b(c(x1662))) -> c(b(b(x1662))) c(b(c(x1662))) -> a(c(c(x1662))) c(b(b(x1662))) -> c(c(c(x1662))) a(c(c(x1662))) -> c(c(c(x1662))) b(b(c(x1663))) -> b(b(b(x1663))) b(b(c(x1663))) -> b(a(c(x1663))) b(b(b(x1663))) -> b(c(c(x1663))) b(a(c(x1663))) -> b(c(c(x1663))) b(b(b(x1663))) -> b(a(b(x1663))) b(a(c(x1663))) -> b(a(b(x1663))) c(b(c(x1664))) -> c(b(b(x1664))) c(b(c(x1664))) -> c(c(c(x1664))) c(b(b(x1664))) -> c(a(b(x1664))) c(c(c(x1664))) -> c(a(b(x1664))) c(b(b(x1664))) -> c(c(c(x1664))) b(c(x)) -> b(b(x)) b(c(x)) -> c(c(x)) b(b(x)) -> c(c(x)) b(b(x)) -> a(b(x)) c(c(x)) -> a(b(x)) b(b(c(x1666))) -> b(b(b(x1666))) b(b(c(x1666))) -> a(b(c(x1666))) b(b(b(x1666))) -> a(b(b(x1666))) a(b(c(x1666))) -> a(b(b(x1666))) c(b(b(x1667))) -> c(b(a(x1667))) c(b(b(x1667))) -> a(b(b(x1667))) c(b(a(x1667))) -> a(b(a(x1667))) a(b(b(x1667))) -> a(b(a(x1667))) c(b(b(x1668))) -> c(b(a(x1668))) c(b(b(x1668))) -> c(a(b(x1668))) c(b(a(x1668))) -> c(a(b(x1668))) b(b(x)) -> b(a(x)) b(b(x)) -> c(c(x)) b(a(x)) -> a(b(x)) c(c(x)) -> a(b(x)) b(a(x)) -> c(c(x)) b(b(b(x1670))) -> b(b(a(x1670))) b(b(b(x1670))) -> c(c(b(x1670))) b(b(a(x1670))) -> c(c(a(x1670))) c(c(b(x1670))) -> c(c(a(x1670))) c(b(b(x1671))) -> c(b(a(x1671))) c(b(b(x1671))) -> a(c(b(x1671))) c(b(a(x1671))) -> c(a(b(x1671))) a(c(b(x1671))) -> c(a(b(x1671))) c(b(a(x1671))) -> a(c(a(x1671))) a(c(b(x1671))) -> a(c(a(x1671))) b(b(b(x1672))) -> b(b(a(x1672))) b(b(b(x1672))) -> b(a(b(x1672))) b(b(a(x1672))) -> b(a(b(x1672))) c(b(b(x1673))) -> c(b(a(x1673))) c(b(b(x1673))) -> c(c(b(x1673))) c(b(a(x1673))) -> c(a(b(x1673))) c(c(b(x1673))) -> c(a(b(x1673))) c(b(a(x1673))) -> c(c(c(x1673))) c(c(b(x1673))) -> c(c(c(x1673))) c(b(a(x1673))) -> c(c(a(x1673))) c(c(b(x1673))) -> c(c(a(x1673))) b(b(x)) -> b(a(x)) b(b(x)) -> a(b(x)) b(a(x)) -> a(b(x)) b(b(b(x1675))) -> b(b(a(x1675))) b(b(b(x1675))) -> a(b(b(x1675))) b(b(a(x1675))) -> a(b(a(x1675))) a(b(b(x1675))) -> a(b(a(x1675))) b(a(c(x1676))) -> b(c(a(x1676))) b(a(c(x1676))) -> a(b(c(x1676))) b(c(a(x1676))) -> a(b(a(x1676))) a(b(c(x1676))) -> a(b(a(x1676))) c(a(c(x1677))) -> c(c(a(x1677))) c(a(c(x1677))) -> a(b(c(x1677))) c(c(a(x1677))) -> a(b(a(x1677))) a(b(c(x1677))) -> a(b(a(x1677))) a(c(x)) -> c(a(x)) a(c(x)) -> c(c(x)) c(a(x)) -> a(b(x)) c(c(x)) -> a(b(x)) c(a(x)) -> c(c(x)) b(a(c(x1679))) -> b(c(a(x1679))) b(a(c(x1679))) -> c(c(c(x1679))) b(c(a(x1679))) -> a(b(a(x1679))) c(c(c(x1679))) -> a(b(c(x1679))) a(b(c(x1679))) -> a(b(a(x1679))) b(c(a(x1679))) -> b(a(a(x1679))) b(a(a(x1679))) -> a(b(a(x1679))) c(c(c(x1679))) -> a(b(c(x1679))) a(b(c(x1679))) -> a(b(a(x1679))) b(c(a(x1679))) -> b(b(a(x1679))) b(b(a(x1679))) -> a(b(a(x1679))) c(c(c(x1679))) -> a(b(c(x1679))) a(b(c(x1679))) -> a(b(a(x1679))) b(c(a(x1679))) -> c(c(a(x1679))) c(c(a(x1679))) -> a(b(a(x1679))) c(c(c(x1679))) -> a(b(c(x1679))) a(b(c(x1679))) -> a(b(a(x1679))) b(c(a(x1679))) -> b(a(b(x1679))) b(a(b(x1679))) -> a(b(b(x1679))) c(c(c(x1679))) -> c(a(b(x1679))) c(a(b(x1679))) -> a(b(b(x1679))) b(c(a(x1679))) -> b(a(b(x1679))) b(a(b(x1679))) -> a(b(b(x1679))) c(c(c(x1679))) -> a(b(c(x1679))) a(b(c(x1679))) -> a(b(b(x1679))) b(c(a(x1679))) -> b(a(b(x1679))) b(a(b(x1679))) -> c(c(b(x1679))) c(c(c(x1679))) -> c(a(b(x1679))) c(a(b(x1679))) -> c(c(b(x1679))) b(c(a(x1679))) -> b(c(c(x1679))) b(c(c(x1679))) -> a(b(c(x1679))) c(c(c(x1679))) -> a(b(c(x1679))) b(c(a(x1679))) -> b(c(c(x1679))) b(c(c(x1679))) -> c(c(c(x1679))) b(c(a(x1679))) -> c(c(a(x1679))) c(c(a(x1679))) -> c(c(c(x1679))) b(c(a(x1679))) -> a(b(a(x1679))) a(b(a(x1679))) -> a(a(b(x1679))) c(c(c(x1679))) -> a(b(c(x1679))) a(b(c(x1679))) -> a(a(b(x1679))) b(c(a(x1679))) -> a(b(a(x1679))) a(b(a(x1679))) -> a(c(c(x1679))) c(c(c(x1679))) -> a(b(c(x1679))) a(b(c(x1679))) -> a(c(c(x1679))) b(c(a(x1679))) -> c(c(a(x1679))) c(c(a(x1679))) -> c(a(b(x1679))) c(c(c(x1679))) -> c(a(b(x1679))) c(a(c(x1680))) -> c(c(a(x1680))) c(a(c(x1680))) -> c(c(c(x1680))) c(c(a(x1680))) -> c(a(b(x1680))) c(c(c(x1680))) -> c(a(b(x1680))) c(c(a(x1680))) -> c(c(c(x1680))) a(c(x)) -> c(a(x)) a(c(x)) -> a(b(x)) c(a(x)) -> a(b(x)) c(b(x)) -> c(c(x)) c(b(x)) -> a(b(x)) c(c(x)) -> a(b(x)) c(b(x)) -> c(c(x)) c(b(x)) -> c(a(x)) c(a(x)) -> c(c(x)) c(c(x)) -> a(b(x)) c(a(x)) -> a(b(x)) b(c(b(x1684))) -> b(c(c(x1684))) b(c(b(x1684))) -> b(a(b(x1684))) b(c(c(x1684))) -> b(a(b(x1684))) a(c(b(x1685))) -> a(c(c(x1685))) a(c(b(x1685))) -> c(c(b(x1685))) a(c(c(x1685))) -> c(c(c(x1685))) c(c(b(x1685))) -> c(c(c(x1685))) a(c(c(x1685))) -> c(a(c(x1685))) c(c(b(x1685))) -> c(a(c(x1685))) c(c(b(x1686))) -> c(c(c(x1686))) c(c(b(x1686))) -> a(b(b(x1686))) a(b(b(x1686))) -> a(c(c(x1686))) a(c(c(x1686))) -> c(c(c(x1686))) c(c(c(x1686))) -> a(b(c(x1686))) a(b(b(x1686))) -> a(c(c(x1686))) a(c(c(x1686))) -> a(b(c(x1686))) c(c(c(x1686))) -> c(a(b(x1686))) c(a(b(x1686))) -> a(b(b(x1686))) c(c(c(x1686))) -> a(b(c(x1686))) a(b(c(x1686))) -> a(b(b(x1686))) c(c(c(x1686))) -> a(b(c(x1686))) a(b(c(x1686))) -> a(b(a(x1686))) a(b(b(x1686))) -> a(b(a(x1686))) c(c(c(x1686))) -> a(b(c(x1686))) a(b(c(x1686))) -> a(a(b(x1686))) a(b(b(x1686))) -> a(a(b(x1686))) c(c(c(x1686))) -> a(b(c(x1686))) a(b(c(x1686))) -> a(a(b(x1686))) a(b(b(x1686))) -> a(c(c(x1686))) a(c(c(x1686))) -> a(a(b(x1686))) c(c(c(x1686))) -> a(b(c(x1686))) a(b(c(x1686))) -> a(a(b(x1686))) a(b(b(x1686))) -> a(b(a(x1686))) a(b(a(x1686))) -> a(a(b(x1686))) c(c(c(x1686))) -> a(b(c(x1686))) a(b(c(x1686))) -> a(c(c(x1686))) a(b(b(x1686))) -> a(c(c(x1686))) c(c(c(x1686))) -> a(b(c(x1686))) a(b(c(x1686))) -> a(c(c(x1686))) a(b(b(x1686))) -> a(b(a(x1686))) a(b(a(x1686))) -> a(c(c(x1686))) b(c(b(x1687))) -> b(c(c(x1687))) b(c(b(x1687))) -> a(b(b(x1687))) b(c(c(x1687))) -> a(b(c(x1687))) a(b(b(x1687))) -> a(c(c(x1687))) a(c(c(x1687))) -> a(b(c(x1687))) b(c(c(x1687))) -> b(a(c(x1687))) b(a(c(x1687))) -> a(b(c(x1687))) a(b(b(x1687))) -> a(c(c(x1687))) a(c(c(x1687))) -> a(b(c(x1687))) b(c(c(x1687))) -> b(b(c(x1687))) b(b(c(x1687))) -> a(b(c(x1687))) a(b(b(x1687))) -> a(c(c(x1687))) a(c(c(x1687))) -> a(b(c(x1687))) b(c(c(x1687))) -> c(c(c(x1687))) c(c(c(x1687))) -> a(b(c(x1687))) a(b(b(x1687))) -> a(c(c(x1687))) a(c(c(x1687))) -> a(b(c(x1687))) b(c(c(x1687))) -> c(c(c(x1687))) a(b(b(x1687))) -> a(c(c(x1687))) a(c(c(x1687))) -> c(c(c(x1687))) b(c(c(x1687))) -> b(a(c(x1687))) b(a(c(x1687))) -> c(c(c(x1687))) a(b(b(x1687))) -> a(c(c(x1687))) a(c(c(x1687))) -> c(c(c(x1687))) b(c(c(x1687))) -> b(b(c(x1687))) b(b(c(x1687))) -> c(c(c(x1687))) a(b(b(x1687))) -> a(c(c(x1687))) a(c(c(x1687))) -> c(c(c(x1687))) b(c(c(x1687))) -> b(a(b(x1687))) b(a(b(x1687))) -> a(b(b(x1687))) b(c(c(x1687))) -> a(b(c(x1687))) a(b(c(x1687))) -> a(b(b(x1687))) b(c(c(x1687))) -> a(b(c(x1687))) a(b(c(x1687))) -> a(b(a(x1687))) a(b(b(x1687))) -> a(b(a(x1687))) b(c(c(x1687))) -> a(b(c(x1687))) a(b(c(x1687))) -> a(a(b(x1687))) a(b(b(x1687))) -> a(a(b(x1687))) b(c(c(x1687))) -> a(b(c(x1687))) a(b(c(x1687))) -> a(a(b(x1687))) a(b(b(x1687))) -> a(c(c(x1687))) a(c(c(x1687))) -> a(a(b(x1687))) b(c(c(x1687))) -> a(b(c(x1687))) a(b(c(x1687))) -> a(a(b(x1687))) a(b(b(x1687))) -> a(b(a(x1687))) a(b(a(x1687))) -> a(a(b(x1687))) b(c(c(x1687))) -> a(b(c(x1687))) a(b(c(x1687))) -> a(c(c(x1687))) a(b(b(x1687))) -> a(c(c(x1687))) b(c(c(x1687))) -> a(b(c(x1687))) a(b(c(x1687))) -> a(c(c(x1687))) a(b(b(x1687))) -> a(b(a(x1687))) a(b(a(x1687))) -> a(c(c(x1687))) a(c(b(x1688))) -> a(c(c(x1688))) a(c(b(x1688))) -> a(b(b(x1688))) a(b(b(x1688))) -> a(c(c(x1688))) a(c(c(x1688))) -> a(a(b(x1688))) a(b(b(x1688))) -> a(a(b(x1688))) c(b(x)) -> c(c(x)) c(b(x)) -> a(c(x)) a(c(x)) -> c(c(x)) c(c(x)) -> a(b(x)) a(c(x)) -> a(b(x)) b(c(b(x1690))) -> b(c(c(x1690))) b(c(b(x1690))) -> b(b(b(x1690))) b(b(b(x1690))) -> b(c(c(x1690))) b(c(c(x1690))) -> b(a(b(x1690))) b(b(b(x1690))) -> b(a(b(x1690))) a(c(b(x1691))) -> a(c(c(x1691))) a(c(b(x1691))) -> c(a(b(x1691))) c(a(b(x1691))) -> a(b(b(x1691))) a(b(b(x1691))) -> a(c(c(x1691))) a(c(c(x1691))) -> c(c(c(x1691))) c(a(b(x1691))) -> c(c(b(x1691))) c(c(b(x1691))) -> c(c(c(x1691))) a(c(c(x1691))) -> c(a(c(x1691))) c(a(c(x1691))) -> c(c(c(x1691))) c(a(b(x1691))) -> c(c(b(x1691))) c(c(b(x1691))) -> c(c(c(x1691))) a(c(c(x1691))) -> a(a(b(x1691))) c(a(b(x1691))) -> a(b(b(x1691))) a(b(b(x1691))) -> a(a(b(x1691))) a(c(c(x1691))) -> a(b(c(x1691))) a(b(c(x1691))) -> a(a(b(x1691))) c(a(b(x1691))) -> a(b(b(x1691))) a(b(b(x1691))) -> a(a(b(x1691))) a(c(c(x1691))) -> c(a(c(x1691))) c(a(b(x1691))) -> c(c(b(x1691))) c(c(b(x1691))) -> c(a(c(x1691))) a(c(c(x1691))) -> c(c(c(x1691))) c(c(c(x1691))) -> c(a(b(x1691))) a(c(c(x1691))) -> c(a(c(x1691))) c(a(c(x1691))) -> c(a(b(x1691))) a(c(c(x1691))) -> a(b(c(x1691))) a(b(c(x1691))) -> a(b(a(x1691))) c(a(b(x1691))) -> a(b(b(x1691))) a(b(b(x1691))) -> a(b(a(x1691))) a(c(c(x1691))) -> a(b(c(x1691))) a(b(c(x1691))) -> a(b(b(x1691))) c(a(b(x1691))) -> a(b(b(x1691))) a(c(c(x1691))) -> a(b(c(x1691))) a(b(c(x1691))) -> a(b(b(x1691))) c(a(b(x1691))) -> c(c(b(x1691))) c(c(b(x1691))) -> a(b(b(x1691))) a(c(c(x1691))) -> c(a(c(x1691))) c(a(c(x1691))) -> c(c(a(x1691))) c(a(b(x1691))) -> c(c(b(x1691))) c(c(b(x1691))) -> c(c(a(x1691))) b(c(b(x1692))) -> b(c(c(x1692))) b(c(b(x1692))) -> c(c(b(x1692))) b(c(c(x1692))) -> c(c(c(x1692))) c(c(b(x1692))) -> c(c(c(x1692))) c(b(c(x1693))) -> c(c(c(x1693))) c(b(c(x1693))) -> a(b(c(x1693))) c(c(c(x1693))) -> a(b(c(x1693))) c(b(c(x1694))) -> c(c(c(x1694))) c(b(c(x1694))) -> c(a(c(x1694))) c(a(c(x1694))) -> c(c(c(x1694))) c(c(c(x1694))) -> c(a(b(x1694))) c(a(c(x1694))) -> c(a(b(x1694))) c(c(c(x1694))) -> a(b(c(x1694))) c(a(c(x1694))) -> a(b(c(x1694))) b(c(x)) -> c(c(x)) b(c(x)) -> b(a(x)) b(a(x)) -> c(c(x)) c(c(x)) -> a(b(x)) b(a(x)) -> a(b(x)) b(b(c(x1696))) -> b(c(c(x1696))) b(b(c(x1696))) -> c(c(c(x1696))) b(c(c(x1696))) -> a(b(c(x1696))) c(c(c(x1696))) -> a(b(c(x1696))) b(c(c(x1696))) -> c(c(c(x1696))) b(c(x)) -> c(c(x)) b(c(x)) -> a(b(x)) c(c(x)) -> a(b(x)) c(b(c(x1698))) -> c(c(c(x1698))) c(b(c(x1698))) -> a(c(c(x1698))) a(c(c(x1698))) -> c(c(c(x1698))) c(c(c(x1698))) -> a(b(c(x1698))) a(c(c(x1698))) -> a(b(c(x1698))) b(c(x)) -> c(c(x)) b(c(x)) -> b(b(x)) b(b(x)) -> c(c(x)) c(c(x)) -> a(b(x)) b(b(x)) -> a(b(x)) b(b(c(x1700))) -> b(c(c(x1700))) b(b(c(x1700))) -> b(a(c(x1700))) b(a(c(x1700))) -> b(c(c(x1700))) b(c(c(x1700))) -> b(a(c(x1700))) b(c(c(x1700))) -> b(a(b(x1700))) b(a(c(x1700))) -> b(a(b(x1700))) b(c(c(x1700))) -> a(b(c(x1700))) b(a(c(x1700))) -> a(b(c(x1700))) b(c(c(x1700))) -> c(c(c(x1700))) b(a(c(x1700))) -> c(c(c(x1700))) c(b(c(x1701))) -> c(c(c(x1701))) c(b(c(x1701))) -> c(c(c(x1701))) b(b(c(x1702))) -> b(c(c(x1702))) b(b(c(x1702))) -> a(b(c(x1702))) b(c(c(x1702))) -> a(b(c(x1702))) c(b(b(x1703))) -> c(a(b(x1703))) c(b(b(x1703))) -> a(b(b(x1703))) c(a(b(x1703))) -> a(b(b(x1703))) c(b(b(x1704))) -> c(a(b(x1704))) c(b(b(x1704))) -> c(a(b(x1704))) b(b(x)) -> a(b(x)) b(b(x)) -> c(c(x)) c(c(x)) -> a(b(x)) b(b(b(x1706))) -> b(a(b(x1706))) b(b(b(x1706))) -> c(c(b(x1706))) b(a(b(x1706))) -> a(b(b(x1706))) c(c(b(x1706))) -> a(b(b(x1706))) b(a(b(x1706))) -> c(c(b(x1706))) c(b(b(x1707))) -> c(a(b(x1707))) c(b(b(x1707))) -> a(c(b(x1707))) a(c(b(x1707))) -> c(a(b(x1707))) c(a(b(x1707))) -> a(b(b(x1707))) a(c(b(x1707))) -> a(b(b(x1707))) c(a(b(x1707))) -> c(c(b(x1707))) a(c(b(x1707))) -> c(c(b(x1707))) b(b(x)) -> a(b(x)) b(b(x)) -> b(a(x)) b(a(x)) -> a(b(x)) b(b(b(x1709))) -> b(a(b(x1709))) b(b(b(x1709))) -> b(a(b(x1709))) c(b(b(x1710))) -> c(a(b(x1710))) c(b(b(x1710))) -> c(c(b(x1710))) c(c(b(x1710))) -> c(a(b(x1710))) c(a(b(x1710))) -> a(b(b(x1710))) c(c(b(x1710))) -> a(b(b(x1710))) c(a(b(x1710))) -> c(c(b(x1710))) b(b(b(x1711))) -> b(a(b(x1711))) b(b(b(x1711))) -> a(b(b(x1711))) b(a(b(x1711))) -> a(b(b(x1711))) weak: b(a(x)) -> a(b(x)) c(a(x)) -> a(b(x)) c(b(x)) -> a(b(x)) c(b(x)) -> c(a(x)) b(c(x)) -> b(a(x)) b(b(x)) -> c(c(x)) a(c(x)) -> c(c(x)) b(a(x)) -> c(c(x)) c(c(x)) -> a(b(x)) c(a(x)) -> c(c(x)) b(c(x)) -> a(b(x)) a(c(x)) -> a(b(x)) c(b(x)) -> a(c(x)) b(c(x)) -> b(b(x)) b(b(x)) -> b(a(x)) a(c(x)) -> c(a(x)) c(b(x)) -> c(c(x)) b(c(x)) -> c(c(x)) b(b(x)) -> a(b(x)) Shift Processor (ldh) lab=left (force): strict: weak: Rule Labeling Processor: strict: weak: rule labeling (right): b(a(x)) -> a(b(x)): 1 c(a(x)) -> a(b(x)): 1 c(b(x)) -> a(b(x)): 1 c(b(x)) -> c(a(x)): 2 b(c(x)) -> b(a(x)): 2 b(b(x)) -> c(c(x)): 0 a(c(x)) -> c(c(x)): 16 b(a(x)) -> c(c(x)): 0 c(c(x)) -> a(b(x)): 1 c(a(x)) -> c(c(x)): 0 b(c(x)) -> a(b(x)): 1 a(c(x)) -> a(b(x)): 1 c(b(x)) -> a(c(x)): 17 b(c(x)) -> b(b(x)): 1 b(b(x)) -> b(a(x)): 2 a(c(x)) -> c(a(x)): 3 c(b(x)) -> c(c(x)): 0 b(c(x)) -> c(c(x)): 0 b(b(x)) -> a(b(x)): 1 Decreasing Processor: The following diagrams are decreasing: peak: c(a(b(x1541))) <-0|0[==1,==1]- c(b(a(x1541))) -2|[==1,==1]-> a(b(a(x1541))) joins (1): c(a(b(x1541))) -1|[==1,==1]-> a(b(b(x1541))) -5|0[==1,>>0]-> a(c(c(x1541))) a(b(a(x1541))) -7|0[==1,>>0]-> a(c(c(x1541))) peak: c(a(b(x1542))) <-0|0[==1,=>1]- c(b(a(x1542))) -3|[==1,?=2]-> c(a(a(x1542))) joins (1): c(a(a(x1542))) -9|[==1,>>0]-> c(c(a(x1542))) -1|0[==1,=>1]-> c(a(b(x1542))) peak: b(a(b(x1543))) <-0|0[==1,=?1]- b(b(a(x1543))) -5|[==1,>=0]-> c(c(a(x1543))) joins (1): b(a(b(x1543))) -7|[==1,>=0]-> c(c(b(x1543))) c(c(a(x1543))) -1|0[==1,=?1]-> c(a(b(x1543))) -9|[==1,>=0]-> c(c(b(x1543))) peak: a(b(x)) <-0|[==1,=?1]- b(a(x)) -7|[==1,>=0]-> c(c(x)) joins (1): c(c(x)) -8|[==1,=?1]-> a(b(x)) peak: c(a(b(x1545))) <-0|0[==1,=>1]- c(b(a(x1545))) -12|[==1,?=17]-> a(c(a(x1545))) joins (1): a(c(a(x1545))) -6|[==1,?>16]-> c(c(a(x1545))) -1|0[==1,=>1]-> c(a(b(x1545))) peak: b(a(b(x1546))) <-0|0[==1,=>1]- b(b(a(x1546))) -14|[==1,?=2]-> b(a(a(x1546))) joins (1): b(a(b(x1546))) -7|[==1,>>0]-> c(c(b(x1546))) -3|0[==1,?=2]-> c(c(a(x1546))) b(a(a(x1546))) -7|[==1,>>0]-> c(c(a(x1546))) peak: c(a(b(x1547))) <-0|0[==1,=?1]- c(b(a(x1547))) -16|[==1,>=0]-> c(c(a(x1547))) joins (1): c(c(a(x1547))) -1|0[==1,=?1]-> c(a(b(x1547))) peak: b(a(b(x1548))) <-0|0[==1,==1]- b(b(a(x1548))) -18|[==1,==1]-> a(b(a(x1548))) joins (1): b(a(b(x1548))) -0|[==1,==1]-> a(b(b(x1548))) -5|0[==1,>>0]-> a(c(c(x1548))) a(b(a(x1548))) -7|0[==1,>>0]-> a(c(c(x1548))) peak: b(a(b(x1549))) <-1|0[==1,=>1]- b(c(a(x1549))) -4|[==1,?=2]-> b(a(a(x1549))) joins (1): b(a(b(x1549))) -7|[==1,>>0]-> c(c(b(x1549))) -3|0[==1,?=2]-> c(c(a(x1549))) b(a(a(x1549))) -7|[==1,>>0]-> c(c(a(x1549))) peak: a(a(b(x1550))) <-1|0[==1,=>1]- a(c(a(x1550))) -6|[==1,?=16]-> c(c(a(x1550))) joins (1): c(c(a(x1550))) -8|[==1,=>1]-> a(b(a(x1550))) -0|0[==1,=>1]-> a(a(b(x1550))) peak: c(a(b(x1551))) <-1|0[==1,==1]- c(c(a(x1551))) -8|[==1,==1]-> a(b(a(x1551))) joins (1): c(a(b(x1551))) -1|[==1,==1]-> a(b(b(x1551))) -5|0[==1,>>0]-> a(c(c(x1551))) a(b(a(x1551))) -7|0[==1,>>0]-> a(c(c(x1551))) peak: a(b(x)) <-1|[==1,=?1]- c(a(x)) -9|[==1,>=0]-> c(c(x)) joins (1): c(c(x)) -8|[==1,=?1]-> a(b(x)) peak: b(a(b(x1553))) <-1|0[==1,==1]- b(c(a(x1553))) -10|[==1,==1]-> a(b(a(x1553))) joins (1): b(a(b(x1553))) -0|[==1,==1]-> a(b(b(x1553))) -5|0[==1,>>0]-> a(c(c(x1553))) a(b(a(x1553))) -7|0[==1,>>0]-> a(c(c(x1553))) peak: a(a(b(x1554))) <-1|0[==1,==1]- a(c(a(x1554))) -11|[==1,==1]-> a(b(a(x1554))) joins (1): a(b(a(x1554))) -0|0[==1,==1]-> a(a(b(x1554))) peak: b(a(b(x1555))) <-1|0[==1,==1]- b(c(a(x1555))) -13|[==1,==1]-> b(b(a(x1555))) joins (1): b(b(a(x1555))) -0|0[==1,==1]-> b(a(b(x1555))) peak: a(a(b(x1556))) <-1|0[==1,=>1]- a(c(a(x1556))) -15|[==1,?=3]-> c(a(a(x1556))) joins (1): c(a(a(x1556))) -1|[==1,=>1]-> a(b(a(x1556))) -0|0[==1,=>1]-> a(a(b(x1556))) peak: b(a(b(x1557))) <-1|0[==1,=?1]- b(c(a(x1557))) -17|[==1,>=0]-> c(c(a(x1557))) joins (1): b(a(b(x1557))) -7|[==1,>=0]-> c(c(b(x1557))) c(c(a(x1557))) -1|0[==1,=?1]-> c(a(b(x1557))) -9|[==1,>=0]-> c(c(b(x1557))) peak: a(b(x)) <-2|[==1,=>1]- c(b(x)) -3|[==1,?=2]-> c(a(x)) joins (1): c(a(x)) -1|[==1,=>1]-> a(b(x)) peak: b(a(b(x1559))) <-2|0[==1,=>1]- b(c(b(x1559))) -4|[==1,?=2]-> b(a(b(x1559))) joins (1): peak: a(a(b(x1560))) <-2|0[==1,=>1]- a(c(b(x1560))) -6|[==1,?=16]-> c(c(b(x1560))) joins (1): c(c(b(x1560))) -8|[==1,=>1]-> a(b(b(x1560))) -18|0[==1,=>1]-> a(a(b(x1560))) peak: c(a(b(x1561))) <-2|0[==1,==1]- c(c(b(x1561))) -8|[==1,==1]-> a(b(b(x1561))) joins (1): c(a(b(x1561))) -1|[==1,==1]-> a(b(b(x1561))) peak: b(a(b(x1562))) <-2|0[==1,==1]- b(c(b(x1562))) -10|[==1,==1]-> a(b(b(x1562))) joins (1): b(a(b(x1562))) -0|[==1,==1]-> a(b(b(x1562))) peak: a(a(b(x1563))) <-2|0[==1,==1]- a(c(b(x1563))) -11|[==1,==1]-> a(b(b(x1563))) joins (1): a(b(b(x1563))) -18|0[==1,==1]-> a(a(b(x1563))) peak: a(b(x)) <-2|[==1,=>1]- c(b(x)) -12|[==1,?=17]-> a(c(x)) joins (1): a(c(x)) -11|[==1,=>1]-> a(b(x)) peak: b(a(b(x1565))) <-2|0[==1,==1]- b(c(b(x1565))) -13|[==1,==1]-> b(b(b(x1565))) joins (1): b(a(b(x1565))) -0|[==1,==1]-> a(b(b(x1565))) b(b(b(x1565))) -18|[==1,==1]-> a(b(b(x1565))) peak: a(a(b(x1566))) <-2|0[==1,=>1]- a(c(b(x1566))) -15|[==1,?=3]-> c(a(b(x1566))) joins (1): c(a(b(x1566))) -1|[==1,=>1]-> a(b(b(x1566))) -18|0[==1,=>1]-> a(a(b(x1566))) peak: a(b(x)) <-2|[==1,=?1]- c(b(x)) -16|[==1,>=0]-> c(c(x)) joins (1): c(c(x)) -8|[==1,=?1]-> a(b(x)) peak: b(a(b(x1568))) <-2|0[==1,=?1]- b(c(b(x1568))) -17|[==1,>=0]-> c(c(b(x1568))) joins (1): b(a(b(x1568))) -7|[==1,>=0]-> c(c(b(x1568))) peak: c(a(x)) <-3|[==1,=?2]- c(b(x)) -2|[==1,>=1]-> a(b(x)) joins (1): c(a(x)) -1|[==1,>=1]-> a(b(x)) peak: b(c(a(x1570))) <-3|0[==1,==2]- b(c(b(x1570))) -4|[==1,==2]-> b(a(b(x1570))) joins (1): b(c(a(x1570))) -1|0[==1,>>1]-> b(a(b(x1570))) peak: a(c(a(x1571))) <-3|0[==1,=>2]- a(c(b(x1571))) -6|[==1,?=16]-> c(c(b(x1571))) joins (1): a(c(a(x1571))) -6|[==1,?=16]-> c(c(a(x1571))) c(c(b(x1571))) -3|0[==1,=>2]-> c(c(a(x1571))) peak: c(c(a(x1572))) <-3|0[==1,=?2]- c(c(b(x1572))) -8|[==1,>=1]-> a(b(b(x1572))) joins (1): c(c(a(x1572))) -8|[==1,>=1]-> a(b(a(x1572))) a(b(b(x1572))) -14|0[==1,=?2]-> a(b(a(x1572))) peak: b(c(a(x1573))) <-3|0[==1,=?2]- b(c(b(x1573))) -10|[==1,>=1]-> a(b(b(x1573))) joins (1): b(c(a(x1573))) -10|[==1,>=1]-> a(b(a(x1573))) a(b(b(x1573))) -14|0[==1,=?2]-> a(b(a(x1573))) peak: a(c(a(x1574))) <-3|0[==1,=?2]- a(c(b(x1574))) -11|[==1,>=1]-> a(b(b(x1574))) joins (1): a(c(a(x1574))) -1|0[==1,>=1]-> a(a(b(x1574))) a(b(b(x1574))) -18|0[==1,>=1]-> a(a(b(x1574))) peak: c(a(x)) <-3|[==1,=>2]- c(b(x)) -12|[==1,?=17]-> a(c(x)) joins (1): a(c(x)) -15|[==1,?>3]-> c(a(x)) peak: b(c(a(x1576))) <-3|0[==1,=?2]- b(c(b(x1576))) -13|[==1,>=1]-> b(b(b(x1576))) joins (1): b(c(a(x1576))) -1|0[==1,>=1]-> b(a(b(x1576))) b(b(b(x1576))) -14|[==1,=?2]-> b(a(b(x1576))) peak: a(c(a(x1577))) <-3|0[==1,=>2]- a(c(b(x1577))) -15|[==1,?=3]-> c(a(b(x1577))) joins (1): a(c(a(x1577))) -1|0[==1,>>1]-> a(a(b(x1577))) c(a(b(x1577))) -1|[==1,>>1]-> a(b(b(x1577))) -18|0[==1,>>1]-> a(a(b(x1577))) peak: c(a(x)) <-3|[==1,=?2]- c(b(x)) -16|[==1,>=0]-> c(c(x)) joins (1): c(a(x)) -9|[==1,>=0]-> c(c(x)) peak: b(c(a(x1579))) <-3|0[==1,=?2]- b(c(b(x1579))) -17|[==1,>=0]-> c(c(b(x1579))) joins (1): b(c(a(x1579))) -17|[==1,>=0]-> c(c(a(x1579))) c(c(b(x1579))) -3|0[==1,=?2]-> c(c(a(x1579))) peak: c(b(a(x1580))) <-4|0[==1,=?2]- c(b(c(x1580))) -2|[==1,>=1]-> a(b(c(x1580))) joins (1): c(b(a(x1580))) -2|[==1,>=1]-> a(b(a(x1580))) a(b(c(x1580))) -4|0[==1,=?2]-> a(b(a(x1580))) peak: c(b(a(x1581))) <-4|0[==1,==2]- c(b(c(x1581))) -3|[==1,==2]-> c(a(c(x1581))) joins (1): c(b(a(x1581))) -0|0[==1,>>1]-> c(a(b(x1581))) c(a(c(x1581))) -11|0[==1,>>1]-> c(a(b(x1581))) peak: b(b(a(x1582))) <-4|0[==1,=?2]- b(b(c(x1582))) -5|[==1,>=0]-> c(c(c(x1582))) joins (1): b(b(a(x1582))) -5|[==1,>=0]-> c(c(a(x1582))) -9|0[==1,>=0]-> c(c(c(x1582))) peak: b(a(x)) <-4|[==1,=?2]- b(c(x)) -10|[==1,>=1]-> a(b(x)) joins (1): b(a(x)) -0|[==1,>=1]-> a(b(x)) peak: c(b(a(x1584))) <-4|0[==1,=>2]- c(b(c(x1584))) -12|[==1,?=17]-> a(c(c(x1584))) joins (1): c(b(a(x1584))) -7|0[==1,>>0]-> c(c(c(x1584))) a(c(c(x1584))) -6|[==1,?>16]-> c(c(c(x1584))) peak: b(a(x)) <-4|[==1,=?2]- b(c(x)) -13|[==1,>=1]-> b(b(x)) joins (1): b(b(x)) -14|[==1,=?2]-> b(a(x)) peak: b(b(a(x1586))) <-4|0[==1,==2]- b(b(c(x1586))) -14|[==1,==2]-> b(a(c(x1586))) joins (1): b(b(a(x1586))) -0|0[==1,>>1]-> b(a(b(x1586))) b(a(c(x1586))) -11|0[==1,>>1]-> b(a(b(x1586))) peak: c(b(a(x1587))) <-4|0[==1,=?2]- c(b(c(x1587))) -16|[==1,>=0]-> c(c(c(x1587))) joins (1): c(b(a(x1587))) -7|0[==1,>=0]-> c(c(c(x1587))) peak: b(a(x)) <-4|[==1,=?2]- b(c(x)) -17|[==1,>=0]-> c(c(x)) joins (1): b(a(x)) -7|[==1,>=0]-> c(c(x)) peak: b(b(a(x1589))) <-4|0[==1,=?2]- b(b(c(x1589))) -18|[==1,>=1]-> a(b(c(x1589))) joins (1): b(b(a(x1589))) -18|[==1,>=1]-> a(b(a(x1589))) a(b(c(x1589))) -4|0[==1,=?2]-> a(b(a(x1589))) peak: c(c(c(x1590))) <-5|0[==1,=>0]- c(b(b(x1590))) -2|[==1,?=1]-> a(b(b(x1590))) joins (1): c(c(c(x1590))) -8|[==1,?=1]-> a(b(c(x1590))) -17|0[==1,=>0]-> a(c(c(x1590))) a(b(b(x1590))) -5|0[==1,=>0]-> a(c(c(x1590))) peak: c(c(c(x1591))) <-5|0[==1,=>0]- c(b(b(x1591))) -3|[==1,?=2]-> c(a(b(x1591))) joins (1): c(c(c(x1591))) -8|0[==1,?>1]-> c(a(b(x1591))) peak: b(c(c(x1592))) <-5|0[==1,==0]- b(b(b(x1592))) -5|[==1,==0]-> c(c(b(x1592))) joins (1): b(c(c(x1592))) -17|[==1,==0]-> c(c(c(x1592))) c(c(b(x1592))) -16|0[==1,==0]-> c(c(c(x1592))) peak: c(c(c(x1593))) <-5|0[==1,=>0]- c(b(b(x1593))) -12|[==1,?=17]-> a(c(b(x1593))) joins (1): c(c(c(x1593))) -8|0[==1,?>1]-> c(a(b(x1593))) a(c(b(x1593))) -15|[==1,?>3]-> c(a(b(x1593))) peak: c(c(x)) <-5|[==1,=>0]- b(b(x)) -14|[==1,?=2]-> b(a(x)) joins (1): b(a(x)) -7|[==1,=>0]-> c(c(x)) peak: b(c(c(x1595))) <-5|0[==1,=>0]- b(b(b(x1595))) -14|[==1,?=2]-> b(a(b(x1595))) joins (1): b(c(c(x1595))) -8|0[==1,?>1]-> b(a(b(x1595))) peak: c(c(c(x1596))) <-5|0[==1,==0]- c(b(b(x1596))) -16|[==1,==0]-> c(c(b(x1596))) joins (1): c(c(b(x1596))) -16|0[==1,==0]-> c(c(c(x1596))) peak: c(c(x)) <-5|[==1,=>0]- b(b(x)) -18|[==1,?=1]-> a(b(x)) joins (1): c(c(x)) -8|[==1,?=1]-> a(b(x)) peak: b(c(c(x1598))) <-5|0[==1,=>0]- b(b(b(x1598))) -18|[==1,?=1]-> a(b(b(x1598))) joins (1): b(c(c(x1598))) -10|[==1,?=1]-> a(b(c(x1598))) -17|0[==1,=>0]-> a(c(c(x1598))) a(b(b(x1598))) -5|0[==1,=>0]-> a(c(c(x1598))) peak: b(c(c(x1599))) <-6|0[==1,=?16]- b(a(c(x1599))) -0|[==1,>=1]-> a(b(c(x1599))) joins (1): b(c(c(x1599))) -10|[==1,>=1]-> a(b(c(x1599))) peak: c(c(c(x1600))) <-6|0[==1,=?16]- c(a(c(x1600))) -1|[==1,>=1]-> a(b(c(x1600))) joins (1): c(c(c(x1600))) -8|[==1,>=1]-> a(b(c(x1600))) peak: b(c(c(x1601))) <-6|0[==1,=?16]- b(a(c(x1601))) -7|[==1,>=0]-> c(c(c(x1601))) joins (1): b(c(c(x1601))) -17|[==1,>=0]-> c(c(c(x1601))) peak: c(c(c(x1602))) <-6|0[==1,=?16]- c(a(c(x1602))) -9|[==1,>=0]-> c(c(c(x1602))) joins (1): peak: c(c(x)) <-6|[==1,=?16]- a(c(x)) -11|[==1,>=1]-> a(b(x)) joins (1): c(c(x)) -8|[==1,>=1]-> a(b(x)) peak: c(c(x)) <-6|[==1,=?16]- a(c(x)) -15|[==1,>=3]-> c(a(x)) joins (1): c(a(x)) -9|[==1,>>0]-> c(c(x)) peak: c(c(x)) <-7|[==1,=>0]- b(a(x)) -0|[==1,?=1]-> a(b(x)) joins (1): c(c(x)) -8|[==1,?=1]-> a(b(x)) peak: c(c(c(x1606))) <-7|0[==1,=>0]- c(b(a(x1606))) -2|[==1,?=1]-> a(b(a(x1606))) joins (1): c(c(c(x1606))) -8|[==1,?=1]-> a(b(c(x1606))) -17|0[==1,=>0]-> a(c(c(x1606))) a(b(a(x1606))) -7|0[==1,=>0]-> a(c(c(x1606))) peak: c(c(c(x1607))) <-7|0[==1,=>0]- c(b(a(x1607))) -3|[==1,?=2]-> c(a(a(x1607))) joins (1): c(a(a(x1607))) -9|[==1,=>0]-> c(c(a(x1607))) -9|0[==1,=>0]-> c(c(c(x1607))) peak: b(c(c(x1608))) <-7|0[==1,==0]- b(b(a(x1608))) -5|[==1,==0]-> c(c(a(x1608))) joins (1): b(c(c(x1608))) -17|[==1,==0]-> c(c(c(x1608))) c(c(a(x1608))) -9|0[==1,==0]-> c(c(c(x1608))) peak: c(c(c(x1609))) <-7|0[==1,=>0]- c(b(a(x1609))) -12|[==1,?=17]-> a(c(a(x1609))) joins (1): a(c(a(x1609))) -6|[==1,?>16]-> c(c(a(x1609))) -9|0[==1,=>0]-> c(c(c(x1609))) peak: b(c(c(x1610))) <-7|0[==1,=>0]- b(b(a(x1610))) -14|[==1,?=2]-> b(a(a(x1610))) joins (1): b(c(c(x1610))) -17|[==1,=>0]-> c(c(c(x1610))) b(a(a(x1610))) -7|[==1,=>0]-> c(c(a(x1610))) -9|0[==1,=>0]-> c(c(c(x1610))) peak: c(c(c(x1611))) <-7|0[==1,==0]- c(b(a(x1611))) -16|[==1,==0]-> c(c(a(x1611))) joins (1): c(c(a(x1611))) -9|0[==1,==0]-> c(c(c(x1611))) peak: b(c(c(x1612))) <-7|0[==1,=>0]- b(b(a(x1612))) -18|[==1,?=1]-> a(b(a(x1612))) joins (1): b(c(c(x1612))) -10|[==1,?=1]-> a(b(c(x1612))) -17|0[==1,=>0]-> a(c(c(x1612))) a(b(a(x1612))) -7|0[==1,=>0]-> a(c(c(x1612))) peak: b(a(b(x1613))) <-8|0[==1,=>1]- b(c(c(x1613))) -4|[==1,?=2]-> b(a(c(x1613))) joins (1): b(a(c(x1613))) -11|0[==1,=>1]-> b(a(b(x1613))) peak: a(a(b(x1614))) <-8|0[==1,=>1]- a(c(c(x1614))) -6|[==1,?=16]-> c(c(c(x1614))) joins (1): c(c(c(x1614))) -8|[==1,=>1]-> a(b(c(x1614))) -10|0[==1,=>1]-> a(a(b(x1614))) peak: c(a(b(x1615))) <-8|0[==1,==1]- c(c(c(x1615))) -8|[==1,==1]-> a(b(c(x1615))) joins (1): c(a(b(x1615))) -1|[==1,==1]-> a(b(b(x1615))) a(b(c(x1615))) -13|0[==1,==1]-> a(b(b(x1615))) peak: b(a(b(x1616))) <-8|0[==1,==1]- b(c(c(x1616))) -10|[==1,==1]-> a(b(c(x1616))) joins (1): b(a(b(x1616))) -0|[==1,==1]-> a(b(b(x1616))) a(b(c(x1616))) -13|0[==1,==1]-> a(b(b(x1616))) peak: a(a(b(x1617))) <-8|0[==1,==1]- a(c(c(x1617))) -11|[==1,==1]-> a(b(c(x1617))) joins (1): a(b(c(x1617))) -10|0[==1,==1]-> a(a(b(x1617))) peak: b(a(b(x1618))) <-8|0[==1,==1]- b(c(c(x1618))) -13|[==1,==1]-> b(b(c(x1618))) joins (1): b(b(c(x1618))) -10|0[==1,==1]-> b(a(b(x1618))) peak: a(a(b(x1619))) <-8|0[==1,=>1]- a(c(c(x1619))) -15|[==1,?=3]-> c(a(c(x1619))) joins (1): c(a(c(x1619))) -1|[==1,=>1]-> a(b(c(x1619))) -10|0[==1,=>1]-> a(a(b(x1619))) peak: b(a(b(x1620))) <-8|0[==1,=?1]- b(c(c(x1620))) -17|[==1,>=0]-> c(c(c(x1620))) joins (1): b(a(b(x1620))) -7|[==1,>=0]-> c(c(b(x1620))) -16|0[==1,>=0]-> c(c(c(x1620))) peak: c(c(x)) <-9|[==1,=>0]- c(a(x)) -1|[==1,?=1]-> a(b(x)) joins (1): c(c(x)) -8|[==1,?=1]-> a(b(x)) peak: b(c(c(x1622))) <-9|0[==1,=>0]- b(c(a(x1622))) -4|[==1,?=2]-> b(a(a(x1622))) joins (1): b(c(c(x1622))) -17|[==1,=>0]-> c(c(c(x1622))) b(a(a(x1622))) -7|[==1,=>0]-> c(c(a(x1622))) -9|0[==1,=>0]-> c(c(c(x1622))) peak: a(c(c(x1623))) <-9|0[==1,=>0]- a(c(a(x1623))) -6|[==1,?=16]-> c(c(a(x1623))) joins (1): a(c(c(x1623))) -6|[==1,?=16]-> c(c(c(x1623))) c(c(a(x1623))) -9|0[==1,=>0]-> c(c(c(x1623))) peak: c(c(c(x1624))) <-9|0[==1,=>0]- c(c(a(x1624))) -8|[==1,?=1]-> a(b(a(x1624))) joins (1): c(c(c(x1624))) -8|[==1,?=1]-> a(b(c(x1624))) -17|0[==1,=>0]-> a(c(c(x1624))) a(b(a(x1624))) -7|0[==1,=>0]-> a(c(c(x1624))) peak: b(c(c(x1625))) <-9|0[==1,=>0]- b(c(a(x1625))) -10|[==1,?=1]-> a(b(a(x1625))) joins (1): b(c(c(x1625))) -10|[==1,?=1]-> a(b(c(x1625))) -17|0[==1,=>0]-> a(c(c(x1625))) a(b(a(x1625))) -7|0[==1,=>0]-> a(c(c(x1625))) peak: a(c(c(x1626))) <-9|0[==1,=>0]- a(c(a(x1626))) -11|[==1,?=1]-> a(b(a(x1626))) joins (1): a(b(a(x1626))) -7|0[==1,=>0]-> a(c(c(x1626))) peak: b(c(c(x1627))) <-9|0[==1,=>0]- b(c(a(x1627))) -13|[==1,?=1]-> b(b(a(x1627))) joins (1): b(b(a(x1627))) -7|0[==1,=>0]-> b(c(c(x1627))) peak: a(c(c(x1628))) <-9|0[==1,=>0]- a(c(a(x1628))) -15|[==1,?=3]-> c(a(a(x1628))) joins (1): c(a(a(x1628))) -1|[==1,?>1]-> a(b(a(x1628))) -7|0[==1,=>0]-> a(c(c(x1628))) peak: b(c(c(x1629))) <-9|0[==1,==0]- b(c(a(x1629))) -17|[==1,==0]-> c(c(a(x1629))) joins (1): b(c(c(x1629))) -17|[==1,==0]-> c(c(c(x1629))) c(c(a(x1629))) -9|0[==1,==0]-> c(c(c(x1629))) peak: c(a(b(x1630))) <-10|0[==1,==1]- c(b(c(x1630))) -2|[==1,==1]-> a(b(c(x1630))) joins (1): c(a(b(x1630))) -1|[==1,==1]-> a(b(b(x1630))) a(b(c(x1630))) -13|0[==1,==1]-> a(b(b(x1630))) peak: c(a(b(x1631))) <-10|0[==1,=>1]- c(b(c(x1631))) -3|[==1,?=2]-> c(a(c(x1631))) joins (1): c(a(c(x1631))) -11|0[==1,=>1]-> c(a(b(x1631))) peak: a(b(x)) <-10|[==1,=>1]- b(c(x)) -4|[==1,?=2]-> b(a(x)) joins (1): b(a(x)) -0|[==1,=>1]-> a(b(x)) peak: b(a(b(x1633))) <-10|0[==1,=?1]- b(b(c(x1633))) -5|[==1,>=0]-> c(c(c(x1633))) joins (1): b(a(b(x1633))) -7|[==1,>=0]-> c(c(b(x1633))) -16|0[==1,>=0]-> c(c(c(x1633))) peak: c(a(b(x1634))) <-10|0[==1,=>1]- c(b(c(x1634))) -12|[==1,?=17]-> a(c(c(x1634))) joins (1): a(c(c(x1634))) -6|[==1,?>16]-> c(c(c(x1634))) -8|0[==1,=>1]-> c(a(b(x1634))) peak: a(b(x)) <-10|[==1,==1]- b(c(x)) -13|[==1,==1]-> b(b(x)) joins (1): b(b(x)) -18|[==1,==1]-> a(b(x)) peak: b(a(b(x1636))) <-10|0[==1,=>1]- b(b(c(x1636))) -14|[==1,?=2]-> b(a(c(x1636))) joins (1): b(a(c(x1636))) -11|0[==1,=>1]-> b(a(b(x1636))) peak: c(a(b(x1637))) <-10|0[==1,=?1]- c(b(c(x1637))) -16|[==1,>=0]-> c(c(c(x1637))) joins (1): c(c(c(x1637))) -8|0[==1,=?1]-> c(a(b(x1637))) peak: a(b(x)) <-10|[==1,=?1]- b(c(x)) -17|[==1,>=0]-> c(c(x)) joins (1): c(c(x)) -8|[==1,=?1]-> a(b(x)) peak: b(a(b(x1639))) <-10|0[==1,==1]- b(b(c(x1639))) -18|[==1,==1]-> a(b(c(x1639))) joins (1): b(a(b(x1639))) -0|[==1,==1]-> a(b(b(x1639))) a(b(c(x1639))) -13|0[==1,==1]-> a(b(b(x1639))) peak: b(a(b(x1640))) <-11|0[==1,==1]- b(a(c(x1640))) -0|[==1,==1]-> a(b(c(x1640))) joins (1): b(a(b(x1640))) -0|[==1,==1]-> a(b(b(x1640))) a(b(c(x1640))) -13|0[==1,==1]-> a(b(b(x1640))) peak: c(a(b(x1641))) <-11|0[==1,==1]- c(a(c(x1641))) -1|[==1,==1]-> a(b(c(x1641))) joins (1): c(a(b(x1641))) -1|[==1,==1]-> a(b(b(x1641))) a(b(c(x1641))) -13|0[==1,==1]-> a(b(b(x1641))) peak: a(b(x)) <-11|[==1,=>1]- a(c(x)) -6|[==1,?=16]-> c(c(x)) joins (1): c(c(x)) -8|[==1,=>1]-> a(b(x)) peak: b(a(b(x1643))) <-11|0[==1,=?1]- b(a(c(x1643))) -7|[==1,>=0]-> c(c(c(x1643))) joins (1): b(a(b(x1643))) -7|[==1,>=0]-> c(c(b(x1643))) -16|0[==1,>=0]-> c(c(c(x1643))) peak: c(a(b(x1644))) <-11|0[==1,=?1]- c(a(c(x1644))) -9|[==1,>=0]-> c(c(c(x1644))) joins (1): c(c(c(x1644))) -8|0[==1,=?1]-> c(a(b(x1644))) peak: a(b(x)) <-11|[==1,=>1]- a(c(x)) -15|[==1,?=3]-> c(a(x)) joins (1): c(a(x)) -1|[==1,=>1]-> a(b(x)) peak: a(c(x)) <-12|[==1,=?17]- c(b(x)) -2|[==1,>=1]-> a(b(x)) joins (1): a(c(x)) -11|[==1,>=1]-> a(b(x)) peak: a(c(x)) <-12|[==1,=?17]- c(b(x)) -3|[==1,>=2]-> c(a(x)) joins (1): a(c(x)) -15|[==1,>?3]-> c(a(x)) peak: b(a(c(x1648))) <-12|0[==1,=?17]- b(c(b(x1648))) -4|[==1,>=2]-> b(a(b(x1648))) joins (1): b(a(c(x1648))) -11|0[==1,>>1]-> b(a(b(x1648))) peak: a(a(c(x1649))) <-12|0[==1,=?17]- a(c(b(x1649))) -6|[==1,>=16]-> c(c(b(x1649))) joins (1): a(a(c(x1649))) -6|0[==1,>=16]-> a(c(c(x1649))) c(c(b(x1649))) -8|[==1,>>1]-> a(b(b(x1649))) -5|0[==1,>>0]-> a(c(c(x1649))) peak: c(a(c(x1650))) <-12|0[==1,=?17]- c(c(b(x1650))) -8|[==1,>=1]-> a(b(b(x1650))) joins (1): a(b(b(x1650))) -5|0[==1,>>0]-> a(c(c(x1650))) -15|[==1,>?3]-> c(a(c(x1650))) peak: b(a(c(x1651))) <-12|0[==1,=?17]- b(c(b(x1651))) -10|[==1,>=1]-> a(b(b(x1651))) joins (1): b(a(c(x1651))) -0|[==1,>=1]-> a(b(c(x1651))) -13|0[==1,>=1]-> a(b(b(x1651))) peak: a(a(c(x1652))) <-12|0[==1,=?17]- a(c(b(x1652))) -11|[==1,>=1]-> a(b(b(x1652))) joins (1): a(a(c(x1652))) -6|0[==1,>?16]-> a(c(c(x1652))) a(b(b(x1652))) -5|0[==1,>>0]-> a(c(c(x1652))) peak: b(a(c(x1653))) <-12|0[==1,=?17]- b(c(b(x1653))) -13|[==1,>=1]-> b(b(b(x1653))) joins (1): b(a(c(x1653))) -6|0[==1,>?16]-> b(c(c(x1653))) b(b(b(x1653))) -5|0[==1,>>0]-> b(c(c(x1653))) peak: a(a(c(x1654))) <-12|0[==1,=?17]- a(c(b(x1654))) -15|[==1,>=3]-> c(a(b(x1654))) joins (1): a(a(c(x1654))) -6|0[==1,>?16]-> a(c(c(x1654))) c(a(b(x1654))) -1|[==1,>>1]-> a(b(b(x1654))) -5|0[==1,>>0]-> a(c(c(x1654))) peak: a(c(x)) <-12|[==1,=?17]- c(b(x)) -16|[==1,>=0]-> c(c(x)) joins (1): a(c(x)) -6|[==1,>?16]-> c(c(x)) peak: b(a(c(x1656))) <-12|0[==1,=?17]- b(c(b(x1656))) -17|[==1,>=0]-> c(c(b(x1656))) joins (1): b(a(c(x1656))) -7|[==1,>=0]-> c(c(c(x1656))) c(c(b(x1656))) -16|0[==1,>=0]-> c(c(c(x1656))) peak: c(b(b(x1657))) <-13|0[==1,==1]- c(b(c(x1657))) -2|[==1,==1]-> a(b(c(x1657))) joins (1): c(b(b(x1657))) -2|[==1,==1]-> a(b(b(x1657))) a(b(c(x1657))) -13|0[==1,==1]-> a(b(b(x1657))) peak: c(b(b(x1658))) <-13|0[==1,=>1]- c(b(c(x1658))) -3|[==1,?=2]-> c(a(c(x1658))) joins (1): c(b(b(x1658))) -3|[==1,?=2]-> c(a(b(x1658))) c(a(c(x1658))) -11|0[==1,=>1]-> c(a(b(x1658))) peak: b(b(x)) <-13|[==1,=>1]- b(c(x)) -4|[==1,?=2]-> b(a(x)) joins (1): b(b(x)) -14|[==1,?=2]-> b(a(x)) peak: b(b(b(x1660))) <-13|0[==1,=?1]- b(b(c(x1660))) -5|[==1,>=0]-> c(c(c(x1660))) joins (1): b(b(b(x1660))) -5|0[==1,>=0]-> b(c(c(x1660))) -17|[==1,>=0]-> c(c(c(x1660))) peak: b(b(x)) <-13|[==1,==1]- b(c(x)) -10|[==1,==1]-> a(b(x)) joins (1): b(b(x)) -18|[==1,==1]-> a(b(x)) peak: c(b(b(x1662))) <-13|0[==1,=>1]- c(b(c(x1662))) -12|[==1,?=17]-> a(c(c(x1662))) joins (1): c(b(b(x1662))) -5|0[==1,>>0]-> c(c(c(x1662))) a(c(c(x1662))) -6|[==1,?>16]-> c(c(c(x1662))) peak: b(b(b(x1663))) <-13|0[==1,=>1]- b(b(c(x1663))) -14|[==1,?=2]-> b(a(c(x1663))) joins (1): b(b(b(x1663))) -14|[==1,?=2]-> b(a(b(x1663))) b(a(c(x1663))) -11|0[==1,=>1]-> b(a(b(x1663))) peak: c(b(b(x1664))) <-13|0[==1,=?1]- c(b(c(x1664))) -16|[==1,>=0]-> c(c(c(x1664))) joins (1): c(b(b(x1664))) -5|0[==1,>=0]-> c(c(c(x1664))) peak: b(b(x)) <-13|[==1,=?1]- b(c(x)) -17|[==1,>=0]-> c(c(x)) joins (1): b(b(x)) -5|[==1,>=0]-> c(c(x)) peak: b(b(b(x1666))) <-13|0[==1,==1]- b(b(c(x1666))) -18|[==1,==1]-> a(b(c(x1666))) joins (1): b(b(b(x1666))) -18|[==1,==1]-> a(b(b(x1666))) a(b(c(x1666))) -13|0[==1,==1]-> a(b(b(x1666))) peak: c(b(a(x1667))) <-14|0[==1,=?2]- c(b(b(x1667))) -2|[==1,>=1]-> a(b(b(x1667))) joins (1): c(b(a(x1667))) -2|[==1,>=1]-> a(b(a(x1667))) a(b(b(x1667))) -14|0[==1,=?2]-> a(b(a(x1667))) peak: c(b(a(x1668))) <-14|0[==1,==2]- c(b(b(x1668))) -3|[==1,==2]-> c(a(b(x1668))) joins (1): c(b(a(x1668))) -0|0[==1,>>1]-> c(a(b(x1668))) peak: b(a(x)) <-14|[==1,=?2]- b(b(x)) -5|[==1,>=0]-> c(c(x)) joins (1): b(a(x)) -7|[==1,>=0]-> c(c(x)) peak: b(b(a(x1670))) <-14|0[==1,=?2]- b(b(b(x1670))) -5|[==1,>=0]-> c(c(b(x1670))) joins (1): b(b(a(x1670))) -5|[==1,>=0]-> c(c(a(x1670))) c(c(b(x1670))) -3|0[==1,=?2]-> c(c(a(x1670))) peak: c(b(a(x1671))) <-14|0[==1,=>2]- c(b(b(x1671))) -12|[==1,?=17]-> a(c(b(x1671))) joins (1): c(b(a(x1671))) -0|0[==1,>>1]-> c(a(b(x1671))) a(c(b(x1671))) -15|[==1,?>3]-> c(a(b(x1671))) peak: b(b(a(x1672))) <-14|0[==1,==2]- b(b(b(x1672))) -14|[==1,==2]-> b(a(b(x1672))) joins (1): b(b(a(x1672))) -0|0[==1,>>1]-> b(a(b(x1672))) peak: c(b(a(x1673))) <-14|0[==1,=?2]- c(b(b(x1673))) -16|[==1,>=0]-> c(c(b(x1673))) joins (1): c(b(a(x1673))) -0|0[==1,>?1]-> c(a(b(x1673))) c(c(b(x1673))) -2|0[==1,>?1]-> c(a(b(x1673))) peak: b(a(x)) <-14|[==1,=?2]- b(b(x)) -18|[==1,>=1]-> a(b(x)) joins (1): b(a(x)) -0|[==1,>=1]-> a(b(x)) peak: b(b(a(x1675))) <-14|0[==1,=?2]- b(b(b(x1675))) -18|[==1,>=1]-> a(b(b(x1675))) joins (1): b(b(a(x1675))) -18|[==1,>=1]-> a(b(a(x1675))) a(b(b(x1675))) -14|0[==1,=?2]-> a(b(a(x1675))) peak: b(c(a(x1676))) <-15|0[==1,=?3]- b(a(c(x1676))) -0|[==1,>=1]-> a(b(c(x1676))) joins (1): b(c(a(x1676))) -10|[==1,>=1]-> a(b(a(x1676))) a(b(c(x1676))) -4|0[==1,>?2]-> a(b(a(x1676))) peak: c(c(a(x1677))) <-15|0[==1,=?3]- c(a(c(x1677))) -1|[==1,>=1]-> a(b(c(x1677))) joins (1): c(c(a(x1677))) -8|[==1,>=1]-> a(b(a(x1677))) a(b(c(x1677))) -4|0[==1,>?2]-> a(b(a(x1677))) peak: c(a(x)) <-15|[==1,=>3]- a(c(x)) -6|[==1,?=16]-> c(c(x)) joins (1): c(a(x)) -9|[==1,>>0]-> c(c(x)) peak: b(c(a(x1679))) <-15|0[==1,=?3]- b(a(c(x1679))) -7|[==1,>=0]-> c(c(c(x1679))) joins (1): b(c(a(x1679))) -9|0[==1,>=0]-> b(c(c(x1679))) -17|[==1,>=0]-> c(c(c(x1679))) peak: c(c(a(x1680))) <-15|0[==1,=?3]- c(a(c(x1680))) -9|[==1,>=0]-> c(c(c(x1680))) joins (1): c(c(a(x1680))) -9|0[==1,>=0]-> c(c(c(x1680))) peak: c(a(x)) <-15|[==1,=?3]- a(c(x)) -11|[==1,>=1]-> a(b(x)) joins (1): c(a(x)) -1|[==1,>=1]-> a(b(x)) peak: c(c(x)) <-16|[==1,=>0]- c(b(x)) -2|[==1,?=1]-> a(b(x)) joins (1): c(c(x)) -8|[==1,?=1]-> a(b(x)) peak: c(c(x)) <-16|[==1,=>0]- c(b(x)) -3|[==1,?=2]-> c(a(x)) joins (1): c(a(x)) -9|[==1,=>0]-> c(c(x)) peak: b(c(c(x1684))) <-16|0[==1,=>0]- b(c(b(x1684))) -4|[==1,?=2]-> b(a(b(x1684))) joins (1): b(c(c(x1684))) -8|0[==1,?>1]-> b(a(b(x1684))) peak: a(c(c(x1685))) <-16|0[==1,=>0]- a(c(b(x1685))) -6|[==1,?=16]-> c(c(b(x1685))) joins (1): a(c(c(x1685))) -6|[==1,?=16]-> c(c(c(x1685))) c(c(b(x1685))) -16|0[==1,=>0]-> c(c(c(x1685))) peak: c(c(c(x1686))) <-16|0[==1,=>0]- c(c(b(x1686))) -8|[==1,?=1]-> a(b(b(x1686))) joins (1): c(c(c(x1686))) -8|[==1,?=1]-> a(b(c(x1686))) -17|0[==1,=>0]-> a(c(c(x1686))) a(b(b(x1686))) -5|0[==1,=>0]-> a(c(c(x1686))) peak: b(c(c(x1687))) <-16|0[==1,=>0]- b(c(b(x1687))) -10|[==1,?=1]-> a(b(b(x1687))) joins (1): b(c(c(x1687))) -10|[==1,?=1]-> a(b(c(x1687))) -17|0[==1,=>0]-> a(c(c(x1687))) a(b(b(x1687))) -5|0[==1,=>0]-> a(c(c(x1687))) peak: a(c(c(x1688))) <-16|0[==1,=>0]- a(c(b(x1688))) -11|[==1,?=1]-> a(b(b(x1688))) joins (1): a(b(b(x1688))) -5|0[==1,=>0]-> a(c(c(x1688))) peak: c(c(x)) <-16|[==1,=>0]- c(b(x)) -12|[==1,?=17]-> a(c(x)) joins (1): a(c(x)) -6|[==1,?>16]-> c(c(x)) peak: b(c(c(x1690))) <-16|0[==1,=>0]- b(c(b(x1690))) -13|[==1,?=1]-> b(b(b(x1690))) joins (1): b(b(b(x1690))) -5|0[==1,=>0]-> b(c(c(x1690))) peak: a(c(c(x1691))) <-16|0[==1,=>0]- a(c(b(x1691))) -15|[==1,?=3]-> c(a(b(x1691))) joins (1): c(a(b(x1691))) -1|[==1,?>1]-> a(b(b(x1691))) -5|0[==1,=>0]-> a(c(c(x1691))) peak: b(c(c(x1692))) <-16|0[==1,==0]- b(c(b(x1692))) -17|[==1,==0]-> c(c(b(x1692))) joins (1): b(c(c(x1692))) -17|[==1,==0]-> c(c(c(x1692))) c(c(b(x1692))) -16|0[==1,==0]-> c(c(c(x1692))) peak: c(c(c(x1693))) <-17|0[==1,=>0]- c(b(c(x1693))) -2|[==1,?=1]-> a(b(c(x1693))) joins (1): c(c(c(x1693))) -8|[==1,?=1]-> a(b(c(x1693))) peak: c(c(c(x1694))) <-17|0[==1,=>0]- c(b(c(x1694))) -3|[==1,?=2]-> c(a(c(x1694))) joins (1): c(a(c(x1694))) -9|[==1,=>0]-> c(c(c(x1694))) peak: c(c(x)) <-17|[==1,=>0]- b(c(x)) -4|[==1,?=2]-> b(a(x)) joins (1): b(a(x)) -7|[==1,=>0]-> c(c(x)) peak: b(c(c(x1696))) <-17|0[==1,==0]- b(b(c(x1696))) -5|[==1,==0]-> c(c(c(x1696))) joins (1): b(c(c(x1696))) -17|[==1,==0]-> c(c(c(x1696))) peak: c(c(x)) <-17|[==1,=>0]- b(c(x)) -10|[==1,?=1]-> a(b(x)) joins (1): c(c(x)) -8|[==1,?=1]-> a(b(x)) peak: c(c(c(x1698))) <-17|0[==1,=>0]- c(b(c(x1698))) -12|[==1,?=17]-> a(c(c(x1698))) joins (1): a(c(c(x1698))) -6|[==1,?>16]-> c(c(c(x1698))) peak: c(c(x)) <-17|[==1,=>0]- b(c(x)) -13|[==1,?=1]-> b(b(x)) joins (1): b(b(x)) -5|[==1,=>0]-> c(c(x)) peak: b(c(c(x1700))) <-17|0[==1,=>0]- b(b(c(x1700))) -14|[==1,?=2]-> b(a(c(x1700))) joins (1): b(c(c(x1700))) -4|[==1,?=2]-> b(a(c(x1700))) peak: c(c(c(x1701))) <-17|0[==1,==0]- c(b(c(x1701))) -16|[==1,==0]-> c(c(c(x1701))) joins (1): peak: b(c(c(x1702))) <-17|0[==1,=>0]- b(b(c(x1702))) -18|[==1,?=1]-> a(b(c(x1702))) joins (1): b(c(c(x1702))) -10|[==1,?=1]-> a(b(c(x1702))) peak: c(a(b(x1703))) <-18|0[==1,==1]- c(b(b(x1703))) -2|[==1,==1]-> a(b(b(x1703))) joins (1): c(a(b(x1703))) -1|[==1,==1]-> a(b(b(x1703))) peak: c(a(b(x1704))) <-18|0[==1,=>1]- c(b(b(x1704))) -3|[==1,?=2]-> c(a(b(x1704))) joins (1): peak: a(b(x)) <-18|[==1,=?1]- b(b(x)) -5|[==1,>=0]-> c(c(x)) joins (1): c(c(x)) -8|[==1,=?1]-> a(b(x)) peak: b(a(b(x1706))) <-18|0[==1,=?1]- b(b(b(x1706))) -5|[==1,>=0]-> c(c(b(x1706))) joins (1): b(a(b(x1706))) -7|[==1,>=0]-> c(c(b(x1706))) peak: c(a(b(x1707))) <-18|0[==1,=>1]- c(b(b(x1707))) -12|[==1,?=17]-> a(c(b(x1707))) joins (1): a(c(b(x1707))) -15|[==1,?>3]-> c(a(b(x1707))) peak: a(b(x)) <-18|[==1,=>1]- b(b(x)) -14|[==1,?=2]-> b(a(x)) joins (1): b(a(x)) -0|[==1,=>1]-> a(b(x)) peak: b(a(b(x1709))) <-18|0[==1,=>1]- b(b(b(x1709))) -14|[==1,?=2]-> b(a(b(x1709))) joins (1): peak: c(a(b(x1710))) <-18|0[==1,=?1]- c(b(b(x1710))) -16|[==1,>=0]-> c(c(b(x1710))) joins (1): c(c(b(x1710))) -2|0[==1,=?1]-> c(a(b(x1710))) peak: b(a(b(x1711))) <-18|0[==1,==1]- b(b(b(x1711))) -18|[==1,==1]-> a(b(b(x1711))) joins (1): b(a(b(x1711))) -0|[==1,==1]-> a(b(b(x1711))) Qed