YES

Problem:
 c(c(x)) -> a(a(x))
 b(b(x)) -> c(c(x))
 c(c(x)) -> b(b(x))
 c(b(x)) -> c(c(x))
 b(b(x)) -> c(b(x))
 a(a(x)) -> c(b(x))
 c(a(x)) -> a(a(x))
 a(c(x)) -> c(a(x))
 c(b(x)) -> a(c(x))
 b(c(x)) -> a(c(x))
 a(a(x)) -> b(c(x))
 a(a(x)) -> b(a(x))
 b(c(x)) -> b(a(x))
 a(c(x)) -> b(c(x))
 c(b(x)) -> b(c(x))
 a(b(x)) -> a(a(x))

Proof:
 Church Rosser Transformation Processor (no redundant rules):
  strict:
   
  weak:
   
  critical peaks: 104
   a(a(a(x513))) <-0|0[]- a(a(b(x513))) -4|[]-> b(a(b(x513)))
   a(a(a(x514))) <-0|0[]- a(a(b(x514))) -5|[]-> b(c(b(x514)))
   c(a(a(x515))) <-0|0[]- c(a(b(x515))) -9|[]-> a(a(b(x515)))
   a(a(a(x516))) <-0|0[]- a(a(b(x516))) -10|[]-> c(b(b(x516)))
   a(b(c(x517))) <-1|0[]- a(c(b(x517))) -2|[]-> b(c(b(x517)))
   b(b(c(x518))) <-1|0[]- b(c(b(x518))) -3|[]-> b(a(b(x518)))
   b(b(c(x519))) <-1|0[]- b(c(b(x519))) -6|[]-> a(c(b(x519)))
   b(c(x)) <-1|[]- c(b(x)) -7|[]-> a(c(x))
   a(b(c(x521))) <-1|0[]- a(c(b(x521))) -8|[]-> c(a(b(x521)))
   b(c(x)) <-1|[]- c(b(x)) -12|[]-> c(c(x))
   c(b(c(x523))) <-1|0[]- c(c(b(x523))) -13|[]-> b(b(b(x523)))
   c(b(c(x524))) <-1|0[]- c(c(b(x524))) -15|[]-> a(a(b(x524)))
   a(b(c(x525))) <-2|0[]- a(a(c(x525))) -4|[]-> b(a(c(x525)))
   a(b(c(x526))) <-2|0[]- a(a(c(x526))) -5|[]-> b(c(c(x526)))
   b(c(x)) <-2|[]- a(c(x)) -8|[]-> c(a(x))
   c(b(c(x528))) <-2|0[]- c(a(c(x528))) -9|[]-> a(a(c(x528)))
   a(b(c(x529))) <-2|0[]- a(a(c(x529))) -10|[]-> c(b(c(x529)))
   a(b(a(x530))) <-3|0[]- a(b(c(x530))) -0|[]-> a(a(c(x530)))
   c(b(a(x531))) <-3|0[]- c(b(c(x531))) -1|[]-> b(c(c(x531)))
   b(a(x)) <-3|[]- b(c(x)) -6|[]-> a(c(x))
   c(b(a(x533))) <-3|0[]- c(b(c(x533))) -7|[]-> a(c(c(x533)))
   b(b(a(x534))) <-3|0[]- b(b(c(x534))) -11|[]-> c(b(c(x534)))
   c(b(a(x535))) <-3|0[]- c(b(c(x535))) -12|[]-> c(c(c(x535)))
   b(b(a(x536))) <-3|0[]- b(b(c(x536))) -14|[]-> c(c(c(x536)))
   a(b(a(x537))) <-4|0[]- a(a(a(x537))) -4|[]-> b(a(a(x537)))
   b(a(x)) <-4|[]- a(a(x)) -5|[]-> b(c(x))
   a(b(a(x539))) <-4|0[]- a(a(a(x539))) -5|[]-> b(c(a(x539)))
   c(b(a(x540))) <-4|0[]- c(a(a(x540))) -9|[]-> a(a(a(x540)))
   b(a(x)) <-4|[]- a(a(x)) -10|[]-> c(b(x))
   a(b(a(x542))) <-4|0[]- a(a(a(x542))) -10|[]-> c(b(a(x542)))
   b(c(x)) <-5|[]- a(a(x)) -4|[]-> b(a(x))
   a(b(c(x544))) <-5|0[]- a(a(a(x544))) -4|[]-> b(a(a(x544)))
   a(b(c(x545))) <-5|0[]- a(a(a(x545))) -5|[]-> b(c(a(x545)))
   c(b(c(x546))) <-5|0[]- c(a(a(x546))) -9|[]-> a(a(a(x546)))
   b(c(x)) <-5|[]- a(a(x)) -10|[]-> c(b(x))
   a(b(c(x548))) <-5|0[]- a(a(a(x548))) -10|[]-> c(b(a(x548)))
   a(a(c(x549))) <-6|0[]- a(b(c(x549))) -0|[]-> a(a(c(x549)))
   c(a(c(x550))) <-6|0[]- c(b(c(x550))) -1|[]-> b(c(c(x550)))
   a(c(x)) <-6|[]- b(c(x)) -3|[]-> b(a(x))
   c(a(c(x552))) <-6|0[]- c(b(c(x552))) -7|[]-> a(c(c(x552)))
   b(a(c(x553))) <-6|0[]- b(b(c(x553))) -11|[]-> c(b(c(x553)))
   c(a(c(x554))) <-6|0[]- c(b(c(x554))) -12|[]-> c(c(c(x554)))
   b(a(c(x555))) <-6|0[]- b(b(c(x555))) -14|[]-> c(c(c(x555)))
   a(c(x)) <-7|[]- c(b(x)) -1|[]-> b(c(x))
   a(a(c(x557))) <-7|0[]- a(c(b(x557))) -2|[]-> b(c(b(x557)))
   b(a(c(x558))) <-7|0[]- b(c(b(x558))) -3|[]-> b(a(b(x558)))
   b(a(c(x559))) <-7|0[]- b(c(b(x559))) -6|[]-> a(c(b(x559)))
   a(a(c(x560))) <-7|0[]- a(c(b(x560))) -8|[]-> c(a(b(x560)))
   a(c(x)) <-7|[]- c(b(x)) -12|[]-> c(c(x))
   c(a(c(x562))) <-7|0[]- c(c(b(x562))) -13|[]-> b(b(b(x562)))
   c(a(c(x563))) <-7|0[]- c(c(b(x563))) -15|[]-> a(a(b(x563)))
   c(a(x)) <-8|[]- a(c(x)) -2|[]-> b(c(x))
   a(c(a(x565))) <-8|0[]- a(a(c(x565))) -4|[]-> b(a(c(x565)))
   a(c(a(x566))) <-8|0[]- a(a(c(x566))) -5|[]-> b(c(c(x566)))
   c(c(a(x567))) <-8|0[]- c(a(c(x567))) -9|[]-> a(a(c(x567)))
   a(c(a(x568))) <-8|0[]- a(a(c(x568))) -10|[]-> c(b(c(x568)))
   a(a(a(x569))) <-9|0[]- a(c(a(x569))) -2|[]-> b(c(a(x569)))
   b(a(a(x570))) <-9|0[]- b(c(a(x570))) -3|[]-> b(a(a(x570)))
   b(a(a(x571))) <-9|0[]- b(c(a(x571))) -6|[]-> a(c(a(x571)))
   a(a(a(x572))) <-9|0[]- a(c(a(x572))) -8|[]-> c(a(a(x572)))
   c(a(a(x573))) <-9|0[]- c(c(a(x573))) -13|[]-> b(b(a(x573)))
   c(a(a(x574))) <-9|0[]- c(c(a(x574))) -15|[]-> a(a(a(x574)))
   c(b(x)) <-10|[]- a(a(x)) -4|[]-> b(a(x))
   a(c(b(x576))) <-10|0[]- a(a(a(x576))) -4|[]-> b(a(a(x576)))
   c(b(x)) <-10|[]- a(a(x)) -5|[]-> b(c(x))
   a(c(b(x578))) <-10|0[]- a(a(a(x578))) -5|[]-> b(c(a(x578)))
   c(c(b(x579))) <-10|0[]- c(a(a(x579))) -9|[]-> a(a(a(x579)))
   a(c(b(x580))) <-10|0[]- a(a(a(x580))) -10|[]-> c(b(a(x580)))
   a(c(b(x581))) <-11|0[]- a(b(b(x581))) -0|[]-> a(a(b(x581)))
   c(c(b(x582))) <-11|0[]- c(b(b(x582))) -1|[]-> b(c(b(x582)))
   c(c(b(x583))) <-11|0[]- c(b(b(x583))) -7|[]-> a(c(b(x583)))
   b(c(b(x584))) <-11|0[]- b(b(b(x584))) -11|[]-> c(b(b(x584)))
   c(c(b(x585))) <-11|0[]- c(b(b(x585))) -12|[]-> c(c(b(x585)))
   c(b(x)) <-11|[]- b(b(x)) -14|[]-> c(c(x))
   b(c(b(x587))) <-11|0[]- b(b(b(x587))) -14|[]-> c(c(b(x587)))
   c(c(x)) <-12|[]- c(b(x)) -1|[]-> b(c(x))
   a(c(c(x589))) <-12|0[]- a(c(b(x589))) -2|[]-> b(c(b(x589)))
   b(c(c(x590))) <-12|0[]- b(c(b(x590))) -3|[]-> b(a(b(x590)))
   b(c(c(x591))) <-12|0[]- b(c(b(x591))) -6|[]-> a(c(b(x591)))
   c(c(x)) <-12|[]- c(b(x)) -7|[]-> a(c(x))
   a(c(c(x593))) <-12|0[]- a(c(b(x593))) -8|[]-> c(a(b(x593)))
   c(c(c(x594))) <-12|0[]- c(c(b(x594))) -13|[]-> b(b(b(x594)))
   c(c(c(x595))) <-12|0[]- c(c(b(x595))) -15|[]-> a(a(b(x595)))
   a(b(b(x596))) <-13|0[]- a(c(c(x596))) -2|[]-> b(c(c(x596)))
   b(b(b(x597))) <-13|0[]- b(c(c(x597))) -3|[]-> b(a(c(x597)))
   b(b(b(x598))) <-13|0[]- b(c(c(x598))) -6|[]-> a(c(c(x598)))
   a(b(b(x599))) <-13|0[]- a(c(c(x599))) -8|[]-> c(a(c(x599)))
   c(b(b(x600))) <-13|0[]- c(c(c(x600))) -13|[]-> b(b(c(x600)))
   b(b(x)) <-13|[]- c(c(x)) -15|[]-> a(a(x))
   c(b(b(x602))) <-13|0[]- c(c(c(x602))) -15|[]-> a(a(c(x602)))
   a(c(c(x603))) <-14|0[]- a(b(b(x603))) -0|[]-> a(a(b(x603)))
   c(c(c(x604))) <-14|0[]- c(b(b(x604))) -1|[]-> b(c(b(x604)))
   c(c(c(x605))) <-14|0[]- c(b(b(x605))) -7|[]-> a(c(b(x605)))
   c(c(x)) <-14|[]- b(b(x)) -11|[]-> c(b(x))
   b(c(c(x607))) <-14|0[]- b(b(b(x607))) -11|[]-> c(b(b(x607)))
   c(c(c(x608))) <-14|0[]- c(b(b(x608))) -12|[]-> c(c(b(x608)))
   b(c(c(x609))) <-14|0[]- b(b(b(x609))) -14|[]-> c(c(b(x609)))
   a(a(a(x610))) <-15|0[]- a(c(c(x610))) -2|[]-> b(c(c(x610)))
   b(a(a(x611))) <-15|0[]- b(c(c(x611))) -3|[]-> b(a(c(x611)))
   b(a(a(x612))) <-15|0[]- b(c(c(x612))) -6|[]-> a(c(c(x612)))
   a(a(a(x613))) <-15|0[]- a(c(c(x613))) -8|[]-> c(a(c(x613)))
   a(a(x)) <-15|[]- c(c(x)) -13|[]-> b(b(x))
   c(a(a(x615))) <-15|0[]- c(c(c(x615))) -13|[]-> b(b(c(x615)))
   c(a(a(x616))) <-15|0[]- c(c(c(x616))) -15|[]-> a(a(c(x616)))
  Redundant Rules Transformation:
   a(b(x)) -> a(a(x))
   c(b(x)) -> b(c(x))
   a(c(x)) -> b(c(x))
   b(c(x)) -> b(a(x))
   a(a(x)) -> b(a(x))
   a(a(x)) -> b(c(x))
   b(c(x)) -> a(c(x))
   c(b(x)) -> a(c(x))
   a(c(x)) -> c(a(x))
   c(a(x)) -> a(a(x))
   a(a(x)) -> c(b(x))
   b(b(x)) -> c(b(x))
   c(b(x)) -> c(c(x))
   c(c(x)) -> b(b(x))
   b(b(x)) -> c(c(x))
   c(c(x)) -> a(a(x))
   a(b(x)) -> b(a(x))
   a(b(x)) -> b(c(x))
   a(b(x)) -> c(b(x))
   c(b(x)) -> b(a(x))
   a(c(x)) -> b(a(x))
   a(c(x)) -> a(c(x))
   a(a(x)) -> a(c(x))
   b(c(x)) -> b(c(x))
   b(c(x)) -> c(a(x))
   c(b(x)) -> c(a(x))
   a(c(x)) -> a(a(x))
   c(a(x)) -> b(a(x))
   c(a(x)) -> b(c(x))
   c(a(x)) -> c(b(x))
   a(a(x)) -> c(c(x))
   b(b(x)) -> b(c(x))
   b(b(x)) -> a(c(x))
   c(b(x)) -> b(b(x))
   c(b(x)) -> a(a(x))
   c(c(x)) -> c(b(x))
   c(c(x)) -> c(c(x))
   b(b(x)) -> b(b(x))
   b(b(x)) -> a(a(x))
   c(c(x)) -> b(a(x))
   c(c(x)) -> b(c(x))
   Church Rosser Transformation Processor (no redundant rules):
    strict:
     
    weak:
     
    critical peaks: 581
     c(b(c(x3355))) <-0|0[]- c(c(c(x3355))) -0|[]-> b(c(c(x3355)))
     b(c(x)) <-0|[]- c(c(x)) -1|[]-> b(a(x))
     c(b(c(x3357))) <-0|0[]- c(c(c(x3357))) -1|[]-> b(a(c(x3357)))
     b(c(x)) <-0|[]- c(c(x)) -3|[]-> c(b(x))
     c(b(c(x3359))) <-0|0[]- c(c(c(x3359))) -3|[]-> c(b(c(x3359)))
     a(b(c(x3360))) <-0|0[]- a(c(c(x3360))) -12|[]-> a(a(c(x3360)))
     b(b(c(x3361))) <-0|0[]- b(c(c(x3361))) -14|[]-> c(a(c(x3361)))
     a(b(c(x3362))) <-0|0[]- a(c(c(x3362))) -16|[]-> b(a(c(x3362)))
     b(c(x)) <-0|[]- c(c(x)) -21|[]-> a(a(x))
     c(b(c(x3364))) <-0|0[]- c(c(c(x3364))) -21|[]-> a(a(c(x3364)))
     b(c(x)) <-0|[]- c(c(x)) -23|[]-> b(b(x))
     c(b(c(x3366))) <-0|0[]- c(c(c(x3366))) -23|[]-> b(b(c(x3366)))
     a(b(c(x3367))) <-0|0[]- a(c(c(x3367))) -28|[]-> c(a(c(x3367)))
     b(b(c(x3368))) <-0|0[]- b(c(c(x3368))) -30|[]-> a(c(c(x3368)))
     b(b(c(x3369))) <-0|0[]- b(c(c(x3369))) -33|[]-> b(a(c(x3369)))
     a(b(c(x3370))) <-0|0[]- a(c(c(x3370))) -34|[]-> b(c(c(x3370)))
     b(a(x)) <-1|[]- c(c(x)) -0|[]-> b(c(x))
     c(b(a(x3372))) <-1|0[]- c(c(c(x3372))) -0|[]-> b(c(c(x3372)))
     c(b(a(x3373))) <-1|0[]- c(c(c(x3373))) -1|[]-> b(a(c(x3373)))
     b(a(x)) <-1|[]- c(c(x)) -3|[]-> c(b(x))
     c(b(a(x3375))) <-1|0[]- c(c(c(x3375))) -3|[]-> c(b(c(x3375)))
     a(b(a(x3376))) <-1|0[]- a(c(c(x3376))) -12|[]-> a(a(c(x3376)))
     b(b(a(x3377))) <-1|0[]- b(c(c(x3377))) -14|[]-> c(a(c(x3377)))
     a(b(a(x3378))) <-1|0[]- a(c(c(x3378))) -16|[]-> b(a(c(x3378)))
     b(a(x)) <-1|[]- c(c(x)) -21|[]-> a(a(x))
     c(b(a(x3380))) <-1|0[]- c(c(c(x3380))) -21|[]-> a(a(c(x3380)))
     b(a(x)) <-1|[]- c(c(x)) -23|[]-> b(b(x))
     c(b(a(x3382))) <-1|0[]- c(c(c(x3382))) -23|[]-> b(b(c(x3382)))
     a(b(a(x3383))) <-1|0[]- a(c(c(x3383))) -28|[]-> c(a(c(x3383)))
     b(b(a(x3384))) <-1|0[]- b(c(c(x3384))) -30|[]-> a(c(c(x3384)))
     b(b(a(x3385))) <-1|0[]- b(c(c(x3385))) -33|[]-> b(a(c(x3385)))
     a(b(a(x3386))) <-1|0[]- a(c(c(x3386))) -34|[]-> b(c(c(x3386)))
     b(a(a(x3387))) <-2|0[]- b(b(b(x3387))) -2|[]-> a(a(b(x3387)))
     c(a(a(x3388))) <-2|0[]- c(b(b(x3388))) -4|[]-> a(a(b(x3388)))
     c(a(a(x3389))) <-2|0[]- c(b(b(x3389))) -5|[]-> b(b(b(x3389)))
     a(a(x)) <-2|[]- b(b(x)) -6|[]-> a(c(x))
     b(a(a(x3391))) <-2|0[]- b(b(b(x3391))) -6|[]-> a(c(b(x3391)))
     a(a(x)) <-2|[]- b(b(x)) -7|[]-> b(c(x))
     b(a(a(x3393))) <-2|0[]- b(b(b(x3393))) -7|[]-> b(c(b(x3393)))
     c(a(a(x3394))) <-2|0[]- c(b(b(x3394))) -13|[]-> c(a(b(x3394)))
     c(a(a(x3395))) <-2|0[]- c(b(b(x3395))) -17|[]-> b(a(b(x3395)))
     a(a(a(x3396))) <-2|0[]- a(b(b(x3396))) -18|[]-> c(b(b(x3396)))
     a(a(a(x3397))) <-2|0[]- a(b(b(x3397))) -19|[]-> b(c(b(x3397)))
     a(a(a(x3398))) <-2|0[]- a(b(b(x3398))) -20|[]-> b(a(b(x3398)))
     a(a(x)) <-2|[]- b(b(x)) -22|[]-> c(c(x))
     b(a(a(x3400))) <-2|0[]- b(b(b(x3400))) -22|[]-> c(c(b(x3400)))
     c(a(a(x3401))) <-2|0[]- c(b(b(x3401))) -24|[]-> c(c(b(x3401)))
     a(a(x)) <-2|[]- b(b(x)) -25|[]-> c(b(x))
     b(a(a(x3403))) <-2|0[]- b(b(b(x3403))) -25|[]-> c(b(b(x3403)))
     c(a(a(x3404))) <-2|0[]- c(b(b(x3404))) -29|[]-> a(c(b(x3404)))
     c(a(a(x3405))) <-2|0[]- c(b(b(x3405))) -35|[]-> b(c(b(x3405)))
     a(a(a(x3406))) <-2|0[]- a(b(b(x3406))) -36|[]-> a(a(b(x3406)))
     c(b(x)) <-3|[]- c(c(x)) -0|[]-> b(c(x))
     c(c(b(x3408))) <-3|0[]- c(c(c(x3408))) -0|[]-> b(c(c(x3408)))
     c(b(x)) <-3|[]- c(c(x)) -1|[]-> b(a(x))
     c(c(b(x3410))) <-3|0[]- c(c(c(x3410))) -1|[]-> b(a(c(x3410)))
     c(c(b(x3411))) <-3|0[]- c(c(c(x3411))) -3|[]-> c(b(c(x3411)))
     a(c(b(x3412))) <-3|0[]- a(c(c(x3412))) -12|[]-> a(a(c(x3412)))
     b(c(b(x3413))) <-3|0[]- b(c(c(x3413))) -14|[]-> c(a(c(x3413)))
     a(c(b(x3414))) <-3|0[]- a(c(c(x3414))) -16|[]-> b(a(c(x3414)))
     c(b(x)) <-3|[]- c(c(x)) -21|[]-> a(a(x))
     c(c(b(x3416))) <-3|0[]- c(c(c(x3416))) -21|[]-> a(a(c(x3416)))
     c(b(x)) <-3|[]- c(c(x)) -23|[]-> b(b(x))
     c(c(b(x3418))) <-3|0[]- c(c(c(x3418))) -23|[]-> b(b(c(x3418)))
     a(c(b(x3419))) <-3|0[]- a(c(c(x3419))) -28|[]-> c(a(c(x3419)))
     b(c(b(x3420))) <-3|0[]- b(c(c(x3420))) -30|[]-> a(c(c(x3420)))
     b(c(b(x3421))) <-3|0[]- b(c(c(x3421))) -33|[]-> b(a(c(x3421)))
     a(c(b(x3422))) <-3|0[]- a(c(c(x3422))) -34|[]-> b(c(c(x3422)))
     c(a(a(x3423))) <-4|0[]- c(c(b(x3423))) -0|[]-> b(c(b(x3423)))
     c(a(a(x3424))) <-4|0[]- c(c(b(x3424))) -1|[]-> b(a(b(x3424)))
     c(a(a(x3425))) <-4|0[]- c(c(b(x3425))) -3|[]-> c(b(b(x3425)))
     a(a(x)) <-4|[]- c(b(x)) -5|[]-> b(b(x))
     a(a(a(x3427))) <-4|0[]- a(c(b(x3427))) -12|[]-> a(a(b(x3427)))
     a(a(x)) <-4|[]- c(b(x)) -13|[]-> c(a(x))
     b(a(a(x3429))) <-4|0[]- b(c(b(x3429))) -14|[]-> c(a(b(x3429)))
     a(a(a(x3430))) <-4|0[]- a(c(b(x3430))) -16|[]-> b(a(b(x3430)))
     a(a(x)) <-4|[]- c(b(x)) -17|[]-> b(a(x))
     c(a(a(x3432))) <-4|0[]- c(c(b(x3432))) -21|[]-> a(a(b(x3432)))
     c(a(a(x3433))) <-4|0[]- c(c(b(x3433))) -23|[]-> b(b(b(x3433)))
     a(a(x)) <-4|[]- c(b(x)) -24|[]-> c(c(x))
     a(a(a(x3435))) <-4|0[]- a(c(b(x3435))) -28|[]-> c(a(b(x3435)))
     a(a(x)) <-4|[]- c(b(x)) -29|[]-> a(c(x))
     b(a(a(x3437))) <-4|0[]- b(c(b(x3437))) -30|[]-> a(c(b(x3437)))
     b(a(a(x3438))) <-4|0[]- b(c(b(x3438))) -33|[]-> b(a(b(x3438)))
     a(a(a(x3439))) <-4|0[]- a(c(b(x3439))) -34|[]-> b(c(b(x3439)))
     a(a(x)) <-4|[]- c(b(x)) -35|[]-> b(c(x))
     c(b(b(x3441))) <-5|0[]- c(c(b(x3441))) -0|[]-> b(c(b(x3441)))
     c(b(b(x3442))) <-5|0[]- c(c(b(x3442))) -1|[]-> b(a(b(x3442)))
     c(b(b(x3443))) <-5|0[]- c(c(b(x3443))) -3|[]-> c(b(b(x3443)))
     b(b(x)) <-5|[]- c(b(x)) -4|[]-> a(a(x))
     a(b(b(x3445))) <-5|0[]- a(c(b(x3445))) -12|[]-> a(a(b(x3445)))
     b(b(x)) <-5|[]- c(b(x)) -13|[]-> c(a(x))
     b(b(b(x3447))) <-5|0[]- b(c(b(x3447))) -14|[]-> c(a(b(x3447)))
     a(b(b(x3448))) <-5|0[]- a(c(b(x3448))) -16|[]-> b(a(b(x3448)))
     b(b(x)) <-5|[]- c(b(x)) -17|[]-> b(a(x))
     c(b(b(x3450))) <-5|0[]- c(c(b(x3450))) -21|[]-> a(a(b(x3450)))
     c(b(b(x3451))) <-5|0[]- c(c(b(x3451))) -23|[]-> b(b(b(x3451)))
     b(b(x)) <-5|[]- c(b(x)) -24|[]-> c(c(x))
     a(b(b(x3453))) <-5|0[]- a(c(b(x3453))) -28|[]-> c(a(b(x3453)))
     b(b(x)) <-5|[]- c(b(x)) -29|[]-> a(c(x))
     b(b(b(x3455))) <-5|0[]- b(c(b(x3455))) -30|[]-> a(c(b(x3455)))
     b(b(b(x3456))) <-5|0[]- b(c(b(x3456))) -33|[]-> b(a(b(x3456)))
     a(b(b(x3457))) <-5|0[]- a(c(b(x3457))) -34|[]-> b(c(b(x3457)))
     b(b(x)) <-5|[]- c(b(x)) -35|[]-> b(c(x))
     a(c(x)) <-6|[]- b(b(x)) -2|[]-> a(a(x))
     b(a(c(x3460))) <-6|0[]- b(b(b(x3460))) -2|[]-> a(a(b(x3460)))
     c(a(c(x3461))) <-6|0[]- c(b(b(x3461))) -4|[]-> a(a(b(x3461)))
     c(a(c(x3462))) <-6|0[]- c(b(b(x3462))) -5|[]-> b(b(b(x3462)))
     b(a(c(x3463))) <-6|0[]- b(b(b(x3463))) -6|[]-> a(c(b(x3463)))
     a(c(x)) <-6|[]- b(b(x)) -7|[]-> b(c(x))
     b(a(c(x3465))) <-6|0[]- b(b(b(x3465))) -7|[]-> b(c(b(x3465)))
     c(a(c(x3466))) <-6|0[]- c(b(b(x3466))) -13|[]-> c(a(b(x3466)))
     c(a(c(x3467))) <-6|0[]- c(b(b(x3467))) -17|[]-> b(a(b(x3467)))
     a(a(c(x3468))) <-6|0[]- a(b(b(x3468))) -18|[]-> c(b(b(x3468)))
     a(a(c(x3469))) <-6|0[]- a(b(b(x3469))) -19|[]-> b(c(b(x3469)))
     a(a(c(x3470))) <-6|0[]- a(b(b(x3470))) -20|[]-> b(a(b(x3470)))
     a(c(x)) <-6|[]- b(b(x)) -22|[]-> c(c(x))
     b(a(c(x3472))) <-6|0[]- b(b(b(x3472))) -22|[]-> c(c(b(x3472)))
     c(a(c(x3473))) <-6|0[]- c(b(b(x3473))) -24|[]-> c(c(b(x3473)))
     a(c(x)) <-6|[]- b(b(x)) -25|[]-> c(b(x))
     b(a(c(x3475))) <-6|0[]- b(b(b(x3475))) -25|[]-> c(b(b(x3475)))
     c(a(c(x3476))) <-6|0[]- c(b(b(x3476))) -29|[]-> a(c(b(x3476)))
     c(a(c(x3477))) <-6|0[]- c(b(b(x3477))) -35|[]-> b(c(b(x3477)))
     a(a(c(x3478))) <-6|0[]- a(b(b(x3478))) -36|[]-> a(a(b(x3478)))
     b(c(x)) <-7|[]- b(b(x)) -2|[]-> a(a(x))
     b(b(c(x3480))) <-7|0[]- b(b(b(x3480))) -2|[]-> a(a(b(x3480)))
     c(b(c(x3481))) <-7|0[]- c(b(b(x3481))) -4|[]-> a(a(b(x3481)))
     c(b(c(x3482))) <-7|0[]- c(b(b(x3482))) -5|[]-> b(b(b(x3482)))
     b(c(x)) <-7|[]- b(b(x)) -6|[]-> a(c(x))
     b(b(c(x3484))) <-7|0[]- b(b(b(x3484))) -6|[]-> a(c(b(x3484)))
     b(b(c(x3485))) <-7|0[]- b(b(b(x3485))) -7|[]-> b(c(b(x3485)))
     c(b(c(x3486))) <-7|0[]- c(b(b(x3486))) -13|[]-> c(a(b(x3486)))
     c(b(c(x3487))) <-7|0[]- c(b(b(x3487))) -17|[]-> b(a(b(x3487)))
     a(b(c(x3488))) <-7|0[]- a(b(b(x3488))) -18|[]-> c(b(b(x3488)))
     a(b(c(x3489))) <-7|0[]- a(b(b(x3489))) -19|[]-> b(c(b(x3489)))
     a(b(c(x3490))) <-7|0[]- a(b(b(x3490))) -20|[]-> b(a(b(x3490)))
     b(c(x)) <-7|[]- b(b(x)) -22|[]-> c(c(x))
     b(b(c(x3492))) <-7|0[]- b(b(b(x3492))) -22|[]-> c(c(b(x3492)))
     c(b(c(x3493))) <-7|0[]- c(b(b(x3493))) -24|[]-> c(c(b(x3493)))
     b(c(x)) <-7|[]- b(b(x)) -25|[]-> c(b(x))
     b(b(c(x3495))) <-7|0[]- b(b(b(x3495))) -25|[]-> c(b(b(x3495)))
     c(b(c(x3496))) <-7|0[]- c(b(b(x3496))) -29|[]-> a(c(b(x3496)))
     c(b(c(x3497))) <-7|0[]- c(b(b(x3497))) -35|[]-> b(c(b(x3497)))
     a(b(c(x3498))) <-7|0[]- a(b(b(x3498))) -36|[]-> a(a(b(x3498)))
     a(c(c(x3499))) <-8|0[]- a(a(a(x3499))) -8|[]-> c(c(a(x3499)))
     c(c(c(x3500))) <-8|0[]- c(a(a(x3500))) -9|[]-> c(b(a(x3500)))
     c(c(c(x3501))) <-8|0[]- c(a(a(x3501))) -10|[]-> b(c(a(x3501)))
     c(c(c(x3502))) <-8|0[]- c(a(a(x3502))) -11|[]-> b(a(a(x3502)))
     c(c(x)) <-8|[]- a(a(x)) -15|[]-> a(c(x))
     a(c(c(x3504))) <-8|0[]- a(a(a(x3504))) -15|[]-> a(c(a(x3504)))
     c(c(x)) <-8|[]- a(a(x)) -26|[]-> c(b(x))
     a(c(c(x3506))) <-8|0[]- a(a(a(x3506))) -26|[]-> c(b(a(x3506)))
     c(c(c(x3507))) <-8|0[]- c(a(a(x3507))) -27|[]-> a(a(a(x3507)))
     c(c(x)) <-8|[]- a(a(x)) -31|[]-> b(c(x))
     a(c(c(x3509))) <-8|0[]- a(a(a(x3509))) -31|[]-> b(c(a(x3509)))
     c(c(x)) <-8|[]- a(a(x)) -32|[]-> b(a(x))
     a(c(c(x3511))) <-8|0[]- a(a(a(x3511))) -32|[]-> b(a(a(x3511)))
     c(c(b(x3512))) <-9|0[]- c(c(a(x3512))) -0|[]-> b(c(a(x3512)))
     c(c(b(x3513))) <-9|0[]- c(c(a(x3513))) -1|[]-> b(a(a(x3513)))
     c(c(b(x3514))) <-9|0[]- c(c(a(x3514))) -3|[]-> c(b(a(x3514)))
     c(b(x)) <-9|[]- c(a(x)) -10|[]-> b(c(x))
     c(b(x)) <-9|[]- c(a(x)) -11|[]-> b(a(x))
     a(c(b(x3517))) <-9|0[]- a(c(a(x3517))) -12|[]-> a(a(a(x3517)))
     b(c(b(x3518))) <-9|0[]- b(c(a(x3518))) -14|[]-> c(a(a(x3518)))
     a(c(b(x3519))) <-9|0[]- a(c(a(x3519))) -16|[]-> b(a(a(x3519)))
     c(c(b(x3520))) <-9|0[]- c(c(a(x3520))) -21|[]-> a(a(a(x3520)))
     c(c(b(x3521))) <-9|0[]- c(c(a(x3521))) -23|[]-> b(b(a(x3521)))
     c(b(x)) <-9|[]- c(a(x)) -27|[]-> a(a(x))
     a(c(b(x3523))) <-9|0[]- a(c(a(x3523))) -28|[]-> c(a(a(x3523)))
     b(c(b(x3524))) <-9|0[]- b(c(a(x3524))) -30|[]-> a(c(a(x3524)))
     b(c(b(x3525))) <-9|0[]- b(c(a(x3525))) -33|[]-> b(a(a(x3525)))
     a(c(b(x3526))) <-9|0[]- a(c(a(x3526))) -34|[]-> b(c(a(x3526)))
     c(b(c(x3527))) <-10|0[]- c(c(a(x3527))) -0|[]-> b(c(a(x3527)))
     c(b(c(x3528))) <-10|0[]- c(c(a(x3528))) -1|[]-> b(a(a(x3528)))
     c(b(c(x3529))) <-10|0[]- c(c(a(x3529))) -3|[]-> c(b(a(x3529)))
     b(c(x)) <-10|[]- c(a(x)) -9|[]-> c(b(x))
     b(c(x)) <-10|[]- c(a(x)) -11|[]-> b(a(x))
     a(b(c(x3532))) <-10|0[]- a(c(a(x3532))) -12|[]-> a(a(a(x3532)))
     b(b(c(x3533))) <-10|0[]- b(c(a(x3533))) -14|[]-> c(a(a(x3533)))
     a(b(c(x3534))) <-10|0[]- a(c(a(x3534))) -16|[]-> b(a(a(x3534)))
     c(b(c(x3535))) <-10|0[]- c(c(a(x3535))) -21|[]-> a(a(a(x3535)))
     c(b(c(x3536))) <-10|0[]- c(c(a(x3536))) -23|[]-> b(b(a(x3536)))
     b(c(x)) <-10|[]- c(a(x)) -27|[]-> a(a(x))
     a(b(c(x3538))) <-10|0[]- a(c(a(x3538))) -28|[]-> c(a(a(x3538)))
     b(b(c(x3539))) <-10|0[]- b(c(a(x3539))) -30|[]-> a(c(a(x3539)))
     b(b(c(x3540))) <-10|0[]- b(c(a(x3540))) -33|[]-> b(a(a(x3540)))
     a(b(c(x3541))) <-10|0[]- a(c(a(x3541))) -34|[]-> b(c(a(x3541)))
     c(b(a(x3542))) <-11|0[]- c(c(a(x3542))) -0|[]-> b(c(a(x3542)))
     c(b(a(x3543))) <-11|0[]- c(c(a(x3543))) -1|[]-> b(a(a(x3543)))
     c(b(a(x3544))) <-11|0[]- c(c(a(x3544))) -3|[]-> c(b(a(x3544)))
     b(a(x)) <-11|[]- c(a(x)) -9|[]-> c(b(x))
     b(a(x)) <-11|[]- c(a(x)) -10|[]-> b(c(x))
     a(b(a(x3547))) <-11|0[]- a(c(a(x3547))) -12|[]-> a(a(a(x3547)))
     b(b(a(x3548))) <-11|0[]- b(c(a(x3548))) -14|[]-> c(a(a(x3548)))
     a(b(a(x3549))) <-11|0[]- a(c(a(x3549))) -16|[]-> b(a(a(x3549)))
     c(b(a(x3550))) <-11|0[]- c(c(a(x3550))) -21|[]-> a(a(a(x3550)))
     c(b(a(x3551))) <-11|0[]- c(c(a(x3551))) -23|[]-> b(b(a(x3551)))
     b(a(x)) <-11|[]- c(a(x)) -27|[]-> a(a(x))
     a(b(a(x3553))) <-11|0[]- a(c(a(x3553))) -28|[]-> c(a(a(x3553)))
     b(b(a(x3554))) <-11|0[]- b(c(a(x3554))) -30|[]-> a(c(a(x3554)))
     b(b(a(x3555))) <-11|0[]- b(c(a(x3555))) -33|[]-> b(a(a(x3555)))
     a(b(a(x3556))) <-11|0[]- a(c(a(x3556))) -34|[]-> b(c(a(x3556)))
     a(a(a(x3557))) <-12|0[]- a(a(c(x3557))) -8|[]-> c(c(c(x3557)))
     c(a(a(x3558))) <-12|0[]- c(a(c(x3558))) -9|[]-> c(b(c(x3558)))
     c(a(a(x3559))) <-12|0[]- c(a(c(x3559))) -10|[]-> b(c(c(x3559)))
     c(a(a(x3560))) <-12|0[]- c(a(c(x3560))) -11|[]-> b(a(c(x3560)))
     a(a(a(x3561))) <-12|0[]- a(a(c(x3561))) -15|[]-> a(c(c(x3561)))
     a(a(x)) <-12|[]- a(c(x)) -16|[]-> b(a(x))
     a(a(a(x3563))) <-12|0[]- a(a(c(x3563))) -26|[]-> c(b(c(x3563)))
     c(a(a(x3564))) <-12|0[]- c(a(c(x3564))) -27|[]-> a(a(c(x3564)))
     a(a(x)) <-12|[]- a(c(x)) -28|[]-> c(a(x))
     a(a(a(x3566))) <-12|0[]- a(a(c(x3566))) -31|[]-> b(c(c(x3566)))
     a(a(a(x3567))) <-12|0[]- a(a(c(x3567))) -32|[]-> b(a(c(x3567)))
     a(a(x)) <-12|[]- a(c(x)) -34|[]-> b(c(x))
     c(c(a(x3569))) <-13|0[]- c(c(b(x3569))) -0|[]-> b(c(b(x3569)))
     c(c(a(x3570))) <-13|0[]- c(c(b(x3570))) -1|[]-> b(a(b(x3570)))
     c(c(a(x3571))) <-13|0[]- c(c(b(x3571))) -3|[]-> c(b(b(x3571)))
     c(a(x)) <-13|[]- c(b(x)) -4|[]-> a(a(x))
     c(a(x)) <-13|[]- c(b(x)) -5|[]-> b(b(x))
     a(c(a(x3574))) <-13|0[]- a(c(b(x3574))) -12|[]-> a(a(b(x3574)))
     b(c(a(x3575))) <-13|0[]- b(c(b(x3575))) -14|[]-> c(a(b(x3575)))
     a(c(a(x3576))) <-13|0[]- a(c(b(x3576))) -16|[]-> b(a(b(x3576)))
     c(a(x)) <-13|[]- c(b(x)) -17|[]-> b(a(x))
     c(c(a(x3578))) <-13|0[]- c(c(b(x3578))) -21|[]-> a(a(b(x3578)))
     c(c(a(x3579))) <-13|0[]- c(c(b(x3579))) -23|[]-> b(b(b(x3579)))
     c(a(x)) <-13|[]- c(b(x)) -24|[]-> c(c(x))
     a(c(a(x3581))) <-13|0[]- a(c(b(x3581))) -28|[]-> c(a(b(x3581)))
     c(a(x)) <-13|[]- c(b(x)) -29|[]-> a(c(x))
     b(c(a(x3583))) <-13|0[]- b(c(b(x3583))) -30|[]-> a(c(b(x3583)))
     b(c(a(x3584))) <-13|0[]- b(c(b(x3584))) -33|[]-> b(a(b(x3584)))
     a(c(a(x3585))) <-13|0[]- a(c(b(x3585))) -34|[]-> b(c(b(x3585)))
     c(a(x)) <-13|[]- c(b(x)) -35|[]-> b(c(x))
     b(c(a(x3587))) <-14|0[]- b(b(c(x3587))) -2|[]-> a(a(c(x3587)))
     c(c(a(x3588))) <-14|0[]- c(b(c(x3588))) -4|[]-> a(a(c(x3588)))
     c(c(a(x3589))) <-14|0[]- c(b(c(x3589))) -5|[]-> b(b(c(x3589)))
     b(c(a(x3590))) <-14|0[]- b(b(c(x3590))) -6|[]-> a(c(c(x3590)))
     b(c(a(x3591))) <-14|0[]- b(b(c(x3591))) -7|[]-> b(c(c(x3591)))
     c(c(a(x3592))) <-14|0[]- c(b(c(x3592))) -13|[]-> c(a(c(x3592)))
     c(c(a(x3593))) <-14|0[]- c(b(c(x3593))) -17|[]-> b(a(c(x3593)))
     a(c(a(x3594))) <-14|0[]- a(b(c(x3594))) -18|[]-> c(b(c(x3594)))
     a(c(a(x3595))) <-14|0[]- a(b(c(x3595))) -19|[]-> b(c(c(x3595)))
     a(c(a(x3596))) <-14|0[]- a(b(c(x3596))) -20|[]-> b(a(c(x3596)))
     b(c(a(x3597))) <-14|0[]- b(b(c(x3597))) -22|[]-> c(c(c(x3597)))
     c(c(a(x3598))) <-14|0[]- c(b(c(x3598))) -24|[]-> c(c(c(x3598)))
     b(c(a(x3599))) <-14|0[]- b(b(c(x3599))) -25|[]-> c(b(c(x3599)))
     c(c(a(x3600))) <-14|0[]- c(b(c(x3600))) -29|[]-> a(c(c(x3600)))
     c(a(x)) <-14|[]- b(c(x)) -30|[]-> a(c(x))
     c(a(x)) <-14|[]- b(c(x)) -33|[]-> b(a(x))
     c(c(a(x3603))) <-14|0[]- c(b(c(x3603))) -35|[]-> b(c(c(x3603)))
     a(c(a(x3604))) <-14|0[]- a(b(c(x3604))) -36|[]-> a(a(c(x3604)))
     a(c(x)) <-15|[]- a(a(x)) -8|[]-> c(c(x))
     a(a(c(x3606))) <-15|0[]- a(a(a(x3606))) -8|[]-> c(c(a(x3606)))
     c(a(c(x3607))) <-15|0[]- c(a(a(x3607))) -9|[]-> c(b(a(x3607)))
     c(a(c(x3608))) <-15|0[]- c(a(a(x3608))) -10|[]-> b(c(a(x3608)))
     c(a(c(x3609))) <-15|0[]- c(a(a(x3609))) -11|[]-> b(a(a(x3609)))
     a(a(c(x3610))) <-15|0[]- a(a(a(x3610))) -15|[]-> a(c(a(x3610)))
     a(c(x)) <-15|[]- a(a(x)) -26|[]-> c(b(x))
     a(a(c(x3612))) <-15|0[]- a(a(a(x3612))) -26|[]-> c(b(a(x3612)))
     c(a(c(x3613))) <-15|0[]- c(a(a(x3613))) -27|[]-> a(a(a(x3613)))
     a(c(x)) <-15|[]- a(a(x)) -31|[]-> b(c(x))
     a(a(c(x3615))) <-15|0[]- a(a(a(x3615))) -31|[]-> b(c(a(x3615)))
     a(c(x)) <-15|[]- a(a(x)) -32|[]-> b(a(x))
     a(a(c(x3617))) <-15|0[]- a(a(a(x3617))) -32|[]-> b(a(a(x3617)))
     a(b(a(x3618))) <-16|0[]- a(a(c(x3618))) -8|[]-> c(c(c(x3618)))
     c(b(a(x3619))) <-16|0[]- c(a(c(x3619))) -9|[]-> c(b(c(x3619)))
     c(b(a(x3620))) <-16|0[]- c(a(c(x3620))) -10|[]-> b(c(c(x3620)))
     c(b(a(x3621))) <-16|0[]- c(a(c(x3621))) -11|[]-> b(a(c(x3621)))
     b(a(x)) <-16|[]- a(c(x)) -12|[]-> a(a(x))
     a(b(a(x3623))) <-16|0[]- a(a(c(x3623))) -15|[]-> a(c(c(x3623)))
     a(b(a(x3624))) <-16|0[]- a(a(c(x3624))) -26|[]-> c(b(c(x3624)))
     c(b(a(x3625))) <-16|0[]- c(a(c(x3625))) -27|[]-> a(a(c(x3625)))
     b(a(x)) <-16|[]- a(c(x)) -28|[]-> c(a(x))
     a(b(a(x3627))) <-16|0[]- a(a(c(x3627))) -31|[]-> b(c(c(x3627)))
     a(b(a(x3628))) <-16|0[]- a(a(c(x3628))) -32|[]-> b(a(c(x3628)))
     b(a(x)) <-16|[]- a(c(x)) -34|[]-> b(c(x))
     c(b(a(x3630))) <-17|0[]- c(c(b(x3630))) -0|[]-> b(c(b(x3630)))
     c(b(a(x3631))) <-17|0[]- c(c(b(x3631))) -1|[]-> b(a(b(x3631)))
     c(b(a(x3632))) <-17|0[]- c(c(b(x3632))) -3|[]-> c(b(b(x3632)))
     b(a(x)) <-17|[]- c(b(x)) -4|[]-> a(a(x))
     b(a(x)) <-17|[]- c(b(x)) -5|[]-> b(b(x))
     a(b(a(x3635))) <-17|0[]- a(c(b(x3635))) -12|[]-> a(a(b(x3635)))
     b(a(x)) <-17|[]- c(b(x)) -13|[]-> c(a(x))
     b(b(a(x3637))) <-17|0[]- b(c(b(x3637))) -14|[]-> c(a(b(x3637)))
     a(b(a(x3638))) <-17|0[]- a(c(b(x3638))) -16|[]-> b(a(b(x3638)))
     c(b(a(x3639))) <-17|0[]- c(c(b(x3639))) -21|[]-> a(a(b(x3639)))
     c(b(a(x3640))) <-17|0[]- c(c(b(x3640))) -23|[]-> b(b(b(x3640)))
     b(a(x)) <-17|[]- c(b(x)) -24|[]-> c(c(x))
     a(b(a(x3642))) <-17|0[]- a(c(b(x3642))) -28|[]-> c(a(b(x3642)))
     b(a(x)) <-17|[]- c(b(x)) -29|[]-> a(c(x))
     b(b(a(x3644))) <-17|0[]- b(c(b(x3644))) -30|[]-> a(c(b(x3644)))
     b(b(a(x3645))) <-17|0[]- b(c(b(x3645))) -33|[]-> b(a(b(x3645)))
     a(b(a(x3646))) <-17|0[]- a(c(b(x3646))) -34|[]-> b(c(b(x3646)))
     b(a(x)) <-17|[]- c(b(x)) -35|[]-> b(c(x))
     a(c(b(x3648))) <-18|0[]- a(a(b(x3648))) -8|[]-> c(c(b(x3648)))
     c(c(b(x3649))) <-18|0[]- c(a(b(x3649))) -9|[]-> c(b(b(x3649)))
     c(c(b(x3650))) <-18|0[]- c(a(b(x3650))) -10|[]-> b(c(b(x3650)))
     c(c(b(x3651))) <-18|0[]- c(a(b(x3651))) -11|[]-> b(a(b(x3651)))
     a(c(b(x3652))) <-18|0[]- a(a(b(x3652))) -15|[]-> a(c(b(x3652)))
     c(b(x)) <-18|[]- a(b(x)) -19|[]-> b(c(x))
     c(b(x)) <-18|[]- a(b(x)) -20|[]-> b(a(x))
     a(c(b(x3655))) <-18|0[]- a(a(b(x3655))) -26|[]-> c(b(b(x3655)))
     c(c(b(x3656))) <-18|0[]- c(a(b(x3656))) -27|[]-> a(a(b(x3656)))
     a(c(b(x3657))) <-18|0[]- a(a(b(x3657))) -31|[]-> b(c(b(x3657)))
     a(c(b(x3658))) <-18|0[]- a(a(b(x3658))) -32|[]-> b(a(b(x3658)))
     c(b(x)) <-18|[]- a(b(x)) -36|[]-> a(a(x))
     a(b(c(x3660))) <-19|0[]- a(a(b(x3660))) -8|[]-> c(c(b(x3660)))
     c(b(c(x3661))) <-19|0[]- c(a(b(x3661))) -9|[]-> c(b(b(x3661)))
     c(b(c(x3662))) <-19|0[]- c(a(b(x3662))) -10|[]-> b(c(b(x3662)))
     c(b(c(x3663))) <-19|0[]- c(a(b(x3663))) -11|[]-> b(a(b(x3663)))
     a(b(c(x3664))) <-19|0[]- a(a(b(x3664))) -15|[]-> a(c(b(x3664)))
     b(c(x)) <-19|[]- a(b(x)) -18|[]-> c(b(x))
     b(c(x)) <-19|[]- a(b(x)) -20|[]-> b(a(x))
     a(b(c(x3667))) <-19|0[]- a(a(b(x3667))) -26|[]-> c(b(b(x3667)))
     c(b(c(x3668))) <-19|0[]- c(a(b(x3668))) -27|[]-> a(a(b(x3668)))
     a(b(c(x3669))) <-19|0[]- a(a(b(x3669))) -31|[]-> b(c(b(x3669)))
     a(b(c(x3670))) <-19|0[]- a(a(b(x3670))) -32|[]-> b(a(b(x3670)))
     b(c(x)) <-19|[]- a(b(x)) -36|[]-> a(a(x))
     a(b(a(x3672))) <-20|0[]- a(a(b(x3672))) -8|[]-> c(c(b(x3672)))
     c(b(a(x3673))) <-20|0[]- c(a(b(x3673))) -9|[]-> c(b(b(x3673)))
     c(b(a(x3674))) <-20|0[]- c(a(b(x3674))) -10|[]-> b(c(b(x3674)))
     c(b(a(x3675))) <-20|0[]- c(a(b(x3675))) -11|[]-> b(a(b(x3675)))
     a(b(a(x3676))) <-20|0[]- a(a(b(x3676))) -15|[]-> a(c(b(x3676)))
     b(a(x)) <-20|[]- a(b(x)) -18|[]-> c(b(x))
     b(a(x)) <-20|[]- a(b(x)) -19|[]-> b(c(x))
     a(b(a(x3679))) <-20|0[]- a(a(b(x3679))) -26|[]-> c(b(b(x3679)))
     c(b(a(x3680))) <-20|0[]- c(a(b(x3680))) -27|[]-> a(a(b(x3680)))
     a(b(a(x3681))) <-20|0[]- a(a(b(x3681))) -31|[]-> b(c(b(x3681)))
     a(b(a(x3682))) <-20|0[]- a(a(b(x3682))) -32|[]-> b(a(b(x3682)))
     b(a(x)) <-20|[]- a(b(x)) -36|[]-> a(a(x))
     a(a(x)) <-21|[]- c(c(x)) -0|[]-> b(c(x))
     c(a(a(x3685))) <-21|0[]- c(c(c(x3685))) -0|[]-> b(c(c(x3685)))
     a(a(x)) <-21|[]- c(c(x)) -1|[]-> b(a(x))
     c(a(a(x3687))) <-21|0[]- c(c(c(x3687))) -1|[]-> b(a(c(x3687)))
     a(a(x)) <-21|[]- c(c(x)) -3|[]-> c(b(x))
     c(a(a(x3689))) <-21|0[]- c(c(c(x3689))) -3|[]-> c(b(c(x3689)))
     a(a(a(x3690))) <-21|0[]- a(c(c(x3690))) -12|[]-> a(a(c(x3690)))
     b(a(a(x3691))) <-21|0[]- b(c(c(x3691))) -14|[]-> c(a(c(x3691)))
     a(a(a(x3692))) <-21|0[]- a(c(c(x3692))) -16|[]-> b(a(c(x3692)))
     c(a(a(x3693))) <-21|0[]- c(c(c(x3693))) -21|[]-> a(a(c(x3693)))
     a(a(x)) <-21|[]- c(c(x)) -23|[]-> b(b(x))
     c(a(a(x3695))) <-21|0[]- c(c(c(x3695))) -23|[]-> b(b(c(x3695)))
     a(a(a(x3696))) <-21|0[]- a(c(c(x3696))) -28|[]-> c(a(c(x3696)))
     b(a(a(x3697))) <-21|0[]- b(c(c(x3697))) -30|[]-> a(c(c(x3697)))
     b(a(a(x3698))) <-21|0[]- b(c(c(x3698))) -33|[]-> b(a(c(x3698)))
     a(a(a(x3699))) <-21|0[]- a(c(c(x3699))) -34|[]-> b(c(c(x3699)))
     c(c(x)) <-22|[]- b(b(x)) -2|[]-> a(a(x))
     b(c(c(x3701))) <-22|0[]- b(b(b(x3701))) -2|[]-> a(a(b(x3701)))
     c(c(c(x3702))) <-22|0[]- c(b(b(x3702))) -4|[]-> a(a(b(x3702)))
     c(c(c(x3703))) <-22|0[]- c(b(b(x3703))) -5|[]-> b(b(b(x3703)))
     c(c(x)) <-22|[]- b(b(x)) -6|[]-> a(c(x))
     b(c(c(x3705))) <-22|0[]- b(b(b(x3705))) -6|[]-> a(c(b(x3705)))
     c(c(x)) <-22|[]- b(b(x)) -7|[]-> b(c(x))
     b(c(c(x3707))) <-22|0[]- b(b(b(x3707))) -7|[]-> b(c(b(x3707)))
     c(c(c(x3708))) <-22|0[]- c(b(b(x3708))) -13|[]-> c(a(b(x3708)))
     c(c(c(x3709))) <-22|0[]- c(b(b(x3709))) -17|[]-> b(a(b(x3709)))
     a(c(c(x3710))) <-22|0[]- a(b(b(x3710))) -18|[]-> c(b(b(x3710)))
     a(c(c(x3711))) <-22|0[]- a(b(b(x3711))) -19|[]-> b(c(b(x3711)))
     a(c(c(x3712))) <-22|0[]- a(b(b(x3712))) -20|[]-> b(a(b(x3712)))
     b(c(c(x3713))) <-22|0[]- b(b(b(x3713))) -22|[]-> c(c(b(x3713)))
     c(c(c(x3714))) <-22|0[]- c(b(b(x3714))) -24|[]-> c(c(b(x3714)))
     c(c(x)) <-22|[]- b(b(x)) -25|[]-> c(b(x))
     b(c(c(x3716))) <-22|0[]- b(b(b(x3716))) -25|[]-> c(b(b(x3716)))
     c(c(c(x3717))) <-22|0[]- c(b(b(x3717))) -29|[]-> a(c(b(x3717)))
     c(c(c(x3718))) <-22|0[]- c(b(b(x3718))) -35|[]-> b(c(b(x3718)))
     a(c(c(x3719))) <-22|0[]- a(b(b(x3719))) -36|[]-> a(a(b(x3719)))
     b(b(x)) <-23|[]- c(c(x)) -0|[]-> b(c(x))
     c(b(b(x3721))) <-23|0[]- c(c(c(x3721))) -0|[]-> b(c(c(x3721)))
     b(b(x)) <-23|[]- c(c(x)) -1|[]-> b(a(x))
     c(b(b(x3723))) <-23|0[]- c(c(c(x3723))) -1|[]-> b(a(c(x3723)))
     b(b(x)) <-23|[]- c(c(x)) -3|[]-> c(b(x))
     c(b(b(x3725))) <-23|0[]- c(c(c(x3725))) -3|[]-> c(b(c(x3725)))
     a(b(b(x3726))) <-23|0[]- a(c(c(x3726))) -12|[]-> a(a(c(x3726)))
     b(b(b(x3727))) <-23|0[]- b(c(c(x3727))) -14|[]-> c(a(c(x3727)))
     a(b(b(x3728))) <-23|0[]- a(c(c(x3728))) -16|[]-> b(a(c(x3728)))
     b(b(x)) <-23|[]- c(c(x)) -21|[]-> a(a(x))
     c(b(b(x3730))) <-23|0[]- c(c(c(x3730))) -21|[]-> a(a(c(x3730)))
     c(b(b(x3731))) <-23|0[]- c(c(c(x3731))) -23|[]-> b(b(c(x3731)))
     a(b(b(x3732))) <-23|0[]- a(c(c(x3732))) -28|[]-> c(a(c(x3732)))
     b(b(b(x3733))) <-23|0[]- b(c(c(x3733))) -30|[]-> a(c(c(x3733)))
     b(b(b(x3734))) <-23|0[]- b(c(c(x3734))) -33|[]-> b(a(c(x3734)))
     a(b(b(x3735))) <-23|0[]- a(c(c(x3735))) -34|[]-> b(c(c(x3735)))
     c(c(c(x3736))) <-24|0[]- c(c(b(x3736))) -0|[]-> b(c(b(x3736)))
     c(c(c(x3737))) <-24|0[]- c(c(b(x3737))) -1|[]-> b(a(b(x3737)))
     c(c(c(x3738))) <-24|0[]- c(c(b(x3738))) -3|[]-> c(b(b(x3738)))
     c(c(x)) <-24|[]- c(b(x)) -4|[]-> a(a(x))
     c(c(x)) <-24|[]- c(b(x)) -5|[]-> b(b(x))
     a(c(c(x3741))) <-24|0[]- a(c(b(x3741))) -12|[]-> a(a(b(x3741)))
     c(c(x)) <-24|[]- c(b(x)) -13|[]-> c(a(x))
     b(c(c(x3743))) <-24|0[]- b(c(b(x3743))) -14|[]-> c(a(b(x3743)))
     a(c(c(x3744))) <-24|0[]- a(c(b(x3744))) -16|[]-> b(a(b(x3744)))
     c(c(x)) <-24|[]- c(b(x)) -17|[]-> b(a(x))
     c(c(c(x3746))) <-24|0[]- c(c(b(x3746))) -21|[]-> a(a(b(x3746)))
     c(c(c(x3747))) <-24|0[]- c(c(b(x3747))) -23|[]-> b(b(b(x3747)))
     a(c(c(x3748))) <-24|0[]- a(c(b(x3748))) -28|[]-> c(a(b(x3748)))
     c(c(x)) <-24|[]- c(b(x)) -29|[]-> a(c(x))
     b(c(c(x3750))) <-24|0[]- b(c(b(x3750))) -30|[]-> a(c(b(x3750)))
     b(c(c(x3751))) <-24|0[]- b(c(b(x3751))) -33|[]-> b(a(b(x3751)))
     a(c(c(x3752))) <-24|0[]- a(c(b(x3752))) -34|[]-> b(c(b(x3752)))
     c(c(x)) <-24|[]- c(b(x)) -35|[]-> b(c(x))
     c(b(x)) <-25|[]- b(b(x)) -2|[]-> a(a(x))
     b(c(b(x3755))) <-25|0[]- b(b(b(x3755))) -2|[]-> a(a(b(x3755)))
     c(c(b(x3756))) <-25|0[]- c(b(b(x3756))) -4|[]-> a(a(b(x3756)))
     c(c(b(x3757))) <-25|0[]- c(b(b(x3757))) -5|[]-> b(b(b(x3757)))
     c(b(x)) <-25|[]- b(b(x)) -6|[]-> a(c(x))
     b(c(b(x3759))) <-25|0[]- b(b(b(x3759))) -6|[]-> a(c(b(x3759)))
     c(b(x)) <-25|[]- b(b(x)) -7|[]-> b(c(x))
     b(c(b(x3761))) <-25|0[]- b(b(b(x3761))) -7|[]-> b(c(b(x3761)))
     c(c(b(x3762))) <-25|0[]- c(b(b(x3762))) -13|[]-> c(a(b(x3762)))
     c(c(b(x3763))) <-25|0[]- c(b(b(x3763))) -17|[]-> b(a(b(x3763)))
     a(c(b(x3764))) <-25|0[]- a(b(b(x3764))) -18|[]-> c(b(b(x3764)))
     a(c(b(x3765))) <-25|0[]- a(b(b(x3765))) -19|[]-> b(c(b(x3765)))
     a(c(b(x3766))) <-25|0[]- a(b(b(x3766))) -20|[]-> b(a(b(x3766)))
     c(b(x)) <-25|[]- b(b(x)) -22|[]-> c(c(x))
     b(c(b(x3768))) <-25|0[]- b(b(b(x3768))) -22|[]-> c(c(b(x3768)))
     c(c(b(x3769))) <-25|0[]- c(b(b(x3769))) -24|[]-> c(c(b(x3769)))
     b(c(b(x3770))) <-25|0[]- b(b(b(x3770))) -25|[]-> c(b(b(x3770)))
     c(c(b(x3771))) <-25|0[]- c(b(b(x3771))) -29|[]-> a(c(b(x3771)))
     c(c(b(x3772))) <-25|0[]- c(b(b(x3772))) -35|[]-> b(c(b(x3772)))
     a(c(b(x3773))) <-25|0[]- a(b(b(x3773))) -36|[]-> a(a(b(x3773)))
     c(b(x)) <-26|[]- a(a(x)) -8|[]-> c(c(x))
     a(c(b(x3775))) <-26|0[]- a(a(a(x3775))) -8|[]-> c(c(a(x3775)))
     c(c(b(x3776))) <-26|0[]- c(a(a(x3776))) -9|[]-> c(b(a(x3776)))
     c(c(b(x3777))) <-26|0[]- c(a(a(x3777))) -10|[]-> b(c(a(x3777)))
     c(c(b(x3778))) <-26|0[]- c(a(a(x3778))) -11|[]-> b(a(a(x3778)))
     c(b(x)) <-26|[]- a(a(x)) -15|[]-> a(c(x))
     a(c(b(x3780))) <-26|0[]- a(a(a(x3780))) -15|[]-> a(c(a(x3780)))
     a(c(b(x3781))) <-26|0[]- a(a(a(x3781))) -26|[]-> c(b(a(x3781)))
     c(c(b(x3782))) <-26|0[]- c(a(a(x3782))) -27|[]-> a(a(a(x3782)))
     c(b(x)) <-26|[]- a(a(x)) -31|[]-> b(c(x))
     a(c(b(x3784))) <-26|0[]- a(a(a(x3784))) -31|[]-> b(c(a(x3784)))
     c(b(x)) <-26|[]- a(a(x)) -32|[]-> b(a(x))
     a(c(b(x3786))) <-26|0[]- a(a(a(x3786))) -32|[]-> b(a(a(x3786)))
     c(a(a(x3787))) <-27|0[]- c(c(a(x3787))) -0|[]-> b(c(a(x3787)))
     c(a(a(x3788))) <-27|0[]- c(c(a(x3788))) -1|[]-> b(a(a(x3788)))
     c(a(a(x3789))) <-27|0[]- c(c(a(x3789))) -3|[]-> c(b(a(x3789)))
     a(a(x)) <-27|[]- c(a(x)) -9|[]-> c(b(x))
     a(a(x)) <-27|[]- c(a(x)) -10|[]-> b(c(x))
     a(a(x)) <-27|[]- c(a(x)) -11|[]-> b(a(x))
     a(a(a(x3793))) <-27|0[]- a(c(a(x3793))) -12|[]-> a(a(a(x3793)))
     b(a(a(x3794))) <-27|0[]- b(c(a(x3794))) -14|[]-> c(a(a(x3794)))
     a(a(a(x3795))) <-27|0[]- a(c(a(x3795))) -16|[]-> b(a(a(x3795)))
     c(a(a(x3796))) <-27|0[]- c(c(a(x3796))) -21|[]-> a(a(a(x3796)))
     c(a(a(x3797))) <-27|0[]- c(c(a(x3797))) -23|[]-> b(b(a(x3797)))
     a(a(a(x3798))) <-27|0[]- a(c(a(x3798))) -28|[]-> c(a(a(x3798)))
     b(a(a(x3799))) <-27|0[]- b(c(a(x3799))) -30|[]-> a(c(a(x3799)))
     b(a(a(x3800))) <-27|0[]- b(c(a(x3800))) -33|[]-> b(a(a(x3800)))
     a(a(a(x3801))) <-27|0[]- a(c(a(x3801))) -34|[]-> b(c(a(x3801)))
     a(c(a(x3802))) <-28|0[]- a(a(c(x3802))) -8|[]-> c(c(c(x3802)))
     c(c(a(x3803))) <-28|0[]- c(a(c(x3803))) -9|[]-> c(b(c(x3803)))
     c(c(a(x3804))) <-28|0[]- c(a(c(x3804))) -10|[]-> b(c(c(x3804)))
     c(c(a(x3805))) <-28|0[]- c(a(c(x3805))) -11|[]-> b(a(c(x3805)))
     c(a(x)) <-28|[]- a(c(x)) -12|[]-> a(a(x))
     a(c(a(x3807))) <-28|0[]- a(a(c(x3807))) -15|[]-> a(c(c(x3807)))
     c(a(x)) <-28|[]- a(c(x)) -16|[]-> b(a(x))
     a(c(a(x3809))) <-28|0[]- a(a(c(x3809))) -26|[]-> c(b(c(x3809)))
     c(c(a(x3810))) <-28|0[]- c(a(c(x3810))) -27|[]-> a(a(c(x3810)))
     a(c(a(x3811))) <-28|0[]- a(a(c(x3811))) -31|[]-> b(c(c(x3811)))
     a(c(a(x3812))) <-28|0[]- a(a(c(x3812))) -32|[]-> b(a(c(x3812)))
     c(a(x)) <-28|[]- a(c(x)) -34|[]-> b(c(x))
     c(a(c(x3814))) <-29|0[]- c(c(b(x3814))) -0|[]-> b(c(b(x3814)))
     c(a(c(x3815))) <-29|0[]- c(c(b(x3815))) -1|[]-> b(a(b(x3815)))
     c(a(c(x3816))) <-29|0[]- c(c(b(x3816))) -3|[]-> c(b(b(x3816)))
     a(c(x)) <-29|[]- c(b(x)) -4|[]-> a(a(x))
     a(c(x)) <-29|[]- c(b(x)) -5|[]-> b(b(x))
     a(a(c(x3819))) <-29|0[]- a(c(b(x3819))) -12|[]-> a(a(b(x3819)))
     a(c(x)) <-29|[]- c(b(x)) -13|[]-> c(a(x))
     b(a(c(x3821))) <-29|0[]- b(c(b(x3821))) -14|[]-> c(a(b(x3821)))
     a(a(c(x3822))) <-29|0[]- a(c(b(x3822))) -16|[]-> b(a(b(x3822)))
     a(c(x)) <-29|[]- c(b(x)) -17|[]-> b(a(x))
     c(a(c(x3824))) <-29|0[]- c(c(b(x3824))) -21|[]-> a(a(b(x3824)))
     c(a(c(x3825))) <-29|0[]- c(c(b(x3825))) -23|[]-> b(b(b(x3825)))
     a(c(x)) <-29|[]- c(b(x)) -24|[]-> c(c(x))
     a(a(c(x3827))) <-29|0[]- a(c(b(x3827))) -28|[]-> c(a(b(x3827)))
     b(a(c(x3828))) <-29|0[]- b(c(b(x3828))) -30|[]-> a(c(b(x3828)))
     b(a(c(x3829))) <-29|0[]- b(c(b(x3829))) -33|[]-> b(a(b(x3829)))
     a(a(c(x3830))) <-29|0[]- a(c(b(x3830))) -34|[]-> b(c(b(x3830)))
     a(c(x)) <-29|[]- c(b(x)) -35|[]-> b(c(x))
     b(a(c(x3832))) <-30|0[]- b(b(c(x3832))) -2|[]-> a(a(c(x3832)))
     c(a(c(x3833))) <-30|0[]- c(b(c(x3833))) -4|[]-> a(a(c(x3833)))
     c(a(c(x3834))) <-30|0[]- c(b(c(x3834))) -5|[]-> b(b(c(x3834)))
     b(a(c(x3835))) <-30|0[]- b(b(c(x3835))) -6|[]-> a(c(c(x3835)))
     b(a(c(x3836))) <-30|0[]- b(b(c(x3836))) -7|[]-> b(c(c(x3836)))
     c(a(c(x3837))) <-30|0[]- c(b(c(x3837))) -13|[]-> c(a(c(x3837)))
     a(c(x)) <-30|[]- b(c(x)) -14|[]-> c(a(x))
     c(a(c(x3839))) <-30|0[]- c(b(c(x3839))) -17|[]-> b(a(c(x3839)))
     a(a(c(x3840))) <-30|0[]- a(b(c(x3840))) -18|[]-> c(b(c(x3840)))
     a(a(c(x3841))) <-30|0[]- a(b(c(x3841))) -19|[]-> b(c(c(x3841)))
     a(a(c(x3842))) <-30|0[]- a(b(c(x3842))) -20|[]-> b(a(c(x3842)))
     b(a(c(x3843))) <-30|0[]- b(b(c(x3843))) -22|[]-> c(c(c(x3843)))
     c(a(c(x3844))) <-30|0[]- c(b(c(x3844))) -24|[]-> c(c(c(x3844)))
     b(a(c(x3845))) <-30|0[]- b(b(c(x3845))) -25|[]-> c(b(c(x3845)))
     c(a(c(x3846))) <-30|0[]- c(b(c(x3846))) -29|[]-> a(c(c(x3846)))
     a(c(x)) <-30|[]- b(c(x)) -33|[]-> b(a(x))
     c(a(c(x3848))) <-30|0[]- c(b(c(x3848))) -35|[]-> b(c(c(x3848)))
     a(a(c(x3849))) <-30|0[]- a(b(c(x3849))) -36|[]-> a(a(c(x3849)))
     b(c(x)) <-31|[]- a(a(x)) -8|[]-> c(c(x))
     a(b(c(x3851))) <-31|0[]- a(a(a(x3851))) -8|[]-> c(c(a(x3851)))
     c(b(c(x3852))) <-31|0[]- c(a(a(x3852))) -9|[]-> c(b(a(x3852)))
     c(b(c(x3853))) <-31|0[]- c(a(a(x3853))) -10|[]-> b(c(a(x3853)))
     c(b(c(x3854))) <-31|0[]- c(a(a(x3854))) -11|[]-> b(a(a(x3854)))
     b(c(x)) <-31|[]- a(a(x)) -15|[]-> a(c(x))
     a(b(c(x3856))) <-31|0[]- a(a(a(x3856))) -15|[]-> a(c(a(x3856)))
     b(c(x)) <-31|[]- a(a(x)) -26|[]-> c(b(x))
     a(b(c(x3858))) <-31|0[]- a(a(a(x3858))) -26|[]-> c(b(a(x3858)))
     c(b(c(x3859))) <-31|0[]- c(a(a(x3859))) -27|[]-> a(a(a(x3859)))
     a(b(c(x3860))) <-31|0[]- a(a(a(x3860))) -31|[]-> b(c(a(x3860)))
     b(c(x)) <-31|[]- a(a(x)) -32|[]-> b(a(x))
     a(b(c(x3862))) <-31|0[]- a(a(a(x3862))) -32|[]-> b(a(a(x3862)))
     b(a(x)) <-32|[]- a(a(x)) -8|[]-> c(c(x))
     a(b(a(x3864))) <-32|0[]- a(a(a(x3864))) -8|[]-> c(c(a(x3864)))
     c(b(a(x3865))) <-32|0[]- c(a(a(x3865))) -9|[]-> c(b(a(x3865)))
     c(b(a(x3866))) <-32|0[]- c(a(a(x3866))) -10|[]-> b(c(a(x3866)))
     c(b(a(x3867))) <-32|0[]- c(a(a(x3867))) -11|[]-> b(a(a(x3867)))
     b(a(x)) <-32|[]- a(a(x)) -15|[]-> a(c(x))
     a(b(a(x3869))) <-32|0[]- a(a(a(x3869))) -15|[]-> a(c(a(x3869)))
     b(a(x)) <-32|[]- a(a(x)) -26|[]-> c(b(x))
     a(b(a(x3871))) <-32|0[]- a(a(a(x3871))) -26|[]-> c(b(a(x3871)))
     c(b(a(x3872))) <-32|0[]- c(a(a(x3872))) -27|[]-> a(a(a(x3872)))
     b(a(x)) <-32|[]- a(a(x)) -31|[]-> b(c(x))
     a(b(a(x3874))) <-32|0[]- a(a(a(x3874))) -31|[]-> b(c(a(x3874)))
     a(b(a(x3875))) <-32|0[]- a(a(a(x3875))) -32|[]-> b(a(a(x3875)))
     b(b(a(x3876))) <-33|0[]- b(b(c(x3876))) -2|[]-> a(a(c(x3876)))
     c(b(a(x3877))) <-33|0[]- c(b(c(x3877))) -4|[]-> a(a(c(x3877)))
     c(b(a(x3878))) <-33|0[]- c(b(c(x3878))) -5|[]-> b(b(c(x3878)))
     b(b(a(x3879))) <-33|0[]- b(b(c(x3879))) -6|[]-> a(c(c(x3879)))
     b(b(a(x3880))) <-33|0[]- b(b(c(x3880))) -7|[]-> b(c(c(x3880)))
     c(b(a(x3881))) <-33|0[]- c(b(c(x3881))) -13|[]-> c(a(c(x3881)))
     b(a(x)) <-33|[]- b(c(x)) -14|[]-> c(a(x))
     c(b(a(x3883))) <-33|0[]- c(b(c(x3883))) -17|[]-> b(a(c(x3883)))
     a(b(a(x3884))) <-33|0[]- a(b(c(x3884))) -18|[]-> c(b(c(x3884)))
     a(b(a(x3885))) <-33|0[]- a(b(c(x3885))) -19|[]-> b(c(c(x3885)))
     a(b(a(x3886))) <-33|0[]- a(b(c(x3886))) -20|[]-> b(a(c(x3886)))
     b(b(a(x3887))) <-33|0[]- b(b(c(x3887))) -22|[]-> c(c(c(x3887)))
     c(b(a(x3888))) <-33|0[]- c(b(c(x3888))) -24|[]-> c(c(c(x3888)))
     b(b(a(x3889))) <-33|0[]- b(b(c(x3889))) -25|[]-> c(b(c(x3889)))
     c(b(a(x3890))) <-33|0[]- c(b(c(x3890))) -29|[]-> a(c(c(x3890)))
     b(a(x)) <-33|[]- b(c(x)) -30|[]-> a(c(x))
     c(b(a(x3892))) <-33|0[]- c(b(c(x3892))) -35|[]-> b(c(c(x3892)))
     a(b(a(x3893))) <-33|0[]- a(b(c(x3893))) -36|[]-> a(a(c(x3893)))
     a(b(c(x3894))) <-34|0[]- a(a(c(x3894))) -8|[]-> c(c(c(x3894)))
     c(b(c(x3895))) <-34|0[]- c(a(c(x3895))) -9|[]-> c(b(c(x3895)))
     c(b(c(x3896))) <-34|0[]- c(a(c(x3896))) -10|[]-> b(c(c(x3896)))
     c(b(c(x3897))) <-34|0[]- c(a(c(x3897))) -11|[]-> b(a(c(x3897)))
     b(c(x)) <-34|[]- a(c(x)) -12|[]-> a(a(x))
     a(b(c(x3899))) <-34|0[]- a(a(c(x3899))) -15|[]-> a(c(c(x3899)))
     b(c(x)) <-34|[]- a(c(x)) -16|[]-> b(a(x))
     a(b(c(x3901))) <-34|0[]- a(a(c(x3901))) -26|[]-> c(b(c(x3901)))
     c(b(c(x3902))) <-34|0[]- c(a(c(x3902))) -27|[]-> a(a(c(x3902)))
     b(c(x)) <-34|[]- a(c(x)) -28|[]-> c(a(x))
     a(b(c(x3904))) <-34|0[]- a(a(c(x3904))) -31|[]-> b(c(c(x3904)))
     a(b(c(x3905))) <-34|0[]- a(a(c(x3905))) -32|[]-> b(a(c(x3905)))
     c(b(c(x3906))) <-35|0[]- c(c(b(x3906))) -0|[]-> b(c(b(x3906)))
     c(b(c(x3907))) <-35|0[]- c(c(b(x3907))) -1|[]-> b(a(b(x3907)))
     c(b(c(x3908))) <-35|0[]- c(c(b(x3908))) -3|[]-> c(b(b(x3908)))
     b(c(x)) <-35|[]- c(b(x)) -4|[]-> a(a(x))
     b(c(x)) <-35|[]- c(b(x)) -5|[]-> b(b(x))
     a(b(c(x3911))) <-35|0[]- a(c(b(x3911))) -12|[]-> a(a(b(x3911)))
     b(c(x)) <-35|[]- c(b(x)) -13|[]-> c(a(x))
     b(b(c(x3913))) <-35|0[]- b(c(b(x3913))) -14|[]-> c(a(b(x3913)))
     a(b(c(x3914))) <-35|0[]- a(c(b(x3914))) -16|[]-> b(a(b(x3914)))
     b(c(x)) <-35|[]- c(b(x)) -17|[]-> b(a(x))
     c(b(c(x3916))) <-35|0[]- c(c(b(x3916))) -21|[]-> a(a(b(x3916)))
     c(b(c(x3917))) <-35|0[]- c(c(b(x3917))) -23|[]-> b(b(b(x3917)))
     b(c(x)) <-35|[]- c(b(x)) -24|[]-> c(c(x))
     a(b(c(x3919))) <-35|0[]- a(c(b(x3919))) -28|[]-> c(a(b(x3919)))
     b(c(x)) <-35|[]- c(b(x)) -29|[]-> a(c(x))
     b(b(c(x3921))) <-35|0[]- b(c(b(x3921))) -30|[]-> a(c(b(x3921)))
     b(b(c(x3922))) <-35|0[]- b(c(b(x3922))) -33|[]-> b(a(b(x3922)))
     a(b(c(x3923))) <-35|0[]- a(c(b(x3923))) -34|[]-> b(c(b(x3923)))
     a(a(a(x3924))) <-36|0[]- a(a(b(x3924))) -8|[]-> c(c(b(x3924)))
     c(a(a(x3925))) <-36|0[]- c(a(b(x3925))) -9|[]-> c(b(b(x3925)))
     c(a(a(x3926))) <-36|0[]- c(a(b(x3926))) -10|[]-> b(c(b(x3926)))
     c(a(a(x3927))) <-36|0[]- c(a(b(x3927))) -11|[]-> b(a(b(x3927)))
     a(a(a(x3928))) <-36|0[]- a(a(b(x3928))) -15|[]-> a(c(b(x3928)))
     a(a(x)) <-36|[]- a(b(x)) -18|[]-> c(b(x))
     a(a(x)) <-36|[]- a(b(x)) -19|[]-> b(c(x))
     a(a(x)) <-36|[]- a(b(x)) -20|[]-> b(a(x))
     a(a(a(x3932))) <-36|0[]- a(a(b(x3932))) -26|[]-> c(b(b(x3932)))
     c(a(a(x3933))) <-36|0[]- c(a(b(x3933))) -27|[]-> a(a(b(x3933)))
     a(a(a(x3934))) <-36|0[]- a(a(b(x3934))) -31|[]-> b(c(b(x3934)))
     a(a(a(x3935))) <-36|0[]- a(a(b(x3935))) -32|[]-> b(a(b(x3935)))
    Redundant Rules Transformation:
     c(c(x)) -> b(c(x))
     c(c(x)) -> b(a(x))
     b(b(x)) -> a(a(x))
     c(c(x)) -> c(b(x))
     c(b(x)) -> a(a(x))
     c(b(x)) -> b(b(x))
     b(b(x)) -> a(c(x))
     b(b(x)) -> b(c(x))
     a(a(x)) -> c(c(x))
     c(a(x)) -> c(b(x))
     c(a(x)) -> b(c(x))
     c(a(x)) -> b(a(x))
     a(c(x)) -> a(a(x))
     c(b(x)) -> c(a(x))
     b(c(x)) -> c(a(x))
     a(a(x)) -> a(c(x))
     a(c(x)) -> b(a(x))
     c(b(x)) -> b(a(x))
     a(b(x)) -> c(b(x))
     a(b(x)) -> b(c(x))
     a(b(x)) -> b(a(x))
     c(c(x)) -> a(a(x))
     b(b(x)) -> c(c(x))
     c(c(x)) -> b(b(x))
     c(b(x)) -> c(c(x))
     b(b(x)) -> c(b(x))
     a(a(x)) -> c(b(x))
     c(a(x)) -> a(a(x))
     a(c(x)) -> c(a(x))
     c(b(x)) -> a(c(x))
     b(c(x)) -> a(c(x))
     a(a(x)) -> b(c(x))
     a(a(x)) -> b(a(x))
     b(c(x)) -> b(a(x))
     a(c(x)) -> b(c(x))
     c(b(x)) -> b(c(x))
     a(b(x)) -> a(a(x))
     c(c(x)) -> c(a(x))
     c(c(x)) -> a(c(x))
     b(b(x)) -> b(a(x))
     c(c(x)) -> c(c(x))
     c(b(x)) -> c(b(x))
     b(b(x)) -> c(a(x))
     a(a(x)) -> a(a(x))
     a(a(x)) -> b(b(x))
     c(a(x)) -> b(b(x))
     c(a(x)) -> c(a(x))
     c(a(x)) -> c(c(x))
     c(a(x)) -> a(c(x))
     a(c(x)) -> c(c(x))
     a(c(x)) -> a(c(x))
     a(c(x)) -> c(b(x))
     b(c(x)) -> c(b(x))
     b(c(x)) -> b(c(x))
     b(c(x)) -> a(a(x))
     a(a(x)) -> c(a(x))
     a(b(x)) -> b(b(x))
     a(b(x)) -> c(a(x))
     a(b(x)) -> c(c(x))
     a(b(x)) -> a(c(x))
     b(b(x)) -> b(b(x))
     Church Rosser Transformation Processor (no redundant rules):
      strict:
       a(b(x)) -> a(c(x))
       a(b(x)) -> c(c(x))
       a(b(x)) -> c(a(x))
       a(b(x)) -> b(b(x))
       a(a(x)) -> c(a(x))
       b(c(x)) -> a(a(x))
       b(c(x)) -> c(b(x))
       a(c(x)) -> c(b(x))
       a(c(x)) -> c(c(x))
       c(a(x)) -> a(c(x))
       c(a(x)) -> c(c(x))
       c(a(x)) -> b(b(x))
       a(a(x)) -> b(b(x))
       b(b(x)) -> c(a(x))
       b(b(x)) -> b(a(x))
       c(c(x)) -> a(c(x))
       c(c(x)) -> c(a(x))
       a(b(x)) -> a(a(x))
       c(b(x)) -> b(c(x))
       a(c(x)) -> b(c(x))
       b(c(x)) -> b(a(x))
       a(a(x)) -> b(a(x))
       a(a(x)) -> b(c(x))
       b(c(x)) -> a(c(x))
       c(b(x)) -> a(c(x))
       a(c(x)) -> c(a(x))
       c(a(x)) -> a(a(x))
       a(a(x)) -> c(b(x))
       b(b(x)) -> c(b(x))
       c(b(x)) -> c(c(x))
       c(c(x)) -> b(b(x))
       b(b(x)) -> c(c(x))
       c(c(x)) -> a(a(x))
       a(b(x)) -> b(a(x))
       a(b(x)) -> b(c(x))
       a(b(x)) -> c(b(x))
       c(b(x)) -> b(a(x))
       a(c(x)) -> b(a(x))
       a(a(x)) -> a(c(x))
       b(c(x)) -> c(a(x))
       c(b(x)) -> c(a(x))
       a(c(x)) -> a(a(x))
       c(a(x)) -> b(a(x))
       c(a(x)) -> b(c(x))
       c(a(x)) -> c(b(x))
       a(a(x)) -> c(c(x))
       b(b(x)) -> b(c(x))
       b(b(x)) -> a(c(x))
       c(b(x)) -> b(b(x))
       c(b(x)) -> a(a(x))
       c(c(x)) -> c(b(x))
       b(b(x)) -> a(a(x))
       c(c(x)) -> b(a(x))
       c(c(x)) -> b(c(x))
      weak:
       
      critical peaks: 1252
       a(c(x)) <-0|[]- a(b(x)) -1|[]-> c(c(x))
       a(c(x)) <-0|[]- a(b(x)) -2|[]-> c(a(x))
       a(c(x)) <-0|[]- a(b(x)) -3|[]-> b(b(x))
       a(a(c(x9771))) <-0|0[]- a(a(b(x9771))) -4|[]-> c(a(b(x9771)))
       c(a(c(x9772))) <-0|0[]- c(a(b(x9772))) -9|[]-> a(c(b(x9772)))
       c(a(c(x9773))) <-0|0[]- c(a(b(x9773))) -10|[]-> c(c(b(x9773)))
       c(a(c(x9774))) <-0|0[]- c(a(b(x9774))) -11|[]-> b(b(b(x9774)))
       a(a(c(x9775))) <-0|0[]- a(a(b(x9775))) -12|[]-> b(b(b(x9775)))
       a(c(x)) <-0|[]- a(b(x)) -17|[]-> a(a(x))
       a(a(c(x9777))) <-0|0[]- a(a(b(x9777))) -21|[]-> b(a(b(x9777)))
       a(a(c(x9778))) <-0|0[]- a(a(b(x9778))) -22|[]-> b(c(b(x9778)))
       c(a(c(x9779))) <-0|0[]- c(a(b(x9779))) -26|[]-> a(a(b(x9779)))
       a(a(c(x9780))) <-0|0[]- a(a(b(x9780))) -27|[]-> c(b(b(x9780)))
       a(c(x)) <-0|[]- a(b(x)) -33|[]-> b(a(x))
       a(c(x)) <-0|[]- a(b(x)) -34|[]-> b(c(x))
       a(c(x)) <-0|[]- a(b(x)) -35|[]-> c(b(x))
       a(a(c(x9784))) <-0|0[]- a(a(b(x9784))) -38|[]-> a(c(b(x9784)))
       c(a(c(x9785))) <-0|0[]- c(a(b(x9785))) -42|[]-> b(a(b(x9785)))
       c(a(c(x9786))) <-0|0[]- c(a(b(x9786))) -43|[]-> b(c(b(x9786)))
       c(a(c(x9787))) <-0|0[]- c(a(b(x9787))) -44|[]-> c(b(b(x9787)))
       a(a(c(x9788))) <-0|0[]- a(a(b(x9788))) -45|[]-> c(c(b(x9788)))
       c(c(x)) <-1|[]- a(b(x)) -0|[]-> a(c(x))
       c(c(x)) <-1|[]- a(b(x)) -2|[]-> c(a(x))
       c(c(x)) <-1|[]- a(b(x)) -3|[]-> b(b(x))
       a(c(c(x9792))) <-1|0[]- a(a(b(x9792))) -4|[]-> c(a(b(x9792)))
       c(c(c(x9793))) <-1|0[]- c(a(b(x9793))) -9|[]-> a(c(b(x9793)))
       c(c(c(x9794))) <-1|0[]- c(a(b(x9794))) -10|[]-> c(c(b(x9794)))
       c(c(c(x9795))) <-1|0[]- c(a(b(x9795))) -11|[]-> b(b(b(x9795)))
       a(c(c(x9796))) <-1|0[]- a(a(b(x9796))) -12|[]-> b(b(b(x9796)))
       c(c(x)) <-1|[]- a(b(x)) -17|[]-> a(a(x))
       a(c(c(x9798))) <-1|0[]- a(a(b(x9798))) -21|[]-> b(a(b(x9798)))
       a(c(c(x9799))) <-1|0[]- a(a(b(x9799))) -22|[]-> b(c(b(x9799)))
       c(c(c(x9800))) <-1|0[]- c(a(b(x9800))) -26|[]-> a(a(b(x9800)))
       a(c(c(x9801))) <-1|0[]- a(a(b(x9801))) -27|[]-> c(b(b(x9801)))
       c(c(x)) <-1|[]- a(b(x)) -33|[]-> b(a(x))
       c(c(x)) <-1|[]- a(b(x)) -34|[]-> b(c(x))
       c(c(x)) <-1|[]- a(b(x)) -35|[]-> c(b(x))
       a(c(c(x9805))) <-1|0[]- a(a(b(x9805))) -38|[]-> a(c(b(x9805)))
       c(c(c(x9806))) <-1|0[]- c(a(b(x9806))) -42|[]-> b(a(b(x9806)))
       c(c(c(x9807))) <-1|0[]- c(a(b(x9807))) -43|[]-> b(c(b(x9807)))
       c(c(c(x9808))) <-1|0[]- c(a(b(x9808))) -44|[]-> c(b(b(x9808)))
       a(c(c(x9809))) <-1|0[]- a(a(b(x9809))) -45|[]-> c(c(b(x9809)))
       c(a(x)) <-2|[]- a(b(x)) -0|[]-> a(c(x))
       c(a(x)) <-2|[]- a(b(x)) -1|[]-> c(c(x))
       c(a(x)) <-2|[]- a(b(x)) -3|[]-> b(b(x))
       a(c(a(x9813))) <-2|0[]- a(a(b(x9813))) -4|[]-> c(a(b(x9813)))
       c(c(a(x9814))) <-2|0[]- c(a(b(x9814))) -9|[]-> a(c(b(x9814)))
       c(c(a(x9815))) <-2|0[]- c(a(b(x9815))) -10|[]-> c(c(b(x9815)))
       c(c(a(x9816))) <-2|0[]- c(a(b(x9816))) -11|[]-> b(b(b(x9816)))
       a(c(a(x9817))) <-2|0[]- a(a(b(x9817))) -12|[]-> b(b(b(x9817)))
       c(a(x)) <-2|[]- a(b(x)) -17|[]-> a(a(x))
       a(c(a(x9819))) <-2|0[]- a(a(b(x9819))) -21|[]-> b(a(b(x9819)))
       a(c(a(x9820))) <-2|0[]- a(a(b(x9820))) -22|[]-> b(c(b(x9820)))
       c(c(a(x9821))) <-2|0[]- c(a(b(x9821))) -26|[]-> a(a(b(x9821)))
       a(c(a(x9822))) <-2|0[]- a(a(b(x9822))) -27|[]-> c(b(b(x9822)))
       c(a(x)) <-2|[]- a(b(x)) -33|[]-> b(a(x))
       c(a(x)) <-2|[]- a(b(x)) -34|[]-> b(c(x))
       c(a(x)) <-2|[]- a(b(x)) -35|[]-> c(b(x))
       a(c(a(x9826))) <-2|0[]- a(a(b(x9826))) -38|[]-> a(c(b(x9826)))
       c(c(a(x9827))) <-2|0[]- c(a(b(x9827))) -42|[]-> b(a(b(x9827)))
       c(c(a(x9828))) <-2|0[]- c(a(b(x9828))) -43|[]-> b(c(b(x9828)))
       c(c(a(x9829))) <-2|0[]- c(a(b(x9829))) -44|[]-> c(b(b(x9829)))
       a(c(a(x9830))) <-2|0[]- a(a(b(x9830))) -45|[]-> c(c(b(x9830)))
       b(b(x)) <-3|[]- a(b(x)) -0|[]-> a(c(x))
       b(b(x)) <-3|[]- a(b(x)) -1|[]-> c(c(x))
       b(b(x)) <-3|[]- a(b(x)) -2|[]-> c(a(x))
       a(b(b(x9834))) <-3|0[]- a(a(b(x9834))) -4|[]-> c(a(b(x9834)))
       c(b(b(x9835))) <-3|0[]- c(a(b(x9835))) -9|[]-> a(c(b(x9835)))
       c(b(b(x9836))) <-3|0[]- c(a(b(x9836))) -10|[]-> c(c(b(x9836)))
       c(b(b(x9837))) <-3|0[]- c(a(b(x9837))) -11|[]-> b(b(b(x9837)))
       a(b(b(x9838))) <-3|0[]- a(a(b(x9838))) -12|[]-> b(b(b(x9838)))
       b(b(x)) <-3|[]- a(b(x)) -17|[]-> a(a(x))
       a(b(b(x9840))) <-3|0[]- a(a(b(x9840))) -21|[]-> b(a(b(x9840)))
       a(b(b(x9841))) <-3|0[]- a(a(b(x9841))) -22|[]-> b(c(b(x9841)))
       c(b(b(x9842))) <-3|0[]- c(a(b(x9842))) -26|[]-> a(a(b(x9842)))
       a(b(b(x9843))) <-3|0[]- a(a(b(x9843))) -27|[]-> c(b(b(x9843)))
       b(b(x)) <-3|[]- a(b(x)) -33|[]-> b(a(x))
       b(b(x)) <-3|[]- a(b(x)) -34|[]-> b(c(x))
       b(b(x)) <-3|[]- a(b(x)) -35|[]-> c(b(x))
       a(b(b(x9847))) <-3|0[]- a(a(b(x9847))) -38|[]-> a(c(b(x9847)))
       c(b(b(x9848))) <-3|0[]- c(a(b(x9848))) -42|[]-> b(a(b(x9848)))
       c(b(b(x9849))) <-3|0[]- c(a(b(x9849))) -43|[]-> b(c(b(x9849)))
       c(b(b(x9850))) <-3|0[]- c(a(b(x9850))) -44|[]-> c(b(b(x9850)))
       a(b(b(x9851))) <-3|0[]- a(a(b(x9851))) -45|[]-> c(c(b(x9851)))
       a(c(a(x9852))) <-4|0[]- a(a(a(x9852))) -4|[]-> c(a(a(x9852)))
       c(c(a(x9853))) <-4|0[]- c(a(a(x9853))) -9|[]-> a(c(a(x9853)))
       c(c(a(x9854))) <-4|0[]- c(a(a(x9854))) -10|[]-> c(c(a(x9854)))
       c(c(a(x9855))) <-4|0[]- c(a(a(x9855))) -11|[]-> b(b(a(x9855)))
       c(a(x)) <-4|[]- a(a(x)) -12|[]-> b(b(x))
       a(c(a(x9857))) <-4|0[]- a(a(a(x9857))) -12|[]-> b(b(a(x9857)))
       c(a(x)) <-4|[]- a(a(x)) -21|[]-> b(a(x))
       a(c(a(x9859))) <-4|0[]- a(a(a(x9859))) -21|[]-> b(a(a(x9859)))
       c(a(x)) <-4|[]- a(a(x)) -22|[]-> b(c(x))
       a(c(a(x9861))) <-4|0[]- a(a(a(x9861))) -22|[]-> b(c(a(x9861)))
       c(c(a(x9862))) <-4|0[]- c(a(a(x9862))) -26|[]-> a(a(a(x9862)))
       c(a(x)) <-4|[]- a(a(x)) -27|[]-> c(b(x))
       a(c(a(x9864))) <-4|0[]- a(a(a(x9864))) -27|[]-> c(b(a(x9864)))
       c(a(x)) <-4|[]- a(a(x)) -38|[]-> a(c(x))
       a(c(a(x9866))) <-4|0[]- a(a(a(x9866))) -38|[]-> a(c(a(x9866)))
       c(c(a(x9867))) <-4|0[]- c(a(a(x9867))) -42|[]-> b(a(a(x9867)))
       c(c(a(x9868))) <-4|0[]- c(a(a(x9868))) -43|[]-> b(c(a(x9868)))
       c(c(a(x9869))) <-4|0[]- c(a(a(x9869))) -44|[]-> c(b(a(x9869)))
       c(a(x)) <-4|[]- a(a(x)) -45|[]-> c(c(x))
       a(c(a(x9871))) <-4|0[]- a(a(a(x9871))) -45|[]-> c(c(a(x9871)))
       a(a(a(x9872))) <-5|0[]- a(b(c(x9872))) -0|[]-> a(c(c(x9872)))
       a(a(a(x9873))) <-5|0[]- a(b(c(x9873))) -1|[]-> c(c(c(x9873)))
       a(a(a(x9874))) <-5|0[]- a(b(c(x9874))) -2|[]-> c(a(c(x9874)))
       a(a(a(x9875))) <-5|0[]- a(b(c(x9875))) -3|[]-> b(b(c(x9875)))
       a(a(x)) <-5|[]- b(c(x)) -6|[]-> c(b(x))
       b(a(a(x9877))) <-5|0[]- b(b(c(x9877))) -13|[]-> c(a(c(x9877)))
       b(a(a(x9878))) <-5|0[]- b(b(c(x9878))) -14|[]-> b(a(c(x9878)))
       a(a(a(x9879))) <-5|0[]- a(b(c(x9879))) -17|[]-> a(a(c(x9879)))
       c(a(a(x9880))) <-5|0[]- c(b(c(x9880))) -18|[]-> b(c(c(x9880)))
       a(a(x)) <-5|[]- b(c(x)) -20|[]-> b(a(x))
       a(a(x)) <-5|[]- b(c(x)) -23|[]-> a(c(x))
       c(a(a(x9883))) <-5|0[]- c(b(c(x9883))) -24|[]-> a(c(c(x9883)))
       b(a(a(x9884))) <-5|0[]- b(b(c(x9884))) -28|[]-> c(b(c(x9884)))
       c(a(a(x9885))) <-5|0[]- c(b(c(x9885))) -29|[]-> c(c(c(x9885)))
       b(a(a(x9886))) <-5|0[]- b(b(c(x9886))) -31|[]-> c(c(c(x9886)))
       a(a(a(x9887))) <-5|0[]- a(b(c(x9887))) -33|[]-> b(a(c(x9887)))
       a(a(a(x9888))) <-5|0[]- a(b(c(x9888))) -34|[]-> b(c(c(x9888)))
       a(a(a(x9889))) <-5|0[]- a(b(c(x9889))) -35|[]-> c(b(c(x9889)))
       c(a(a(x9890))) <-5|0[]- c(b(c(x9890))) -36|[]-> b(a(c(x9890)))
       a(a(x)) <-5|[]- b(c(x)) -39|[]-> c(a(x))
       c(a(a(x9892))) <-5|0[]- c(b(c(x9892))) -40|[]-> c(a(c(x9892)))
       b(a(a(x9893))) <-5|0[]- b(b(c(x9893))) -46|[]-> b(c(c(x9893)))
       b(a(a(x9894))) <-5|0[]- b(b(c(x9894))) -47|[]-> a(c(c(x9894)))
       c(a(a(x9895))) <-5|0[]- c(b(c(x9895))) -48|[]-> b(b(c(x9895)))
       c(a(a(x9896))) <-5|0[]- c(b(c(x9896))) -49|[]-> a(a(c(x9896)))
       b(a(a(x9897))) <-5|0[]- b(b(c(x9897))) -51|[]-> a(a(c(x9897)))
       a(c(b(x9898))) <-6|0[]- a(b(c(x9898))) -0|[]-> a(c(c(x9898)))
       a(c(b(x9899))) <-6|0[]- a(b(c(x9899))) -1|[]-> c(c(c(x9899)))
       a(c(b(x9900))) <-6|0[]- a(b(c(x9900))) -2|[]-> c(a(c(x9900)))
       a(c(b(x9901))) <-6|0[]- a(b(c(x9901))) -3|[]-> b(b(c(x9901)))
       c(b(x)) <-6|[]- b(c(x)) -5|[]-> a(a(x))
       b(c(b(x9903))) <-6|0[]- b(b(c(x9903))) -13|[]-> c(a(c(x9903)))
       b(c(b(x9904))) <-6|0[]- b(b(c(x9904))) -14|[]-> b(a(c(x9904)))
       a(c(b(x9905))) <-6|0[]- a(b(c(x9905))) -17|[]-> a(a(c(x9905)))
       c(c(b(x9906))) <-6|0[]- c(b(c(x9906))) -18|[]-> b(c(c(x9906)))
       c(b(x)) <-6|[]- b(c(x)) -20|[]-> b(a(x))
       c(b(x)) <-6|[]- b(c(x)) -23|[]-> a(c(x))
       c(c(b(x9909))) <-6|0[]- c(b(c(x9909))) -24|[]-> a(c(c(x9909)))
       b(c(b(x9910))) <-6|0[]- b(b(c(x9910))) -28|[]-> c(b(c(x9910)))
       c(c(b(x9911))) <-6|0[]- c(b(c(x9911))) -29|[]-> c(c(c(x9911)))
       b(c(b(x9912))) <-6|0[]- b(b(c(x9912))) -31|[]-> c(c(c(x9912)))
       a(c(b(x9913))) <-6|0[]- a(b(c(x9913))) -33|[]-> b(a(c(x9913)))
       a(c(b(x9914))) <-6|0[]- a(b(c(x9914))) -34|[]-> b(c(c(x9914)))
       a(c(b(x9915))) <-6|0[]- a(b(c(x9915))) -35|[]-> c(b(c(x9915)))
       c(c(b(x9916))) <-6|0[]- c(b(c(x9916))) -36|[]-> b(a(c(x9916)))
       c(b(x)) <-6|[]- b(c(x)) -39|[]-> c(a(x))
       c(c(b(x9918))) <-6|0[]- c(b(c(x9918))) -40|[]-> c(a(c(x9918)))
       b(c(b(x9919))) <-6|0[]- b(b(c(x9919))) -46|[]-> b(c(c(x9919)))
       b(c(b(x9920))) <-6|0[]- b(b(c(x9920))) -47|[]-> a(c(c(x9920)))
       c(c(b(x9921))) <-6|0[]- c(b(c(x9921))) -48|[]-> b(b(c(x9921)))
       c(c(b(x9922))) <-6|0[]- c(b(c(x9922))) -49|[]-> a(a(c(x9922)))
       b(c(b(x9923))) <-6|0[]- b(b(c(x9923))) -51|[]-> a(a(c(x9923)))
       a(c(b(x9924))) <-7|0[]- a(a(c(x9924))) -4|[]-> c(a(c(x9924)))
       c(b(x)) <-7|[]- a(c(x)) -8|[]-> c(c(x))
       c(c(b(x9926))) <-7|0[]- c(a(c(x9926))) -9|[]-> a(c(c(x9926)))
       c(c(b(x9927))) <-7|0[]- c(a(c(x9927))) -10|[]-> c(c(c(x9927)))
       c(c(b(x9928))) <-7|0[]- c(a(c(x9928))) -11|[]-> b(b(c(x9928)))
       a(c(b(x9929))) <-7|0[]- a(a(c(x9929))) -12|[]-> b(b(c(x9929)))
       c(b(x)) <-7|[]- a(c(x)) -19|[]-> b(c(x))
       a(c(b(x9931))) <-7|0[]- a(a(c(x9931))) -21|[]-> b(a(c(x9931)))
       a(c(b(x9932))) <-7|0[]- a(a(c(x9932))) -22|[]-> b(c(c(x9932)))
       c(b(x)) <-7|[]- a(c(x)) -25|[]-> c(a(x))
       c(c(b(x9934))) <-7|0[]- c(a(c(x9934))) -26|[]-> a(a(c(x9934)))
       a(c(b(x9935))) <-7|0[]- a(a(c(x9935))) -27|[]-> c(b(c(x9935)))
       c(b(x)) <-7|[]- a(c(x)) -37|[]-> b(a(x))
       a(c(b(x9937))) <-7|0[]- a(a(c(x9937))) -38|[]-> a(c(c(x9937)))
       c(b(x)) <-7|[]- a(c(x)) -41|[]-> a(a(x))
       c(c(b(x9939))) <-7|0[]- c(a(c(x9939))) -42|[]-> b(a(c(x9939)))
       c(c(b(x9940))) <-7|0[]- c(a(c(x9940))) -43|[]-> b(c(c(x9940)))
       c(c(b(x9941))) <-7|0[]- c(a(c(x9941))) -44|[]-> c(b(c(x9941)))
       a(c(b(x9942))) <-7|0[]- a(a(c(x9942))) -45|[]-> c(c(c(x9942)))
       a(c(c(x9943))) <-8|0[]- a(a(c(x9943))) -4|[]-> c(a(c(x9943)))
       c(c(x)) <-8|[]- a(c(x)) -7|[]-> c(b(x))
       c(c(c(x9945))) <-8|0[]- c(a(c(x9945))) -9|[]-> a(c(c(x9945)))
       c(c(c(x9946))) <-8|0[]- c(a(c(x9946))) -10|[]-> c(c(c(x9946)))
       c(c(c(x9947))) <-8|0[]- c(a(c(x9947))) -11|[]-> b(b(c(x9947)))
       a(c(c(x9948))) <-8|0[]- a(a(c(x9948))) -12|[]-> b(b(c(x9948)))
       c(c(x)) <-8|[]- a(c(x)) -19|[]-> b(c(x))
       a(c(c(x9950))) <-8|0[]- a(a(c(x9950))) -21|[]-> b(a(c(x9950)))
       a(c(c(x9951))) <-8|0[]- a(a(c(x9951))) -22|[]-> b(c(c(x9951)))
       c(c(x)) <-8|[]- a(c(x)) -25|[]-> c(a(x))
       c(c(c(x9953))) <-8|0[]- c(a(c(x9953))) -26|[]-> a(a(c(x9953)))
       a(c(c(x9954))) <-8|0[]- a(a(c(x9954))) -27|[]-> c(b(c(x9954)))
       c(c(x)) <-8|[]- a(c(x)) -37|[]-> b(a(x))
       a(c(c(x9956))) <-8|0[]- a(a(c(x9956))) -38|[]-> a(c(c(x9956)))
       c(c(x)) <-8|[]- a(c(x)) -41|[]-> a(a(x))
       c(c(c(x9958))) <-8|0[]- c(a(c(x9958))) -42|[]-> b(a(c(x9958)))
       c(c(c(x9959))) <-8|0[]- c(a(c(x9959))) -43|[]-> b(c(c(x9959)))
       c(c(c(x9960))) <-8|0[]- c(a(c(x9960))) -44|[]-> c(b(c(x9960)))
       a(c(c(x9961))) <-8|0[]- a(a(c(x9961))) -45|[]-> c(c(c(x9961)))
       b(a(c(x9962))) <-9|0[]- b(c(a(x9962))) -5|[]-> a(a(a(x9962)))
       b(a(c(x9963))) <-9|0[]- b(c(a(x9963))) -6|[]-> c(b(a(x9963)))
       a(a(c(x9964))) <-9|0[]- a(c(a(x9964))) -7|[]-> c(b(a(x9964)))
       a(a(c(x9965))) <-9|0[]- a(c(a(x9965))) -8|[]-> c(c(a(x9965)))
       a(c(x)) <-9|[]- c(a(x)) -10|[]-> c(c(x))
       a(c(x)) <-9|[]- c(a(x)) -11|[]-> b(b(x))
       c(a(c(x9968))) <-9|0[]- c(c(a(x9968))) -15|[]-> a(c(a(x9968)))
       c(a(c(x9969))) <-9|0[]- c(c(a(x9969))) -16|[]-> c(a(a(x9969)))
       a(a(c(x9970))) <-9|0[]- a(c(a(x9970))) -19|[]-> b(c(a(x9970)))
       b(a(c(x9971))) <-9|0[]- b(c(a(x9971))) -20|[]-> b(a(a(x9971)))
       b(a(c(x9972))) <-9|0[]- b(c(a(x9972))) -23|[]-> a(c(a(x9972)))
       a(a(c(x9973))) <-9|0[]- a(c(a(x9973))) -25|[]-> c(a(a(x9973)))
       a(c(x)) <-9|[]- c(a(x)) -26|[]-> a(a(x))
       c(a(c(x9975))) <-9|0[]- c(c(a(x9975))) -30|[]-> b(b(a(x9975)))
       c(a(c(x9976))) <-9|0[]- c(c(a(x9976))) -32|[]-> a(a(a(x9976)))
       a(a(c(x9977))) <-9|0[]- a(c(a(x9977))) -37|[]-> b(a(a(x9977)))
       b(a(c(x9978))) <-9|0[]- b(c(a(x9978))) -39|[]-> c(a(a(x9978)))
       a(a(c(x9979))) <-9|0[]- a(c(a(x9979))) -41|[]-> a(a(a(x9979)))
       a(c(x)) <-9|[]- c(a(x)) -42|[]-> b(a(x))
       a(c(x)) <-9|[]- c(a(x)) -43|[]-> b(c(x))
       a(c(x)) <-9|[]- c(a(x)) -44|[]-> c(b(x))
       c(a(c(x9983))) <-9|0[]- c(c(a(x9983))) -50|[]-> c(b(a(x9983)))
       c(a(c(x9984))) <-9|0[]- c(c(a(x9984))) -52|[]-> b(a(a(x9984)))
       c(a(c(x9985))) <-9|0[]- c(c(a(x9985))) -53|[]-> b(c(a(x9985)))
       b(c(c(x9986))) <-10|0[]- b(c(a(x9986))) -5|[]-> a(a(a(x9986)))
       b(c(c(x9987))) <-10|0[]- b(c(a(x9987))) -6|[]-> c(b(a(x9987)))
       a(c(c(x9988))) <-10|0[]- a(c(a(x9988))) -7|[]-> c(b(a(x9988)))
       a(c(c(x9989))) <-10|0[]- a(c(a(x9989))) -8|[]-> c(c(a(x9989)))
       c(c(x)) <-10|[]- c(a(x)) -9|[]-> a(c(x))
       c(c(x)) <-10|[]- c(a(x)) -11|[]-> b(b(x))
       c(c(c(x9992))) <-10|0[]- c(c(a(x9992))) -15|[]-> a(c(a(x9992)))
       c(c(c(x9993))) <-10|0[]- c(c(a(x9993))) -16|[]-> c(a(a(x9993)))
       a(c(c(x9994))) <-10|0[]- a(c(a(x9994))) -19|[]-> b(c(a(x9994)))
       b(c(c(x9995))) <-10|0[]- b(c(a(x9995))) -20|[]-> b(a(a(x9995)))
       b(c(c(x9996))) <-10|0[]- b(c(a(x9996))) -23|[]-> a(c(a(x9996)))
       a(c(c(x9997))) <-10|0[]- a(c(a(x9997))) -25|[]-> c(a(a(x9997)))
       c(c(x)) <-10|[]- c(a(x)) -26|[]-> a(a(x))
       c(c(c(x9999))) <-10|0[]- c(c(a(x9999))) -30|[]-> b(b(a(x9999)))
       c(c(c(x10000))) <-10|0[]- c(c(a(x10000))) -32|[]-> a(a(a(x10000)))
       a(c(c(x10001))) <-10|0[]- a(c(a(x10001))) -37|[]-> b(a(a(x10001)))
       b(c(c(x10002))) <-10|0[]- b(c(a(x10002))) -39|[]-> c(a(a(x10002)))
       a(c(c(x10003))) <-10|0[]- a(c(a(x10003))) -41|[]-> a(a(a(x10003)))
       c(c(x)) <-10|[]- c(a(x)) -42|[]-> b(a(x))
       c(c(x)) <-10|[]- c(a(x)) -43|[]-> b(c(x))
       c(c(x)) <-10|[]- c(a(x)) -44|[]-> c(b(x))
       c(c(c(x10007))) <-10|0[]- c(c(a(x10007))) -50|[]-> c(b(a(x10007)))
       c(c(c(x10008))) <-10|0[]- c(c(a(x10008))) -52|[]-> b(a(a(x10008)))
       c(c(c(x10009))) <-10|0[]- c(c(a(x10009))) -53|[]-> b(c(a(x10009)))
       b(b(b(x10010))) <-11|0[]- b(c(a(x10010))) -5|[]-> a(a(a(x10010)))
       b(b(b(x10011))) <-11|0[]- b(c(a(x10011))) -6|[]-> c(b(a(x10011)))
       a(b(b(x10012))) <-11|0[]- a(c(a(x10012))) -7|[]-> c(b(a(x10012)))
       a(b(b(x10013))) <-11|0[]- a(c(a(x10013))) -8|[]-> c(c(a(x10013)))
       b(b(x)) <-11|[]- c(a(x)) -9|[]-> a(c(x))
       b(b(x)) <-11|[]- c(a(x)) -10|[]-> c(c(x))
       c(b(b(x10016))) <-11|0[]- c(c(a(x10016))) -15|[]-> a(c(a(x10016)))
       c(b(b(x10017))) <-11|0[]- c(c(a(x10017))) -16|[]-> c(a(a(x10017)))
       a(b(b(x10018))) <-11|0[]- a(c(a(x10018))) -19|[]-> b(c(a(x10018)))
       b(b(b(x10019))) <-11|0[]- b(c(a(x10019))) -20|[]-> b(a(a(x10019)))
       b(b(b(x10020))) <-11|0[]- b(c(a(x10020))) -23|[]-> a(c(a(x10020)))
       a(b(b(x10021))) <-11|0[]- a(c(a(x10021))) -25|[]-> c(a(a(x10021)))
       b(b(x)) <-11|[]- c(a(x)) -26|[]-> a(a(x))
       c(b(b(x10023))) <-11|0[]- c(c(a(x10023))) -30|[]-> b(b(a(x10023)))
       c(b(b(x10024))) <-11|0[]- c(c(a(x10024))) -32|[]-> a(a(a(x10024)))
       a(b(b(x10025))) <-11|0[]- a(c(a(x10025))) -37|[]-> b(a(a(x10025)))
       b(b(b(x10026))) <-11|0[]- b(c(a(x10026))) -39|[]-> c(a(a(x10026)))
       a(b(b(x10027))) <-11|0[]- a(c(a(x10027))) -41|[]-> a(a(a(x10027)))
       b(b(x)) <-11|[]- c(a(x)) -42|[]-> b(a(x))
       b(b(x)) <-11|[]- c(a(x)) -43|[]-> b(c(x))
       b(b(x)) <-11|[]- c(a(x)) -44|[]-> c(b(x))
       c(b(b(x10031))) <-11|0[]- c(c(a(x10031))) -50|[]-> c(b(a(x10031)))
       c(b(b(x10032))) <-11|0[]- c(c(a(x10032))) -52|[]-> b(a(a(x10032)))
       c(b(b(x10033))) <-11|0[]- c(c(a(x10033))) -53|[]-> b(c(a(x10033)))
       b(b(x)) <-12|[]- a(a(x)) -4|[]-> c(a(x))
       a(b(b(x10035))) <-12|0[]- a(a(a(x10035))) -4|[]-> c(a(a(x10035)))
       c(b(b(x10036))) <-12|0[]- c(a(a(x10036))) -9|[]-> a(c(a(x10036)))
       c(b(b(x10037))) <-12|0[]- c(a(a(x10037))) -10|[]-> c(c(a(x10037)))
       c(b(b(x10038))) <-12|0[]- c(a(a(x10038))) -11|[]-> b(b(a(x10038)))
       a(b(b(x10039))) <-12|0[]- a(a(a(x10039))) -12|[]-> b(b(a(x10039)))
       b(b(x)) <-12|[]- a(a(x)) -21|[]-> b(a(x))
       a(b(b(x10041))) <-12|0[]- a(a(a(x10041))) -21|[]-> b(a(a(x10041)))
       b(b(x)) <-12|[]- a(a(x)) -22|[]-> b(c(x))
       a(b(b(x10043))) <-12|0[]- a(a(a(x10043))) -22|[]-> b(c(a(x10043)))
       c(b(b(x10044))) <-12|0[]- c(a(a(x10044))) -26|[]-> a(a(a(x10044)))
       b(b(x)) <-12|[]- a(a(x)) -27|[]-> c(b(x))
       a(b(b(x10046))) <-12|0[]- a(a(a(x10046))) -27|[]-> c(b(a(x10046)))
       b(b(x)) <-12|[]- a(a(x)) -38|[]-> a(c(x))
       a(b(b(x10048))) <-12|0[]- a(a(a(x10048))) -38|[]-> a(c(a(x10048)))
       c(b(b(x10049))) <-12|0[]- c(a(a(x10049))) -42|[]-> b(a(a(x10049)))
       c(b(b(x10050))) <-12|0[]- c(a(a(x10050))) -43|[]-> b(c(a(x10050)))
       c(b(b(x10051))) <-12|0[]- c(a(a(x10051))) -44|[]-> c(b(a(x10051)))
       b(b(x)) <-12|[]- a(a(x)) -45|[]-> c(c(x))
       a(b(b(x10053))) <-12|0[]- a(a(a(x10053))) -45|[]-> c(c(a(x10053)))
       a(c(a(x10054))) <-13|0[]- a(b(b(x10054))) -0|[]-> a(c(b(x10054)))
       a(c(a(x10055))) <-13|0[]- a(b(b(x10055))) -1|[]-> c(c(b(x10055)))
       a(c(a(x10056))) <-13|0[]- a(b(b(x10056))) -2|[]-> c(a(b(x10056)))
       a(c(a(x10057))) <-13|0[]- a(b(b(x10057))) -3|[]-> b(b(b(x10057)))
       b(c(a(x10058))) <-13|0[]- b(b(b(x10058))) -13|[]-> c(a(b(x10058)))
       c(a(x)) <-13|[]- b(b(x)) -14|[]-> b(a(x))
       b(c(a(x10060))) <-13|0[]- b(b(b(x10060))) -14|[]-> b(a(b(x10060)))
       a(c(a(x10061))) <-13|0[]- a(b(b(x10061))) -17|[]-> a(a(b(x10061)))
       c(c(a(x10062))) <-13|0[]- c(b(b(x10062))) -18|[]-> b(c(b(x10062)))
       c(c(a(x10063))) <-13|0[]- c(b(b(x10063))) -24|[]-> a(c(b(x10063)))
       c(a(x)) <-13|[]- b(b(x)) -28|[]-> c(b(x))
       b(c(a(x10065))) <-13|0[]- b(b(b(x10065))) -28|[]-> c(b(b(x10065)))
       c(c(a(x10066))) <-13|0[]- c(b(b(x10066))) -29|[]-> c(c(b(x10066)))
       c(a(x)) <-13|[]- b(b(x)) -31|[]-> c(c(x))
       b(c(a(x10068))) <-13|0[]- b(b(b(x10068))) -31|[]-> c(c(b(x10068)))
       a(c(a(x10069))) <-13|0[]- a(b(b(x10069))) -33|[]-> b(a(b(x10069)))
       a(c(a(x10070))) <-13|0[]- a(b(b(x10070))) -34|[]-> b(c(b(x10070)))
       a(c(a(x10071))) <-13|0[]- a(b(b(x10071))) -35|[]-> c(b(b(x10071)))
       c(c(a(x10072))) <-13|0[]- c(b(b(x10072))) -36|[]-> b(a(b(x10072)))
       c(c(a(x10073))) <-13|0[]- c(b(b(x10073))) -40|[]-> c(a(b(x10073)))
       c(a(x)) <-13|[]- b(b(x)) -46|[]-> b(c(x))
       b(c(a(x10075))) <-13|0[]- b(b(b(x10075))) -46|[]-> b(c(b(x10075)))
       c(a(x)) <-13|[]- b(b(x)) -47|[]-> a(c(x))
       b(c(a(x10077))) <-13|0[]- b(b(b(x10077))) -47|[]-> a(c(b(x10077)))
       c(c(a(x10078))) <-13|0[]- c(b(b(x10078))) -48|[]-> b(b(b(x10078)))
       c(c(a(x10079))) <-13|0[]- c(b(b(x10079))) -49|[]-> a(a(b(x10079)))
       c(a(x)) <-13|[]- b(b(x)) -51|[]-> a(a(x))
       b(c(a(x10081))) <-13|0[]- b(b(b(x10081))) -51|[]-> a(a(b(x10081)))
       a(b(a(x10082))) <-14|0[]- a(b(b(x10082))) -0|[]-> a(c(b(x10082)))
       a(b(a(x10083))) <-14|0[]- a(b(b(x10083))) -1|[]-> c(c(b(x10083)))
       a(b(a(x10084))) <-14|0[]- a(b(b(x10084))) -2|[]-> c(a(b(x10084)))
       a(b(a(x10085))) <-14|0[]- a(b(b(x10085))) -3|[]-> b(b(b(x10085)))
       b(a(x)) <-14|[]- b(b(x)) -13|[]-> c(a(x))
       b(b(a(x10087))) <-14|0[]- b(b(b(x10087))) -13|[]-> c(a(b(x10087)))
       b(b(a(x10088))) <-14|0[]- b(b(b(x10088))) -14|[]-> b(a(b(x10088)))
       a(b(a(x10089))) <-14|0[]- a(b(b(x10089))) -17|[]-> a(a(b(x10089)))
       c(b(a(x10090))) <-14|0[]- c(b(b(x10090))) -18|[]-> b(c(b(x10090)))
       c(b(a(x10091))) <-14|0[]- c(b(b(x10091))) -24|[]-> a(c(b(x10091)))
       b(a(x)) <-14|[]- b(b(x)) -28|[]-> c(b(x))
       b(b(a(x10093))) <-14|0[]- b(b(b(x10093))) -28|[]-> c(b(b(x10093)))
       c(b(a(x10094))) <-14|0[]- c(b(b(x10094))) -29|[]-> c(c(b(x10094)))
       b(a(x)) <-14|[]- b(b(x)) -31|[]-> c(c(x))
       b(b(a(x10096))) <-14|0[]- b(b(b(x10096))) -31|[]-> c(c(b(x10096)))
       a(b(a(x10097))) <-14|0[]- a(b(b(x10097))) -33|[]-> b(a(b(x10097)))
       a(b(a(x10098))) <-14|0[]- a(b(b(x10098))) -34|[]-> b(c(b(x10098)))
       a(b(a(x10099))) <-14|0[]- a(b(b(x10099))) -35|[]-> c(b(b(x10099)))
       c(b(a(x10100))) <-14|0[]- c(b(b(x10100))) -36|[]-> b(a(b(x10100)))
       c(b(a(x10101))) <-14|0[]- c(b(b(x10101))) -40|[]-> c(a(b(x10101)))
       b(a(x)) <-14|[]- b(b(x)) -46|[]-> b(c(x))
       b(b(a(x10103))) <-14|0[]- b(b(b(x10103))) -46|[]-> b(c(b(x10103)))
       b(a(x)) <-14|[]- b(b(x)) -47|[]-> a(c(x))
       b(b(a(x10105))) <-14|0[]- b(b(b(x10105))) -47|[]-> a(c(b(x10105)))
       c(b(a(x10106))) <-14|0[]- c(b(b(x10106))) -48|[]-> b(b(b(x10106)))
       c(b(a(x10107))) <-14|0[]- c(b(b(x10107))) -49|[]-> a(a(b(x10107)))
       b(a(x)) <-14|[]- b(b(x)) -51|[]-> a(a(x))
       b(b(a(x10109))) <-14|0[]- b(b(b(x10109))) -51|[]-> a(a(b(x10109)))
       b(a(c(x10110))) <-15|0[]- b(c(c(x10110))) -5|[]-> a(a(c(x10110)))
       b(a(c(x10111))) <-15|0[]- b(c(c(x10111))) -6|[]-> c(b(c(x10111)))
       a(a(c(x10112))) <-15|0[]- a(c(c(x10112))) -7|[]-> c(b(c(x10112)))
       a(a(c(x10113))) <-15|0[]- a(c(c(x10113))) -8|[]-> c(c(c(x10113)))
       c(a(c(x10114))) <-15|0[]- c(c(c(x10114))) -15|[]-> a(c(c(x10114)))
       a(c(x)) <-15|[]- c(c(x)) -16|[]-> c(a(x))
       c(a(c(x10116))) <-15|0[]- c(c(c(x10116))) -16|[]-> c(a(c(x10116)))
       a(a(c(x10117))) <-15|0[]- a(c(c(x10117))) -19|[]-> b(c(c(x10117)))
       b(a(c(x10118))) <-15|0[]- b(c(c(x10118))) -20|[]-> b(a(c(x10118)))
       b(a(c(x10119))) <-15|0[]- b(c(c(x10119))) -23|[]-> a(c(c(x10119)))
       a(a(c(x10120))) <-15|0[]- a(c(c(x10120))) -25|[]-> c(a(c(x10120)))
       a(c(x)) <-15|[]- c(c(x)) -30|[]-> b(b(x))
       c(a(c(x10122))) <-15|0[]- c(c(c(x10122))) -30|[]-> b(b(c(x10122)))
       a(c(x)) <-15|[]- c(c(x)) -32|[]-> a(a(x))
       c(a(c(x10124))) <-15|0[]- c(c(c(x10124))) -32|[]-> a(a(c(x10124)))
       a(a(c(x10125))) <-15|0[]- a(c(c(x10125))) -37|[]-> b(a(c(x10125)))
       b(a(c(x10126))) <-15|0[]- b(c(c(x10126))) -39|[]-> c(a(c(x10126)))
       a(a(c(x10127))) <-15|0[]- a(c(c(x10127))) -41|[]-> a(a(c(x10127)))
       a(c(x)) <-15|[]- c(c(x)) -50|[]-> c(b(x))
       c(a(c(x10129))) <-15|0[]- c(c(c(x10129))) -50|[]-> c(b(c(x10129)))
       a(c(x)) <-15|[]- c(c(x)) -52|[]-> b(a(x))
       c(a(c(x10131))) <-15|0[]- c(c(c(x10131))) -52|[]-> b(a(c(x10131)))
       a(c(x)) <-15|[]- c(c(x)) -53|[]-> b(c(x))
       c(a(c(x10133))) <-15|0[]- c(c(c(x10133))) -53|[]-> b(c(c(x10133)))
       b(c(a(x10134))) <-16|0[]- b(c(c(x10134))) -5|[]-> a(a(c(x10134)))
       b(c(a(x10135))) <-16|0[]- b(c(c(x10135))) -6|[]-> c(b(c(x10135)))
       a(c(a(x10136))) <-16|0[]- a(c(c(x10136))) -7|[]-> c(b(c(x10136)))
       a(c(a(x10137))) <-16|0[]- a(c(c(x10137))) -8|[]-> c(c(c(x10137)))
       c(a(x)) <-16|[]- c(c(x)) -15|[]-> a(c(x))
       c(c(a(x10139))) <-16|0[]- c(c(c(x10139))) -15|[]-> a(c(c(x10139)))
       c(c(a(x10140))) <-16|0[]- c(c(c(x10140))) -16|[]-> c(a(c(x10140)))
       a(c(a(x10141))) <-16|0[]- a(c(c(x10141))) -19|[]-> b(c(c(x10141)))
       b(c(a(x10142))) <-16|0[]- b(c(c(x10142))) -20|[]-> b(a(c(x10142)))
       b(c(a(x10143))) <-16|0[]- b(c(c(x10143))) -23|[]-> a(c(c(x10143)))
       a(c(a(x10144))) <-16|0[]- a(c(c(x10144))) -25|[]-> c(a(c(x10144)))
       c(a(x)) <-16|[]- c(c(x)) -30|[]-> b(b(x))
       c(c(a(x10146))) <-16|0[]- c(c(c(x10146))) -30|[]-> b(b(c(x10146)))
       c(a(x)) <-16|[]- c(c(x)) -32|[]-> a(a(x))
       c(c(a(x10148))) <-16|0[]- c(c(c(x10148))) -32|[]-> a(a(c(x10148)))
       a(c(a(x10149))) <-16|0[]- a(c(c(x10149))) -37|[]-> b(a(c(x10149)))
       b(c(a(x10150))) <-16|0[]- b(c(c(x10150))) -39|[]-> c(a(c(x10150)))
       a(c(a(x10151))) <-16|0[]- a(c(c(x10151))) -41|[]-> a(a(c(x10151)))
       c(a(x)) <-16|[]- c(c(x)) -50|[]-> c(b(x))
       c(c(a(x10153))) <-16|0[]- c(c(c(x10153))) -50|[]-> c(b(c(x10153)))
       c(a(x)) <-16|[]- c(c(x)) -52|[]-> b(a(x))
       c(c(a(x10155))) <-16|0[]- c(c(c(x10155))) -52|[]-> b(a(c(x10155)))
       c(a(x)) <-16|[]- c(c(x)) -53|[]-> b(c(x))
       c(c(a(x10157))) <-16|0[]- c(c(c(x10157))) -53|[]-> b(c(c(x10157)))
       a(a(x)) <-17|[]- a(b(x)) -0|[]-> a(c(x))
       a(a(x)) <-17|[]- a(b(x)) -1|[]-> c(c(x))
       a(a(x)) <-17|[]- a(b(x)) -2|[]-> c(a(x))
       a(a(x)) <-17|[]- a(b(x)) -3|[]-> b(b(x))
       a(a(a(x10162))) <-17|0[]- a(a(b(x10162))) -4|[]-> c(a(b(x10162)))
       c(a(a(x10163))) <-17|0[]- c(a(b(x10163))) -9|[]-> a(c(b(x10163)))
       c(a(a(x10164))) <-17|0[]- c(a(b(x10164))) -10|[]-> c(c(b(x10164)))
       c(a(a(x10165))) <-17|0[]- c(a(b(x10165))) -11|[]-> b(b(b(x10165)))
       a(a(a(x10166))) <-17|0[]- a(a(b(x10166))) -12|[]-> b(b(b(x10166)))
       a(a(a(x10167))) <-17|0[]- a(a(b(x10167))) -21|[]-> b(a(b(x10167)))
       a(a(a(x10168))) <-17|0[]- a(a(b(x10168))) -22|[]-> b(c(b(x10168)))
       c(a(a(x10169))) <-17|0[]- c(a(b(x10169))) -26|[]-> a(a(b(x10169)))
       a(a(a(x10170))) <-17|0[]- a(a(b(x10170))) -27|[]-> c(b(b(x10170)))
       a(a(x)) <-17|[]- a(b(x)) -33|[]-> b(a(x))
       a(a(x)) <-17|[]- a(b(x)) -34|[]-> b(c(x))
       a(a(x)) <-17|[]- a(b(x)) -35|[]-> c(b(x))
       a(a(a(x10174))) <-17|0[]- a(a(b(x10174))) -38|[]-> a(c(b(x10174)))
       c(a(a(x10175))) <-17|0[]- c(a(b(x10175))) -42|[]-> b(a(b(x10175)))
       c(a(a(x10176))) <-17|0[]- c(a(b(x10176))) -43|[]-> b(c(b(x10176)))
       c(a(a(x10177))) <-17|0[]- c(a(b(x10177))) -44|[]-> c(b(b(x10177)))
       a(a(a(x10178))) <-17|0[]- a(a(b(x10178))) -45|[]-> c(c(b(x10178)))
       b(b(c(x10179))) <-18|0[]- b(c(b(x10179))) -5|[]-> a(a(b(x10179)))
       b(b(c(x10180))) <-18|0[]- b(c(b(x10180))) -6|[]-> c(b(b(x10180)))
       a(b(c(x10181))) <-18|0[]- a(c(b(x10181))) -7|[]-> c(b(b(x10181)))
       a(b(c(x10182))) <-18|0[]- a(c(b(x10182))) -8|[]-> c(c(b(x10182)))
       c(b(c(x10183))) <-18|0[]- c(c(b(x10183))) -15|[]-> a(c(b(x10183)))
       c(b(c(x10184))) <-18|0[]- c(c(b(x10184))) -16|[]-> c(a(b(x10184)))
       a(b(c(x10185))) <-18|0[]- a(c(b(x10185))) -19|[]-> b(c(b(x10185)))
       b(b(c(x10186))) <-18|0[]- b(c(b(x10186))) -20|[]-> b(a(b(x10186)))
       b(b(c(x10187))) <-18|0[]- b(c(b(x10187))) -23|[]-> a(c(b(x10187)))
       b(c(x)) <-18|[]- c(b(x)) -24|[]-> a(c(x))
       a(b(c(x10189))) <-18|0[]- a(c(b(x10189))) -25|[]-> c(a(b(x10189)))
       b(c(x)) <-18|[]- c(b(x)) -29|[]-> c(c(x))
       c(b(c(x10191))) <-18|0[]- c(c(b(x10191))) -30|[]-> b(b(b(x10191)))
       c(b(c(x10192))) <-18|0[]- c(c(b(x10192))) -32|[]-> a(a(b(x10192)))
       b(c(x)) <-18|[]- c(b(x)) -36|[]-> b(a(x))
       a(b(c(x10194))) <-18|0[]- a(c(b(x10194))) -37|[]-> b(a(b(x10194)))
       b(b(c(x10195))) <-18|0[]- b(c(b(x10195))) -39|[]-> c(a(b(x10195)))
       b(c(x)) <-18|[]- c(b(x)) -40|[]-> c(a(x))
       a(b(c(x10197))) <-18|0[]- a(c(b(x10197))) -41|[]-> a(a(b(x10197)))
       b(c(x)) <-18|[]- c(b(x)) -48|[]-> b(b(x))
       b(c(x)) <-18|[]- c(b(x)) -49|[]-> a(a(x))
       c(b(c(x10200))) <-18|0[]- c(c(b(x10200))) -50|[]-> c(b(b(x10200)))
       c(b(c(x10201))) <-18|0[]- c(c(b(x10201))) -52|[]-> b(a(b(x10201)))
       c(b(c(x10202))) <-18|0[]- c(c(b(x10202))) -53|[]-> b(c(b(x10202)))
       a(b(c(x10203))) <-19|0[]- a(a(c(x10203))) -4|[]-> c(a(c(x10203)))
       b(c(x)) <-19|[]- a(c(x)) -7|[]-> c(b(x))
       b(c(x)) <-19|[]- a(c(x)) -8|[]-> c(c(x))
       c(b(c(x10206))) <-19|0[]- c(a(c(x10206))) -9|[]-> a(c(c(x10206)))
       c(b(c(x10207))) <-19|0[]- c(a(c(x10207))) -10|[]-> c(c(c(x10207)))
       c(b(c(x10208))) <-19|0[]- c(a(c(x10208))) -11|[]-> b(b(c(x10208)))
       a(b(c(x10209))) <-19|0[]- a(a(c(x10209))) -12|[]-> b(b(c(x10209)))
       a(b(c(x10210))) <-19|0[]- a(a(c(x10210))) -21|[]-> b(a(c(x10210)))
       a(b(c(x10211))) <-19|0[]- a(a(c(x10211))) -22|[]-> b(c(c(x10211)))
       b(c(x)) <-19|[]- a(c(x)) -25|[]-> c(a(x))
       c(b(c(x10213))) <-19|0[]- c(a(c(x10213))) -26|[]-> a(a(c(x10213)))
       a(b(c(x10214))) <-19|0[]- a(a(c(x10214))) -27|[]-> c(b(c(x10214)))
       b(c(x)) <-19|[]- a(c(x)) -37|[]-> b(a(x))
       a(b(c(x10216))) <-19|0[]- a(a(c(x10216))) -38|[]-> a(c(c(x10216)))
       b(c(x)) <-19|[]- a(c(x)) -41|[]-> a(a(x))
       c(b(c(x10218))) <-19|0[]- c(a(c(x10218))) -42|[]-> b(a(c(x10218)))
       c(b(c(x10219))) <-19|0[]- c(a(c(x10219))) -43|[]-> b(c(c(x10219)))
       c(b(c(x10220))) <-19|0[]- c(a(c(x10220))) -44|[]-> c(b(c(x10220)))
       a(b(c(x10221))) <-19|0[]- a(a(c(x10221))) -45|[]-> c(c(c(x10221)))
       a(b(a(x10222))) <-20|0[]- a(b(c(x10222))) -0|[]-> a(c(c(x10222)))
       a(b(a(x10223))) <-20|0[]- a(b(c(x10223))) -1|[]-> c(c(c(x10223)))
       a(b(a(x10224))) <-20|0[]- a(b(c(x10224))) -2|[]-> c(a(c(x10224)))
       a(b(a(x10225))) <-20|0[]- a(b(c(x10225))) -3|[]-> b(b(c(x10225)))
       b(a(x)) <-20|[]- b(c(x)) -5|[]-> a(a(x))
       b(a(x)) <-20|[]- b(c(x)) -6|[]-> c(b(x))
       b(b(a(x10228))) <-20|0[]- b(b(c(x10228))) -13|[]-> c(a(c(x10228)))
       b(b(a(x10229))) <-20|0[]- b(b(c(x10229))) -14|[]-> b(a(c(x10229)))
       a(b(a(x10230))) <-20|0[]- a(b(c(x10230))) -17|[]-> a(a(c(x10230)))
       c(b(a(x10231))) <-20|0[]- c(b(c(x10231))) -18|[]-> b(c(c(x10231)))
       b(a(x)) <-20|[]- b(c(x)) -23|[]-> a(c(x))
       c(b(a(x10233))) <-20|0[]- c(b(c(x10233))) -24|[]-> a(c(c(x10233)))
       b(b(a(x10234))) <-20|0[]- b(b(c(x10234))) -28|[]-> c(b(c(x10234)))
       c(b(a(x10235))) <-20|0[]- c(b(c(x10235))) -29|[]-> c(c(c(x10235)))
       b(b(a(x10236))) <-20|0[]- b(b(c(x10236))) -31|[]-> c(c(c(x10236)))
       a(b(a(x10237))) <-20|0[]- a(b(c(x10237))) -33|[]-> b(a(c(x10237)))
       a(b(a(x10238))) <-20|0[]- a(b(c(x10238))) -34|[]-> b(c(c(x10238)))
       a(b(a(x10239))) <-20|0[]- a(b(c(x10239))) -35|[]-> c(b(c(x10239)))
       c(b(a(x10240))) <-20|0[]- c(b(c(x10240))) -36|[]-> b(a(c(x10240)))
       b(a(x)) <-20|[]- b(c(x)) -39|[]-> c(a(x))
       c(b(a(x10242))) <-20|0[]- c(b(c(x10242))) -40|[]-> c(a(c(x10242)))
       b(b(a(x10243))) <-20|0[]- b(b(c(x10243))) -46|[]-> b(c(c(x10243)))
       b(b(a(x10244))) <-20|0[]- b(b(c(x10244))) -47|[]-> a(c(c(x10244)))
       c(b(a(x10245))) <-20|0[]- c(b(c(x10245))) -48|[]-> b(b(c(x10245)))
       c(b(a(x10246))) <-20|0[]- c(b(c(x10246))) -49|[]-> a(a(c(x10246)))
       b(b(a(x10247))) <-20|0[]- b(b(c(x10247))) -51|[]-> a(a(c(x10247)))
       b(a(x)) <-21|[]- a(a(x)) -4|[]-> c(a(x))
       a(b(a(x10249))) <-21|0[]- a(a(a(x10249))) -4|[]-> c(a(a(x10249)))
       c(b(a(x10250))) <-21|0[]- c(a(a(x10250))) -9|[]-> a(c(a(x10250)))
       c(b(a(x10251))) <-21|0[]- c(a(a(x10251))) -10|[]-> c(c(a(x10251)))
       c(b(a(x10252))) <-21|0[]- c(a(a(x10252))) -11|[]-> b(b(a(x10252)))
       b(a(x)) <-21|[]- a(a(x)) -12|[]-> b(b(x))
       a(b(a(x10254))) <-21|0[]- a(a(a(x10254))) -12|[]-> b(b(a(x10254)))
       a(b(a(x10255))) <-21|0[]- a(a(a(x10255))) -21|[]-> b(a(a(x10255)))
       b(a(x)) <-21|[]- a(a(x)) -22|[]-> b(c(x))
       a(b(a(x10257))) <-21|0[]- a(a(a(x10257))) -22|[]-> b(c(a(x10257)))
       c(b(a(x10258))) <-21|0[]- c(a(a(x10258))) -26|[]-> a(a(a(x10258)))
       b(a(x)) <-21|[]- a(a(x)) -27|[]-> c(b(x))
       a(b(a(x10260))) <-21|0[]- a(a(a(x10260))) -27|[]-> c(b(a(x10260)))
       b(a(x)) <-21|[]- a(a(x)) -38|[]-> a(c(x))
       a(b(a(x10262))) <-21|0[]- a(a(a(x10262))) -38|[]-> a(c(a(x10262)))
       c(b(a(x10263))) <-21|0[]- c(a(a(x10263))) -42|[]-> b(a(a(x10263)))
       c(b(a(x10264))) <-21|0[]- c(a(a(x10264))) -43|[]-> b(c(a(x10264)))
       c(b(a(x10265))) <-21|0[]- c(a(a(x10265))) -44|[]-> c(b(a(x10265)))
       b(a(x)) <-21|[]- a(a(x)) -45|[]-> c(c(x))
       a(b(a(x10267))) <-21|0[]- a(a(a(x10267))) -45|[]-> c(c(a(x10267)))
       b(c(x)) <-22|[]- a(a(x)) -4|[]-> c(a(x))
       a(b(c(x10269))) <-22|0[]- a(a(a(x10269))) -4|[]-> c(a(a(x10269)))
       c(b(c(x10270))) <-22|0[]- c(a(a(x10270))) -9|[]-> a(c(a(x10270)))
       c(b(c(x10271))) <-22|0[]- c(a(a(x10271))) -10|[]-> c(c(a(x10271)))
       c(b(c(x10272))) <-22|0[]- c(a(a(x10272))) -11|[]-> b(b(a(x10272)))
       b(c(x)) <-22|[]- a(a(x)) -12|[]-> b(b(x))
       a(b(c(x10274))) <-22|0[]- a(a(a(x10274))) -12|[]-> b(b(a(x10274)))
       b(c(x)) <-22|[]- a(a(x)) -21|[]-> b(a(x))
       a(b(c(x10276))) <-22|0[]- a(a(a(x10276))) -21|[]-> b(a(a(x10276)))
       a(b(c(x10277))) <-22|0[]- a(a(a(x10277))) -22|[]-> b(c(a(x10277)))
       c(b(c(x10278))) <-22|0[]- c(a(a(x10278))) -26|[]-> a(a(a(x10278)))
       b(c(x)) <-22|[]- a(a(x)) -27|[]-> c(b(x))
       a(b(c(x10280))) <-22|0[]- a(a(a(x10280))) -27|[]-> c(b(a(x10280)))
       b(c(x)) <-22|[]- a(a(x)) -38|[]-> a(c(x))
       a(b(c(x10282))) <-22|0[]- a(a(a(x10282))) -38|[]-> a(c(a(x10282)))
       c(b(c(x10283))) <-22|0[]- c(a(a(x10283))) -42|[]-> b(a(a(x10283)))
       c(b(c(x10284))) <-22|0[]- c(a(a(x10284))) -43|[]-> b(c(a(x10284)))
       c(b(c(x10285))) <-22|0[]- c(a(a(x10285))) -44|[]-> c(b(a(x10285)))
       b(c(x)) <-22|[]- a(a(x)) -45|[]-> c(c(x))
       a(b(c(x10287))) <-22|0[]- a(a(a(x10287))) -45|[]-> c(c(a(x10287)))
       a(a(c(x10288))) <-23|0[]- a(b(c(x10288))) -0|[]-> a(c(c(x10288)))
       a(a(c(x10289))) <-23|0[]- a(b(c(x10289))) -1|[]-> c(c(c(x10289)))
       a(a(c(x10290))) <-23|0[]- a(b(c(x10290))) -2|[]-> c(a(c(x10290)))
       a(a(c(x10291))) <-23|0[]- a(b(c(x10291))) -3|[]-> b(b(c(x10291)))
       a(c(x)) <-23|[]- b(c(x)) -5|[]-> a(a(x))
       a(c(x)) <-23|[]- b(c(x)) -6|[]-> c(b(x))
       b(a(c(x10294))) <-23|0[]- b(b(c(x10294))) -13|[]-> c(a(c(x10294)))
       b(a(c(x10295))) <-23|0[]- b(b(c(x10295))) -14|[]-> b(a(c(x10295)))
       a(a(c(x10296))) <-23|0[]- a(b(c(x10296))) -17|[]-> a(a(c(x10296)))
       c(a(c(x10297))) <-23|0[]- c(b(c(x10297))) -18|[]-> b(c(c(x10297)))
       a(c(x)) <-23|[]- b(c(x)) -20|[]-> b(a(x))
       c(a(c(x10299))) <-23|0[]- c(b(c(x10299))) -24|[]-> a(c(c(x10299)))
       b(a(c(x10300))) <-23|0[]- b(b(c(x10300))) -28|[]-> c(b(c(x10300)))
       c(a(c(x10301))) <-23|0[]- c(b(c(x10301))) -29|[]-> c(c(c(x10301)))
       b(a(c(x10302))) <-23|0[]- b(b(c(x10302))) -31|[]-> c(c(c(x10302)))
       a(a(c(x10303))) <-23|0[]- a(b(c(x10303))) -33|[]-> b(a(c(x10303)))
       a(a(c(x10304))) <-23|0[]- a(b(c(x10304))) -34|[]-> b(c(c(x10304)))
       a(a(c(x10305))) <-23|0[]- a(b(c(x10305))) -35|[]-> c(b(c(x10305)))
       c(a(c(x10306))) <-23|0[]- c(b(c(x10306))) -36|[]-> b(a(c(x10306)))
       a(c(x)) <-23|[]- b(c(x)) -39|[]-> c(a(x))
       c(a(c(x10308))) <-23|0[]- c(b(c(x10308))) -40|[]-> c(a(c(x10308)))
       b(a(c(x10309))) <-23|0[]- b(b(c(x10309))) -46|[]-> b(c(c(x10309)))
       b(a(c(x10310))) <-23|0[]- b(b(c(x10310))) -47|[]-> a(c(c(x10310)))
       c(a(c(x10311))) <-23|0[]- c(b(c(x10311))) -48|[]-> b(b(c(x10311)))
       c(a(c(x10312))) <-23|0[]- c(b(c(x10312))) -49|[]-> a(a(c(x10312)))
       b(a(c(x10313))) <-23|0[]- b(b(c(x10313))) -51|[]-> a(a(c(x10313)))
       b(a(c(x10314))) <-24|0[]- b(c(b(x10314))) -5|[]-> a(a(b(x10314)))
       b(a(c(x10315))) <-24|0[]- b(c(b(x10315))) -6|[]-> c(b(b(x10315)))
       a(a(c(x10316))) <-24|0[]- a(c(b(x10316))) -7|[]-> c(b(b(x10316)))
       a(a(c(x10317))) <-24|0[]- a(c(b(x10317))) -8|[]-> c(c(b(x10317)))
       c(a(c(x10318))) <-24|0[]- c(c(b(x10318))) -15|[]-> a(c(b(x10318)))
       c(a(c(x10319))) <-24|0[]- c(c(b(x10319))) -16|[]-> c(a(b(x10319)))
       a(c(x)) <-24|[]- c(b(x)) -18|[]-> b(c(x))
       a(a(c(x10321))) <-24|0[]- a(c(b(x10321))) -19|[]-> b(c(b(x10321)))
       b(a(c(x10322))) <-24|0[]- b(c(b(x10322))) -20|[]-> b(a(b(x10322)))
       b(a(c(x10323))) <-24|0[]- b(c(b(x10323))) -23|[]-> a(c(b(x10323)))
       a(a(c(x10324))) <-24|0[]- a(c(b(x10324))) -25|[]-> c(a(b(x10324)))
       a(c(x)) <-24|[]- c(b(x)) -29|[]-> c(c(x))
       c(a(c(x10326))) <-24|0[]- c(c(b(x10326))) -30|[]-> b(b(b(x10326)))
       c(a(c(x10327))) <-24|0[]- c(c(b(x10327))) -32|[]-> a(a(b(x10327)))
       a(c(x)) <-24|[]- c(b(x)) -36|[]-> b(a(x))
       a(a(c(x10329))) <-24|0[]- a(c(b(x10329))) -37|[]-> b(a(b(x10329)))
       b(a(c(x10330))) <-24|0[]- b(c(b(x10330))) -39|[]-> c(a(b(x10330)))
       a(c(x)) <-24|[]- c(b(x)) -40|[]-> c(a(x))
       a(a(c(x10332))) <-24|0[]- a(c(b(x10332))) -41|[]-> a(a(b(x10332)))
       a(c(x)) <-24|[]- c(b(x)) -48|[]-> b(b(x))
       a(c(x)) <-24|[]- c(b(x)) -49|[]-> a(a(x))
       c(a(c(x10335))) <-24|0[]- c(c(b(x10335))) -50|[]-> c(b(b(x10335)))
       c(a(c(x10336))) <-24|0[]- c(c(b(x10336))) -52|[]-> b(a(b(x10336)))
       c(a(c(x10337))) <-24|0[]- c(c(b(x10337))) -53|[]-> b(c(b(x10337)))
       a(c(a(x10338))) <-25|0[]- a(a(c(x10338))) -4|[]-> c(a(c(x10338)))
       c(a(x)) <-25|[]- a(c(x)) -7|[]-> c(b(x))
       c(a(x)) <-25|[]- a(c(x)) -8|[]-> c(c(x))
       c(c(a(x10341))) <-25|0[]- c(a(c(x10341))) -9|[]-> a(c(c(x10341)))
       c(c(a(x10342))) <-25|0[]- c(a(c(x10342))) -10|[]-> c(c(c(x10342)))
       c(c(a(x10343))) <-25|0[]- c(a(c(x10343))) -11|[]-> b(b(c(x10343)))
       a(c(a(x10344))) <-25|0[]- a(a(c(x10344))) -12|[]-> b(b(c(x10344)))
       c(a(x)) <-25|[]- a(c(x)) -19|[]-> b(c(x))
       a(c(a(x10346))) <-25|0[]- a(a(c(x10346))) -21|[]-> b(a(c(x10346)))
       a(c(a(x10347))) <-25|0[]- a(a(c(x10347))) -22|[]-> b(c(c(x10347)))
       c(c(a(x10348))) <-25|0[]- c(a(c(x10348))) -26|[]-> a(a(c(x10348)))
       a(c(a(x10349))) <-25|0[]- a(a(c(x10349))) -27|[]-> c(b(c(x10349)))
       c(a(x)) <-25|[]- a(c(x)) -37|[]-> b(a(x))
       a(c(a(x10351))) <-25|0[]- a(a(c(x10351))) -38|[]-> a(c(c(x10351)))
       c(a(x)) <-25|[]- a(c(x)) -41|[]-> a(a(x))
       c(c(a(x10353))) <-25|0[]- c(a(c(x10353))) -42|[]-> b(a(c(x10353)))
       c(c(a(x10354))) <-25|0[]- c(a(c(x10354))) -43|[]-> b(c(c(x10354)))
       c(c(a(x10355))) <-25|0[]- c(a(c(x10355))) -44|[]-> c(b(c(x10355)))
       a(c(a(x10356))) <-25|0[]- a(a(c(x10356))) -45|[]-> c(c(c(x10356)))
       b(a(a(x10357))) <-26|0[]- b(c(a(x10357))) -5|[]-> a(a(a(x10357)))
       b(a(a(x10358))) <-26|0[]- b(c(a(x10358))) -6|[]-> c(b(a(x10358)))
       a(a(a(x10359))) <-26|0[]- a(c(a(x10359))) -7|[]-> c(b(a(x10359)))
       a(a(a(x10360))) <-26|0[]- a(c(a(x10360))) -8|[]-> c(c(a(x10360)))
       a(a(x)) <-26|[]- c(a(x)) -9|[]-> a(c(x))
       a(a(x)) <-26|[]- c(a(x)) -10|[]-> c(c(x))
       a(a(x)) <-26|[]- c(a(x)) -11|[]-> b(b(x))
       c(a(a(x10364))) <-26|0[]- c(c(a(x10364))) -15|[]-> a(c(a(x10364)))
       c(a(a(x10365))) <-26|0[]- c(c(a(x10365))) -16|[]-> c(a(a(x10365)))
       a(a(a(x10366))) <-26|0[]- a(c(a(x10366))) -19|[]-> b(c(a(x10366)))
       b(a(a(x10367))) <-26|0[]- b(c(a(x10367))) -20|[]-> b(a(a(x10367)))
       b(a(a(x10368))) <-26|0[]- b(c(a(x10368))) -23|[]-> a(c(a(x10368)))
       a(a(a(x10369))) <-26|0[]- a(c(a(x10369))) -25|[]-> c(a(a(x10369)))
       c(a(a(x10370))) <-26|0[]- c(c(a(x10370))) -30|[]-> b(b(a(x10370)))
       c(a(a(x10371))) <-26|0[]- c(c(a(x10371))) -32|[]-> a(a(a(x10371)))
       a(a(a(x10372))) <-26|0[]- a(c(a(x10372))) -37|[]-> b(a(a(x10372)))
       b(a(a(x10373))) <-26|0[]- b(c(a(x10373))) -39|[]-> c(a(a(x10373)))
       a(a(a(x10374))) <-26|0[]- a(c(a(x10374))) -41|[]-> a(a(a(x10374)))
       a(a(x)) <-26|[]- c(a(x)) -42|[]-> b(a(x))
       a(a(x)) <-26|[]- c(a(x)) -43|[]-> b(c(x))
       a(a(x)) <-26|[]- c(a(x)) -44|[]-> c(b(x))
       c(a(a(x10378))) <-26|0[]- c(c(a(x10378))) -50|[]-> c(b(a(x10378)))
       c(a(a(x10379))) <-26|0[]- c(c(a(x10379))) -52|[]-> b(a(a(x10379)))
       c(a(a(x10380))) <-26|0[]- c(c(a(x10380))) -53|[]-> b(c(a(x10380)))
       c(b(x)) <-27|[]- a(a(x)) -4|[]-> c(a(x))
       a(c(b(x10382))) <-27|0[]- a(a(a(x10382))) -4|[]-> c(a(a(x10382)))
       c(c(b(x10383))) <-27|0[]- c(a(a(x10383))) -9|[]-> a(c(a(x10383)))
       c(c(b(x10384))) <-27|0[]- c(a(a(x10384))) -10|[]-> c(c(a(x10384)))
       c(c(b(x10385))) <-27|0[]- c(a(a(x10385))) -11|[]-> b(b(a(x10385)))
       c(b(x)) <-27|[]- a(a(x)) -12|[]-> b(b(x))
       a(c(b(x10387))) <-27|0[]- a(a(a(x10387))) -12|[]-> b(b(a(x10387)))
       c(b(x)) <-27|[]- a(a(x)) -21|[]-> b(a(x))
       a(c(b(x10389))) <-27|0[]- a(a(a(x10389))) -21|[]-> b(a(a(x10389)))
       c(b(x)) <-27|[]- a(a(x)) -22|[]-> b(c(x))
       a(c(b(x10391))) <-27|0[]- a(a(a(x10391))) -22|[]-> b(c(a(x10391)))
       c(c(b(x10392))) <-27|0[]- c(a(a(x10392))) -26|[]-> a(a(a(x10392)))
       a(c(b(x10393))) <-27|0[]- a(a(a(x10393))) -27|[]-> c(b(a(x10393)))
       c(b(x)) <-27|[]- a(a(x)) -38|[]-> a(c(x))
       a(c(b(x10395))) <-27|0[]- a(a(a(x10395))) -38|[]-> a(c(a(x10395)))
       c(c(b(x10396))) <-27|0[]- c(a(a(x10396))) -42|[]-> b(a(a(x10396)))
       c(c(b(x10397))) <-27|0[]- c(a(a(x10397))) -43|[]-> b(c(a(x10397)))
       c(c(b(x10398))) <-27|0[]- c(a(a(x10398))) -44|[]-> c(b(a(x10398)))
       c(b(x)) <-27|[]- a(a(x)) -45|[]-> c(c(x))
       a(c(b(x10400))) <-27|0[]- a(a(a(x10400))) -45|[]-> c(c(a(x10400)))
       a(c(b(x10401))) <-28|0[]- a(b(b(x10401))) -0|[]-> a(c(b(x10401)))
       a(c(b(x10402))) <-28|0[]- a(b(b(x10402))) -1|[]-> c(c(b(x10402)))
       a(c(b(x10403))) <-28|0[]- a(b(b(x10403))) -2|[]-> c(a(b(x10403)))
       a(c(b(x10404))) <-28|0[]- a(b(b(x10404))) -3|[]-> b(b(b(x10404)))
       c(b(x)) <-28|[]- b(b(x)) -13|[]-> c(a(x))
       b(c(b(x10406))) <-28|0[]- b(b(b(x10406))) -13|[]-> c(a(b(x10406)))
       c(b(x)) <-28|[]- b(b(x)) -14|[]-> b(a(x))
       b(c(b(x10408))) <-28|0[]- b(b(b(x10408))) -14|[]-> b(a(b(x10408)))
       a(c(b(x10409))) <-28|0[]- a(b(b(x10409))) -17|[]-> a(a(b(x10409)))
       c(c(b(x10410))) <-28|0[]- c(b(b(x10410))) -18|[]-> b(c(b(x10410)))
       c(c(b(x10411))) <-28|0[]- c(b(b(x10411))) -24|[]-> a(c(b(x10411)))
       b(c(b(x10412))) <-28|0[]- b(b(b(x10412))) -28|[]-> c(b(b(x10412)))
       c(c(b(x10413))) <-28|0[]- c(b(b(x10413))) -29|[]-> c(c(b(x10413)))
       c(b(x)) <-28|[]- b(b(x)) -31|[]-> c(c(x))
       b(c(b(x10415))) <-28|0[]- b(b(b(x10415))) -31|[]-> c(c(b(x10415)))
       a(c(b(x10416))) <-28|0[]- a(b(b(x10416))) -33|[]-> b(a(b(x10416)))
       a(c(b(x10417))) <-28|0[]- a(b(b(x10417))) -34|[]-> b(c(b(x10417)))
       a(c(b(x10418))) <-28|0[]- a(b(b(x10418))) -35|[]-> c(b(b(x10418)))
       c(c(b(x10419))) <-28|0[]- c(b(b(x10419))) -36|[]-> b(a(b(x10419)))
       c(c(b(x10420))) <-28|0[]- c(b(b(x10420))) -40|[]-> c(a(b(x10420)))
       c(b(x)) <-28|[]- b(b(x)) -46|[]-> b(c(x))
       b(c(b(x10422))) <-28|0[]- b(b(b(x10422))) -46|[]-> b(c(b(x10422)))
       c(b(x)) <-28|[]- b(b(x)) -47|[]-> a(c(x))
       b(c(b(x10424))) <-28|0[]- b(b(b(x10424))) -47|[]-> a(c(b(x10424)))
       c(c(b(x10425))) <-28|0[]- c(b(b(x10425))) -48|[]-> b(b(b(x10425)))
       c(c(b(x10426))) <-28|0[]- c(b(b(x10426))) -49|[]-> a(a(b(x10426)))
       c(b(x)) <-28|[]- b(b(x)) -51|[]-> a(a(x))
       b(c(b(x10428))) <-28|0[]- b(b(b(x10428))) -51|[]-> a(a(b(x10428)))
       b(c(c(x10429))) <-29|0[]- b(c(b(x10429))) -5|[]-> a(a(b(x10429)))
       b(c(c(x10430))) <-29|0[]- b(c(b(x10430))) -6|[]-> c(b(b(x10430)))
       a(c(c(x10431))) <-29|0[]- a(c(b(x10431))) -7|[]-> c(b(b(x10431)))
       a(c(c(x10432))) <-29|0[]- a(c(b(x10432))) -8|[]-> c(c(b(x10432)))
       c(c(c(x10433))) <-29|0[]- c(c(b(x10433))) -15|[]-> a(c(b(x10433)))
       c(c(c(x10434))) <-29|0[]- c(c(b(x10434))) -16|[]-> c(a(b(x10434)))
       c(c(x)) <-29|[]- c(b(x)) -18|[]-> b(c(x))
       a(c(c(x10436))) <-29|0[]- a(c(b(x10436))) -19|[]-> b(c(b(x10436)))
       b(c(c(x10437))) <-29|0[]- b(c(b(x10437))) -20|[]-> b(a(b(x10437)))
       b(c(c(x10438))) <-29|0[]- b(c(b(x10438))) -23|[]-> a(c(b(x10438)))
       c(c(x)) <-29|[]- c(b(x)) -24|[]-> a(c(x))
       a(c(c(x10440))) <-29|0[]- a(c(b(x10440))) -25|[]-> c(a(b(x10440)))
       c(c(c(x10441))) <-29|0[]- c(c(b(x10441))) -30|[]-> b(b(b(x10441)))
       c(c(c(x10442))) <-29|0[]- c(c(b(x10442))) -32|[]-> a(a(b(x10442)))
       c(c(x)) <-29|[]- c(b(x)) -36|[]-> b(a(x))
       a(c(c(x10444))) <-29|0[]- a(c(b(x10444))) -37|[]-> b(a(b(x10444)))
       b(c(c(x10445))) <-29|0[]- b(c(b(x10445))) -39|[]-> c(a(b(x10445)))
       c(c(x)) <-29|[]- c(b(x)) -40|[]-> c(a(x))
       a(c(c(x10447))) <-29|0[]- a(c(b(x10447))) -41|[]-> a(a(b(x10447)))
       c(c(x)) <-29|[]- c(b(x)) -48|[]-> b(b(x))
       c(c(x)) <-29|[]- c(b(x)) -49|[]-> a(a(x))
       c(c(c(x10450))) <-29|0[]- c(c(b(x10450))) -50|[]-> c(b(b(x10450)))
       c(c(c(x10451))) <-29|0[]- c(c(b(x10451))) -52|[]-> b(a(b(x10451)))
       c(c(c(x10452))) <-29|0[]- c(c(b(x10452))) -53|[]-> b(c(b(x10452)))
       b(b(b(x10453))) <-30|0[]- b(c(c(x10453))) -5|[]-> a(a(c(x10453)))
       b(b(b(x10454))) <-30|0[]- b(c(c(x10454))) -6|[]-> c(b(c(x10454)))
       a(b(b(x10455))) <-30|0[]- a(c(c(x10455))) -7|[]-> c(b(c(x10455)))
       a(b(b(x10456))) <-30|0[]- a(c(c(x10456))) -8|[]-> c(c(c(x10456)))
       b(b(x)) <-30|[]- c(c(x)) -15|[]-> a(c(x))
       c(b(b(x10458))) <-30|0[]- c(c(c(x10458))) -15|[]-> a(c(c(x10458)))
       b(b(x)) <-30|[]- c(c(x)) -16|[]-> c(a(x))
       c(b(b(x10460))) <-30|0[]- c(c(c(x10460))) -16|[]-> c(a(c(x10460)))
       a(b(b(x10461))) <-30|0[]- a(c(c(x10461))) -19|[]-> b(c(c(x10461)))
       b(b(b(x10462))) <-30|0[]- b(c(c(x10462))) -20|[]-> b(a(c(x10462)))
       b(b(b(x10463))) <-30|0[]- b(c(c(x10463))) -23|[]-> a(c(c(x10463)))
       a(b(b(x10464))) <-30|0[]- a(c(c(x10464))) -25|[]-> c(a(c(x10464)))
       c(b(b(x10465))) <-30|0[]- c(c(c(x10465))) -30|[]-> b(b(c(x10465)))
       b(b(x)) <-30|[]- c(c(x)) -32|[]-> a(a(x))
       c(b(b(x10467))) <-30|0[]- c(c(c(x10467))) -32|[]-> a(a(c(x10467)))
       a(b(b(x10468))) <-30|0[]- a(c(c(x10468))) -37|[]-> b(a(c(x10468)))
       b(b(b(x10469))) <-30|0[]- b(c(c(x10469))) -39|[]-> c(a(c(x10469)))
       a(b(b(x10470))) <-30|0[]- a(c(c(x10470))) -41|[]-> a(a(c(x10470)))
       b(b(x)) <-30|[]- c(c(x)) -50|[]-> c(b(x))
       c(b(b(x10472))) <-30|0[]- c(c(c(x10472))) -50|[]-> c(b(c(x10472)))
       b(b(x)) <-30|[]- c(c(x)) -52|[]-> b(a(x))
       c(b(b(x10474))) <-30|0[]- c(c(c(x10474))) -52|[]-> b(a(c(x10474)))
       b(b(x)) <-30|[]- c(c(x)) -53|[]-> b(c(x))
       c(b(b(x10476))) <-30|0[]- c(c(c(x10476))) -53|[]-> b(c(c(x10476)))
       a(c(c(x10477))) <-31|0[]- a(b(b(x10477))) -0|[]-> a(c(b(x10477)))
       a(c(c(x10478))) <-31|0[]- a(b(b(x10478))) -1|[]-> c(c(b(x10478)))
       a(c(c(x10479))) <-31|0[]- a(b(b(x10479))) -2|[]-> c(a(b(x10479)))
       a(c(c(x10480))) <-31|0[]- a(b(b(x10480))) -3|[]-> b(b(b(x10480)))
       c(c(x)) <-31|[]- b(b(x)) -13|[]-> c(a(x))
       b(c(c(x10482))) <-31|0[]- b(b(b(x10482))) -13|[]-> c(a(b(x10482)))
       c(c(x)) <-31|[]- b(b(x)) -14|[]-> b(a(x))
       b(c(c(x10484))) <-31|0[]- b(b(b(x10484))) -14|[]-> b(a(b(x10484)))
       a(c(c(x10485))) <-31|0[]- a(b(b(x10485))) -17|[]-> a(a(b(x10485)))
       c(c(c(x10486))) <-31|0[]- c(b(b(x10486))) -18|[]-> b(c(b(x10486)))
       c(c(c(x10487))) <-31|0[]- c(b(b(x10487))) -24|[]-> a(c(b(x10487)))
       c(c(x)) <-31|[]- b(b(x)) -28|[]-> c(b(x))
       b(c(c(x10489))) <-31|0[]- b(b(b(x10489))) -28|[]-> c(b(b(x10489)))
       c(c(c(x10490))) <-31|0[]- c(b(b(x10490))) -29|[]-> c(c(b(x10490)))
       b(c(c(x10491))) <-31|0[]- b(b(b(x10491))) -31|[]-> c(c(b(x10491)))
       a(c(c(x10492))) <-31|0[]- a(b(b(x10492))) -33|[]-> b(a(b(x10492)))
       a(c(c(x10493))) <-31|0[]- a(b(b(x10493))) -34|[]-> b(c(b(x10493)))
       a(c(c(x10494))) <-31|0[]- a(b(b(x10494))) -35|[]-> c(b(b(x10494)))
       c(c(c(x10495))) <-31|0[]- c(b(b(x10495))) -36|[]-> b(a(b(x10495)))
       c(c(c(x10496))) <-31|0[]- c(b(b(x10496))) -40|[]-> c(a(b(x10496)))
       c(c(x)) <-31|[]- b(b(x)) -46|[]-> b(c(x))
       b(c(c(x10498))) <-31|0[]- b(b(b(x10498))) -46|[]-> b(c(b(x10498)))
       c(c(x)) <-31|[]- b(b(x)) -47|[]-> a(c(x))
       b(c(c(x10500))) <-31|0[]- b(b(b(x10500))) -47|[]-> a(c(b(x10500)))
       c(c(c(x10501))) <-31|0[]- c(b(b(x10501))) -48|[]-> b(b(b(x10501)))
       c(c(c(x10502))) <-31|0[]- c(b(b(x10502))) -49|[]-> a(a(b(x10502)))
       c(c(x)) <-31|[]- b(b(x)) -51|[]-> a(a(x))
       b(c(c(x10504))) <-31|0[]- b(b(b(x10504))) -51|[]-> a(a(b(x10504)))
       b(a(a(x10505))) <-32|0[]- b(c(c(x10505))) -5|[]-> a(a(c(x10505)))
       b(a(a(x10506))) <-32|0[]- b(c(c(x10506))) -6|[]-> c(b(c(x10506)))
       a(a(a(x10507))) <-32|0[]- a(c(c(x10507))) -7|[]-> c(b(c(x10507)))
       a(a(a(x10508))) <-32|0[]- a(c(c(x10508))) -8|[]-> c(c(c(x10508)))
       a(a(x)) <-32|[]- c(c(x)) -15|[]-> a(c(x))
       c(a(a(x10510))) <-32|0[]- c(c(c(x10510))) -15|[]-> a(c(c(x10510)))
       a(a(x)) <-32|[]- c(c(x)) -16|[]-> c(a(x))
       c(a(a(x10512))) <-32|0[]- c(c(c(x10512))) -16|[]-> c(a(c(x10512)))
       a(a(a(x10513))) <-32|0[]- a(c(c(x10513))) -19|[]-> b(c(c(x10513)))
       b(a(a(x10514))) <-32|0[]- b(c(c(x10514))) -20|[]-> b(a(c(x10514)))
       b(a(a(x10515))) <-32|0[]- b(c(c(x10515))) -23|[]-> a(c(c(x10515)))
       a(a(a(x10516))) <-32|0[]- a(c(c(x10516))) -25|[]-> c(a(c(x10516)))
       a(a(x)) <-32|[]- c(c(x)) -30|[]-> b(b(x))
       c(a(a(x10518))) <-32|0[]- c(c(c(x10518))) -30|[]-> b(b(c(x10518)))
       c(a(a(x10519))) <-32|0[]- c(c(c(x10519))) -32|[]-> a(a(c(x10519)))
       a(a(a(x10520))) <-32|0[]- a(c(c(x10520))) -37|[]-> b(a(c(x10520)))
       b(a(a(x10521))) <-32|0[]- b(c(c(x10521))) -39|[]-> c(a(c(x10521)))
       a(a(a(x10522))) <-32|0[]- a(c(c(x10522))) -41|[]-> a(a(c(x10522)))
       a(a(x)) <-32|[]- c(c(x)) -50|[]-> c(b(x))
       c(a(a(x10524))) <-32|0[]- c(c(c(x10524))) -50|[]-> c(b(c(x10524)))
       a(a(x)) <-32|[]- c(c(x)) -52|[]-> b(a(x))
       c(a(a(x10526))) <-32|0[]- c(c(c(x10526))) -52|[]-> b(a(c(x10526)))
       a(a(x)) <-32|[]- c(c(x)) -53|[]-> b(c(x))
       c(a(a(x10528))) <-32|0[]- c(c(c(x10528))) -53|[]-> b(c(c(x10528)))
       b(a(x)) <-33|[]- a(b(x)) -0|[]-> a(c(x))
       b(a(x)) <-33|[]- a(b(x)) -1|[]-> c(c(x))
       b(a(x)) <-33|[]- a(b(x)) -2|[]-> c(a(x))
       b(a(x)) <-33|[]- a(b(x)) -3|[]-> b(b(x))
       a(b(a(x10533))) <-33|0[]- a(a(b(x10533))) -4|[]-> c(a(b(x10533)))
       c(b(a(x10534))) <-33|0[]- c(a(b(x10534))) -9|[]-> a(c(b(x10534)))
       c(b(a(x10535))) <-33|0[]- c(a(b(x10535))) -10|[]-> c(c(b(x10535)))
       c(b(a(x10536))) <-33|0[]- c(a(b(x10536))) -11|[]-> b(b(b(x10536)))
       a(b(a(x10537))) <-33|0[]- a(a(b(x10537))) -12|[]-> b(b(b(x10537)))
       b(a(x)) <-33|[]- a(b(x)) -17|[]-> a(a(x))
       a(b(a(x10539))) <-33|0[]- a(a(b(x10539))) -21|[]-> b(a(b(x10539)))
       a(b(a(x10540))) <-33|0[]- a(a(b(x10540))) -22|[]-> b(c(b(x10540)))
       c(b(a(x10541))) <-33|0[]- c(a(b(x10541))) -26|[]-> a(a(b(x10541)))
       a(b(a(x10542))) <-33|0[]- a(a(b(x10542))) -27|[]-> c(b(b(x10542)))
       b(a(x)) <-33|[]- a(b(x)) -34|[]-> b(c(x))
       b(a(x)) <-33|[]- a(b(x)) -35|[]-> c(b(x))
       a(b(a(x10545))) <-33|0[]- a(a(b(x10545))) -38|[]-> a(c(b(x10545)))
       c(b(a(x10546))) <-33|0[]- c(a(b(x10546))) -42|[]-> b(a(b(x10546)))
       c(b(a(x10547))) <-33|0[]- c(a(b(x10547))) -43|[]-> b(c(b(x10547)))
       c(b(a(x10548))) <-33|0[]- c(a(b(x10548))) -44|[]-> c(b(b(x10548)))
       a(b(a(x10549))) <-33|0[]- a(a(b(x10549))) -45|[]-> c(c(b(x10549)))
       b(c(x)) <-34|[]- a(b(x)) -0|[]-> a(c(x))
       b(c(x)) <-34|[]- a(b(x)) -1|[]-> c(c(x))
       b(c(x)) <-34|[]- a(b(x)) -2|[]-> c(a(x))
       b(c(x)) <-34|[]- a(b(x)) -3|[]-> b(b(x))
       a(b(c(x10554))) <-34|0[]- a(a(b(x10554))) -4|[]-> c(a(b(x10554)))
       c(b(c(x10555))) <-34|0[]- c(a(b(x10555))) -9|[]-> a(c(b(x10555)))
       c(b(c(x10556))) <-34|0[]- c(a(b(x10556))) -10|[]-> c(c(b(x10556)))
       c(b(c(x10557))) <-34|0[]- c(a(b(x10557))) -11|[]-> b(b(b(x10557)))
       a(b(c(x10558))) <-34|0[]- a(a(b(x10558))) -12|[]-> b(b(b(x10558)))
       b(c(x)) <-34|[]- a(b(x)) -17|[]-> a(a(x))
       a(b(c(x10560))) <-34|0[]- a(a(b(x10560))) -21|[]-> b(a(b(x10560)))
       a(b(c(x10561))) <-34|0[]- a(a(b(x10561))) -22|[]-> b(c(b(x10561)))
       c(b(c(x10562))) <-34|0[]- c(a(b(x10562))) -26|[]-> a(a(b(x10562)))
       a(b(c(x10563))) <-34|0[]- a(a(b(x10563))) -27|[]-> c(b(b(x10563)))
       b(c(x)) <-34|[]- a(b(x)) -33|[]-> b(a(x))
       b(c(x)) <-34|[]- a(b(x)) -35|[]-> c(b(x))
       a(b(c(x10566))) <-34|0[]- a(a(b(x10566))) -38|[]-> a(c(b(x10566)))
       c(b(c(x10567))) <-34|0[]- c(a(b(x10567))) -42|[]-> b(a(b(x10567)))
       c(b(c(x10568))) <-34|0[]- c(a(b(x10568))) -43|[]-> b(c(b(x10568)))
       c(b(c(x10569))) <-34|0[]- c(a(b(x10569))) -44|[]-> c(b(b(x10569)))
       a(b(c(x10570))) <-34|0[]- a(a(b(x10570))) -45|[]-> c(c(b(x10570)))
       c(b(x)) <-35|[]- a(b(x)) -0|[]-> a(c(x))
       c(b(x)) <-35|[]- a(b(x)) -1|[]-> c(c(x))
       c(b(x)) <-35|[]- a(b(x)) -2|[]-> c(a(x))
       c(b(x)) <-35|[]- a(b(x)) -3|[]-> b(b(x))
       a(c(b(x10575))) <-35|0[]- a(a(b(x10575))) -4|[]-> c(a(b(x10575)))
       c(c(b(x10576))) <-35|0[]- c(a(b(x10576))) -9|[]-> a(c(b(x10576)))
       c(c(b(x10577))) <-35|0[]- c(a(b(x10577))) -10|[]-> c(c(b(x10577)))
       c(c(b(x10578))) <-35|0[]- c(a(b(x10578))) -11|[]-> b(b(b(x10578)))
       a(c(b(x10579))) <-35|0[]- a(a(b(x10579))) -12|[]-> b(b(b(x10579)))
       c(b(x)) <-35|[]- a(b(x)) -17|[]-> a(a(x))
       a(c(b(x10581))) <-35|0[]- a(a(b(x10581))) -21|[]-> b(a(b(x10581)))
       a(c(b(x10582))) <-35|0[]- a(a(b(x10582))) -22|[]-> b(c(b(x10582)))
       c(c(b(x10583))) <-35|0[]- c(a(b(x10583))) -26|[]-> a(a(b(x10583)))
       a(c(b(x10584))) <-35|0[]- a(a(b(x10584))) -27|[]-> c(b(b(x10584)))
       c(b(x)) <-35|[]- a(b(x)) -33|[]-> b(a(x))
       c(b(x)) <-35|[]- a(b(x)) -34|[]-> b(c(x))
       a(c(b(x10587))) <-35|0[]- a(a(b(x10587))) -38|[]-> a(c(b(x10587)))
       c(c(b(x10588))) <-35|0[]- c(a(b(x10588))) -42|[]-> b(a(b(x10588)))
       c(c(b(x10589))) <-35|0[]- c(a(b(x10589))) -43|[]-> b(c(b(x10589)))
       c(c(b(x10590))) <-35|0[]- c(a(b(x10590))) -44|[]-> c(b(b(x10590)))
       a(c(b(x10591))) <-35|0[]- a(a(b(x10591))) -45|[]-> c(c(b(x10591)))
       b(b(a(x10592))) <-36|0[]- b(c(b(x10592))) -5|[]-> a(a(b(x10592)))
       b(b(a(x10593))) <-36|0[]- b(c(b(x10593))) -6|[]-> c(b(b(x10593)))
       a(b(a(x10594))) <-36|0[]- a(c(b(x10594))) -7|[]-> c(b(b(x10594)))
       a(b(a(x10595))) <-36|0[]- a(c(b(x10595))) -8|[]-> c(c(b(x10595)))
       c(b(a(x10596))) <-36|0[]- c(c(b(x10596))) -15|[]-> a(c(b(x10596)))
       c(b(a(x10597))) <-36|0[]- c(c(b(x10597))) -16|[]-> c(a(b(x10597)))
       b(a(x)) <-36|[]- c(b(x)) -18|[]-> b(c(x))
       a(b(a(x10599))) <-36|0[]- a(c(b(x10599))) -19|[]-> b(c(b(x10599)))
       b(b(a(x10600))) <-36|0[]- b(c(b(x10600))) -20|[]-> b(a(b(x10600)))
       b(b(a(x10601))) <-36|0[]- b(c(b(x10601))) -23|[]-> a(c(b(x10601)))
       b(a(x)) <-36|[]- c(b(x)) -24|[]-> a(c(x))
       a(b(a(x10603))) <-36|0[]- a(c(b(x10603))) -25|[]-> c(a(b(x10603)))
       b(a(x)) <-36|[]- c(b(x)) -29|[]-> c(c(x))
       c(b(a(x10605))) <-36|0[]- c(c(b(x10605))) -30|[]-> b(b(b(x10605)))
       c(b(a(x10606))) <-36|0[]- c(c(b(x10606))) -32|[]-> a(a(b(x10606)))
       a(b(a(x10607))) <-36|0[]- a(c(b(x10607))) -37|[]-> b(a(b(x10607)))
       b(b(a(x10608))) <-36|0[]- b(c(b(x10608))) -39|[]-> c(a(b(x10608)))
       b(a(x)) <-36|[]- c(b(x)) -40|[]-> c(a(x))
       a(b(a(x10610))) <-36|0[]- a(c(b(x10610))) -41|[]-> a(a(b(x10610)))
       b(a(x)) <-36|[]- c(b(x)) -48|[]-> b(b(x))
       b(a(x)) <-36|[]- c(b(x)) -49|[]-> a(a(x))
       c(b(a(x10613))) <-36|0[]- c(c(b(x10613))) -50|[]-> c(b(b(x10613)))
       c(b(a(x10614))) <-36|0[]- c(c(b(x10614))) -52|[]-> b(a(b(x10614)))
       c(b(a(x10615))) <-36|0[]- c(c(b(x10615))) -53|[]-> b(c(b(x10615)))
       a(b(a(x10616))) <-37|0[]- a(a(c(x10616))) -4|[]-> c(a(c(x10616)))
       b(a(x)) <-37|[]- a(c(x)) -7|[]-> c(b(x))
       b(a(x)) <-37|[]- a(c(x)) -8|[]-> c(c(x))
       c(b(a(x10619))) <-37|0[]- c(a(c(x10619))) -9|[]-> a(c(c(x10619)))
       c(b(a(x10620))) <-37|0[]- c(a(c(x10620))) -10|[]-> c(c(c(x10620)))
       c(b(a(x10621))) <-37|0[]- c(a(c(x10621))) -11|[]-> b(b(c(x10621)))
       a(b(a(x10622))) <-37|0[]- a(a(c(x10622))) -12|[]-> b(b(c(x10622)))
       b(a(x)) <-37|[]- a(c(x)) -19|[]-> b(c(x))
       a(b(a(x10624))) <-37|0[]- a(a(c(x10624))) -21|[]-> b(a(c(x10624)))
       a(b(a(x10625))) <-37|0[]- a(a(c(x10625))) -22|[]-> b(c(c(x10625)))
       b(a(x)) <-37|[]- a(c(x)) -25|[]-> c(a(x))
       c(b(a(x10627))) <-37|0[]- c(a(c(x10627))) -26|[]-> a(a(c(x10627)))
       a(b(a(x10628))) <-37|0[]- a(a(c(x10628))) -27|[]-> c(b(c(x10628)))
       a(b(a(x10629))) <-37|0[]- a(a(c(x10629))) -38|[]-> a(c(c(x10629)))
       b(a(x)) <-37|[]- a(c(x)) -41|[]-> a(a(x))
       c(b(a(x10631))) <-37|0[]- c(a(c(x10631))) -42|[]-> b(a(c(x10631)))
       c(b(a(x10632))) <-37|0[]- c(a(c(x10632))) -43|[]-> b(c(c(x10632)))
       c(b(a(x10633))) <-37|0[]- c(a(c(x10633))) -44|[]-> c(b(c(x10633)))
       a(b(a(x10634))) <-37|0[]- a(a(c(x10634))) -45|[]-> c(c(c(x10634)))
       a(c(x)) <-38|[]- a(a(x)) -4|[]-> c(a(x))
       a(a(c(x10636))) <-38|0[]- a(a(a(x10636))) -4|[]-> c(a(a(x10636)))
       c(a(c(x10637))) <-38|0[]- c(a(a(x10637))) -9|[]-> a(c(a(x10637)))
       c(a(c(x10638))) <-38|0[]- c(a(a(x10638))) -10|[]-> c(c(a(x10638)))
       c(a(c(x10639))) <-38|0[]- c(a(a(x10639))) -11|[]-> b(b(a(x10639)))
       a(c(x)) <-38|[]- a(a(x)) -12|[]-> b(b(x))
       a(a(c(x10641))) <-38|0[]- a(a(a(x10641))) -12|[]-> b(b(a(x10641)))
       a(c(x)) <-38|[]- a(a(x)) -21|[]-> b(a(x))
       a(a(c(x10643))) <-38|0[]- a(a(a(x10643))) -21|[]-> b(a(a(x10643)))
       a(c(x)) <-38|[]- a(a(x)) -22|[]-> b(c(x))
       a(a(c(x10645))) <-38|0[]- a(a(a(x10645))) -22|[]-> b(c(a(x10645)))
       c(a(c(x10646))) <-38|0[]- c(a(a(x10646))) -26|[]-> a(a(a(x10646)))
       a(c(x)) <-38|[]- a(a(x)) -27|[]-> c(b(x))
       a(a(c(x10648))) <-38|0[]- a(a(a(x10648))) -27|[]-> c(b(a(x10648)))
       a(a(c(x10649))) <-38|0[]- a(a(a(x10649))) -38|[]-> a(c(a(x10649)))
       c(a(c(x10650))) <-38|0[]- c(a(a(x10650))) -42|[]-> b(a(a(x10650)))
       c(a(c(x10651))) <-38|0[]- c(a(a(x10651))) -43|[]-> b(c(a(x10651)))
       c(a(c(x10652))) <-38|0[]- c(a(a(x10652))) -44|[]-> c(b(a(x10652)))
       a(c(x)) <-38|[]- a(a(x)) -45|[]-> c(c(x))
       a(a(c(x10654))) <-38|0[]- a(a(a(x10654))) -45|[]-> c(c(a(x10654)))
       a(c(a(x10655))) <-39|0[]- a(b(c(x10655))) -0|[]-> a(c(c(x10655)))
       a(c(a(x10656))) <-39|0[]- a(b(c(x10656))) -1|[]-> c(c(c(x10656)))
       a(c(a(x10657))) <-39|0[]- a(b(c(x10657))) -2|[]-> c(a(c(x10657)))
       a(c(a(x10658))) <-39|0[]- a(b(c(x10658))) -3|[]-> b(b(c(x10658)))
       c(a(x)) <-39|[]- b(c(x)) -5|[]-> a(a(x))
       c(a(x)) <-39|[]- b(c(x)) -6|[]-> c(b(x))
       b(c(a(x10661))) <-39|0[]- b(b(c(x10661))) -13|[]-> c(a(c(x10661)))
       b(c(a(x10662))) <-39|0[]- b(b(c(x10662))) -14|[]-> b(a(c(x10662)))
       a(c(a(x10663))) <-39|0[]- a(b(c(x10663))) -17|[]-> a(a(c(x10663)))
       c(c(a(x10664))) <-39|0[]- c(b(c(x10664))) -18|[]-> b(c(c(x10664)))
       c(a(x)) <-39|[]- b(c(x)) -20|[]-> b(a(x))
       c(a(x)) <-39|[]- b(c(x)) -23|[]-> a(c(x))
       c(c(a(x10667))) <-39|0[]- c(b(c(x10667))) -24|[]-> a(c(c(x10667)))
       b(c(a(x10668))) <-39|0[]- b(b(c(x10668))) -28|[]-> c(b(c(x10668)))
       c(c(a(x10669))) <-39|0[]- c(b(c(x10669))) -29|[]-> c(c(c(x10669)))
       b(c(a(x10670))) <-39|0[]- b(b(c(x10670))) -31|[]-> c(c(c(x10670)))
       a(c(a(x10671))) <-39|0[]- a(b(c(x10671))) -33|[]-> b(a(c(x10671)))
       a(c(a(x10672))) <-39|0[]- a(b(c(x10672))) -34|[]-> b(c(c(x10672)))
       a(c(a(x10673))) <-39|0[]- a(b(c(x10673))) -35|[]-> c(b(c(x10673)))
       c(c(a(x10674))) <-39|0[]- c(b(c(x10674))) -36|[]-> b(a(c(x10674)))
       c(c(a(x10675))) <-39|0[]- c(b(c(x10675))) -40|[]-> c(a(c(x10675)))
       b(c(a(x10676))) <-39|0[]- b(b(c(x10676))) -46|[]-> b(c(c(x10676)))
       b(c(a(x10677))) <-39|0[]- b(b(c(x10677))) -47|[]-> a(c(c(x10677)))
       c(c(a(x10678))) <-39|0[]- c(b(c(x10678))) -48|[]-> b(b(c(x10678)))
       c(c(a(x10679))) <-39|0[]- c(b(c(x10679))) -49|[]-> a(a(c(x10679)))
       b(c(a(x10680))) <-39|0[]- b(b(c(x10680))) -51|[]-> a(a(c(x10680)))
       b(c(a(x10681))) <-40|0[]- b(c(b(x10681))) -5|[]-> a(a(b(x10681)))
       b(c(a(x10682))) <-40|0[]- b(c(b(x10682))) -6|[]-> c(b(b(x10682)))
       a(c(a(x10683))) <-40|0[]- a(c(b(x10683))) -7|[]-> c(b(b(x10683)))
       a(c(a(x10684))) <-40|0[]- a(c(b(x10684))) -8|[]-> c(c(b(x10684)))
       c(c(a(x10685))) <-40|0[]- c(c(b(x10685))) -15|[]-> a(c(b(x10685)))
       c(c(a(x10686))) <-40|0[]- c(c(b(x10686))) -16|[]-> c(a(b(x10686)))
       c(a(x)) <-40|[]- c(b(x)) -18|[]-> b(c(x))
       a(c(a(x10688))) <-40|0[]- a(c(b(x10688))) -19|[]-> b(c(b(x10688)))
       b(c(a(x10689))) <-40|0[]- b(c(b(x10689))) -20|[]-> b(a(b(x10689)))
       b(c(a(x10690))) <-40|0[]- b(c(b(x10690))) -23|[]-> a(c(b(x10690)))
       c(a(x)) <-40|[]- c(b(x)) -24|[]-> a(c(x))
       a(c(a(x10692))) <-40|0[]- a(c(b(x10692))) -25|[]-> c(a(b(x10692)))
       c(a(x)) <-40|[]- c(b(x)) -29|[]-> c(c(x))
       c(c(a(x10694))) <-40|0[]- c(c(b(x10694))) -30|[]-> b(b(b(x10694)))
       c(c(a(x10695))) <-40|0[]- c(c(b(x10695))) -32|[]-> a(a(b(x10695)))
       c(a(x)) <-40|[]- c(b(x)) -36|[]-> b(a(x))
       a(c(a(x10697))) <-40|0[]- a(c(b(x10697))) -37|[]-> b(a(b(x10697)))
       b(c(a(x10698))) <-40|0[]- b(c(b(x10698))) -39|[]-> c(a(b(x10698)))
       a(c(a(x10699))) <-40|0[]- a(c(b(x10699))) -41|[]-> a(a(b(x10699)))
       c(a(x)) <-40|[]- c(b(x)) -48|[]-> b(b(x))
       c(a(x)) <-40|[]- c(b(x)) -49|[]-> a(a(x))
       c(c(a(x10702))) <-40|0[]- c(c(b(x10702))) -50|[]-> c(b(b(x10702)))
       c(c(a(x10703))) <-40|0[]- c(c(b(x10703))) -52|[]-> b(a(b(x10703)))
       c(c(a(x10704))) <-40|0[]- c(c(b(x10704))) -53|[]-> b(c(b(x10704)))
       a(a(a(x10705))) <-41|0[]- a(a(c(x10705))) -4|[]-> c(a(c(x10705)))
       a(a(x)) <-41|[]- a(c(x)) -7|[]-> c(b(x))
       a(a(x)) <-41|[]- a(c(x)) -8|[]-> c(c(x))
       c(a(a(x10708))) <-41|0[]- c(a(c(x10708))) -9|[]-> a(c(c(x10708)))
       c(a(a(x10709))) <-41|0[]- c(a(c(x10709))) -10|[]-> c(c(c(x10709)))
       c(a(a(x10710))) <-41|0[]- c(a(c(x10710))) -11|[]-> b(b(c(x10710)))
       a(a(a(x10711))) <-41|0[]- a(a(c(x10711))) -12|[]-> b(b(c(x10711)))
       a(a(x)) <-41|[]- a(c(x)) -19|[]-> b(c(x))
       a(a(a(x10713))) <-41|0[]- a(a(c(x10713))) -21|[]-> b(a(c(x10713)))
       a(a(a(x10714))) <-41|0[]- a(a(c(x10714))) -22|[]-> b(c(c(x10714)))
       a(a(x)) <-41|[]- a(c(x)) -25|[]-> c(a(x))
       c(a(a(x10716))) <-41|0[]- c(a(c(x10716))) -26|[]-> a(a(c(x10716)))
       a(a(a(x10717))) <-41|0[]- a(a(c(x10717))) -27|[]-> c(b(c(x10717)))
       a(a(x)) <-41|[]- a(c(x)) -37|[]-> b(a(x))
       a(a(a(x10719))) <-41|0[]- a(a(c(x10719))) -38|[]-> a(c(c(x10719)))
       c(a(a(x10720))) <-41|0[]- c(a(c(x10720))) -42|[]-> b(a(c(x10720)))
       c(a(a(x10721))) <-41|0[]- c(a(c(x10721))) -43|[]-> b(c(c(x10721)))
       c(a(a(x10722))) <-41|0[]- c(a(c(x10722))) -44|[]-> c(b(c(x10722)))
       a(a(a(x10723))) <-41|0[]- a(a(c(x10723))) -45|[]-> c(c(c(x10723)))
       b(b(a(x10724))) <-42|0[]- b(c(a(x10724))) -5|[]-> a(a(a(x10724)))
       b(b(a(x10725))) <-42|0[]- b(c(a(x10725))) -6|[]-> c(b(a(x10725)))
       a(b(a(x10726))) <-42|0[]- a(c(a(x10726))) -7|[]-> c(b(a(x10726)))
       a(b(a(x10727))) <-42|0[]- a(c(a(x10727))) -8|[]-> c(c(a(x10727)))
       b(a(x)) <-42|[]- c(a(x)) -9|[]-> a(c(x))
       b(a(x)) <-42|[]- c(a(x)) -10|[]-> c(c(x))
       b(a(x)) <-42|[]- c(a(x)) -11|[]-> b(b(x))
       c(b(a(x10731))) <-42|0[]- c(c(a(x10731))) -15|[]-> a(c(a(x10731)))
       c(b(a(x10732))) <-42|0[]- c(c(a(x10732))) -16|[]-> c(a(a(x10732)))
       a(b(a(x10733))) <-42|0[]- a(c(a(x10733))) -19|[]-> b(c(a(x10733)))
       b(b(a(x10734))) <-42|0[]- b(c(a(x10734))) -20|[]-> b(a(a(x10734)))
       b(b(a(x10735))) <-42|0[]- b(c(a(x10735))) -23|[]-> a(c(a(x10735)))
       a(b(a(x10736))) <-42|0[]- a(c(a(x10736))) -25|[]-> c(a(a(x10736)))
       b(a(x)) <-42|[]- c(a(x)) -26|[]-> a(a(x))
       c(b(a(x10738))) <-42|0[]- c(c(a(x10738))) -30|[]-> b(b(a(x10738)))
       c(b(a(x10739))) <-42|0[]- c(c(a(x10739))) -32|[]-> a(a(a(x10739)))
       a(b(a(x10740))) <-42|0[]- a(c(a(x10740))) -37|[]-> b(a(a(x10740)))
       b(b(a(x10741))) <-42|0[]- b(c(a(x10741))) -39|[]-> c(a(a(x10741)))
       a(b(a(x10742))) <-42|0[]- a(c(a(x10742))) -41|[]-> a(a(a(x10742)))
       b(a(x)) <-42|[]- c(a(x)) -43|[]-> b(c(x))
       b(a(x)) <-42|[]- c(a(x)) -44|[]-> c(b(x))
       c(b(a(x10745))) <-42|0[]- c(c(a(x10745))) -50|[]-> c(b(a(x10745)))
       c(b(a(x10746))) <-42|0[]- c(c(a(x10746))) -52|[]-> b(a(a(x10746)))
       c(b(a(x10747))) <-42|0[]- c(c(a(x10747))) -53|[]-> b(c(a(x10747)))
       b(b(c(x10748))) <-43|0[]- b(c(a(x10748))) -5|[]-> a(a(a(x10748)))
       b(b(c(x10749))) <-43|0[]- b(c(a(x10749))) -6|[]-> c(b(a(x10749)))
       a(b(c(x10750))) <-43|0[]- a(c(a(x10750))) -7|[]-> c(b(a(x10750)))
       a(b(c(x10751))) <-43|0[]- a(c(a(x10751))) -8|[]-> c(c(a(x10751)))
       b(c(x)) <-43|[]- c(a(x)) -9|[]-> a(c(x))
       b(c(x)) <-43|[]- c(a(x)) -10|[]-> c(c(x))
       b(c(x)) <-43|[]- c(a(x)) -11|[]-> b(b(x))
       c(b(c(x10755))) <-43|0[]- c(c(a(x10755))) -15|[]-> a(c(a(x10755)))
       c(b(c(x10756))) <-43|0[]- c(c(a(x10756))) -16|[]-> c(a(a(x10756)))
       a(b(c(x10757))) <-43|0[]- a(c(a(x10757))) -19|[]-> b(c(a(x10757)))
       b(b(c(x10758))) <-43|0[]- b(c(a(x10758))) -20|[]-> b(a(a(x10758)))
       b(b(c(x10759))) <-43|0[]- b(c(a(x10759))) -23|[]-> a(c(a(x10759)))
       a(b(c(x10760))) <-43|0[]- a(c(a(x10760))) -25|[]-> c(a(a(x10760)))
       b(c(x)) <-43|[]- c(a(x)) -26|[]-> a(a(x))
       c(b(c(x10762))) <-43|0[]- c(c(a(x10762))) -30|[]-> b(b(a(x10762)))
       c(b(c(x10763))) <-43|0[]- c(c(a(x10763))) -32|[]-> a(a(a(x10763)))
       a(b(c(x10764))) <-43|0[]- a(c(a(x10764))) -37|[]-> b(a(a(x10764)))
       b(b(c(x10765))) <-43|0[]- b(c(a(x10765))) -39|[]-> c(a(a(x10765)))
       a(b(c(x10766))) <-43|0[]- a(c(a(x10766))) -41|[]-> a(a(a(x10766)))
       b(c(x)) <-43|[]- c(a(x)) -42|[]-> b(a(x))
       b(c(x)) <-43|[]- c(a(x)) -44|[]-> c(b(x))
       c(b(c(x10769))) <-43|0[]- c(c(a(x10769))) -50|[]-> c(b(a(x10769)))
       c(b(c(x10770))) <-43|0[]- c(c(a(x10770))) -52|[]-> b(a(a(x10770)))
       c(b(c(x10771))) <-43|0[]- c(c(a(x10771))) -53|[]-> b(c(a(x10771)))
       b(c(b(x10772))) <-44|0[]- b(c(a(x10772))) -5|[]-> a(a(a(x10772)))
       b(c(b(x10773))) <-44|0[]- b(c(a(x10773))) -6|[]-> c(b(a(x10773)))
       a(c(b(x10774))) <-44|0[]- a(c(a(x10774))) -7|[]-> c(b(a(x10774)))
       a(c(b(x10775))) <-44|0[]- a(c(a(x10775))) -8|[]-> c(c(a(x10775)))
       c(b(x)) <-44|[]- c(a(x)) -9|[]-> a(c(x))
       c(b(x)) <-44|[]- c(a(x)) -10|[]-> c(c(x))
       c(b(x)) <-44|[]- c(a(x)) -11|[]-> b(b(x))
       c(c(b(x10779))) <-44|0[]- c(c(a(x10779))) -15|[]-> a(c(a(x10779)))
       c(c(b(x10780))) <-44|0[]- c(c(a(x10780))) -16|[]-> c(a(a(x10780)))
       a(c(b(x10781))) <-44|0[]- a(c(a(x10781))) -19|[]-> b(c(a(x10781)))
       b(c(b(x10782))) <-44|0[]- b(c(a(x10782))) -20|[]-> b(a(a(x10782)))
       b(c(b(x10783))) <-44|0[]- b(c(a(x10783))) -23|[]-> a(c(a(x10783)))
       a(c(b(x10784))) <-44|0[]- a(c(a(x10784))) -25|[]-> c(a(a(x10784)))
       c(b(x)) <-44|[]- c(a(x)) -26|[]-> a(a(x))
       c(c(b(x10786))) <-44|0[]- c(c(a(x10786))) -30|[]-> b(b(a(x10786)))
       c(c(b(x10787))) <-44|0[]- c(c(a(x10787))) -32|[]-> a(a(a(x10787)))
       a(c(b(x10788))) <-44|0[]- a(c(a(x10788))) -37|[]-> b(a(a(x10788)))
       b(c(b(x10789))) <-44|0[]- b(c(a(x10789))) -39|[]-> c(a(a(x10789)))
       a(c(b(x10790))) <-44|0[]- a(c(a(x10790))) -41|[]-> a(a(a(x10790)))
       c(b(x)) <-44|[]- c(a(x)) -42|[]-> b(a(x))
       c(b(x)) <-44|[]- c(a(x)) -43|[]-> b(c(x))
       c(c(b(x10793))) <-44|0[]- c(c(a(x10793))) -50|[]-> c(b(a(x10793)))
       c(c(b(x10794))) <-44|0[]- c(c(a(x10794))) -52|[]-> b(a(a(x10794)))
       c(c(b(x10795))) <-44|0[]- c(c(a(x10795))) -53|[]-> b(c(a(x10795)))
       c(c(x)) <-45|[]- a(a(x)) -4|[]-> c(a(x))
       a(c(c(x10797))) <-45|0[]- a(a(a(x10797))) -4|[]-> c(a(a(x10797)))
       c(c(c(x10798))) <-45|0[]- c(a(a(x10798))) -9|[]-> a(c(a(x10798)))
       c(c(c(x10799))) <-45|0[]- c(a(a(x10799))) -10|[]-> c(c(a(x10799)))
       c(c(c(x10800))) <-45|0[]- c(a(a(x10800))) -11|[]-> b(b(a(x10800)))
       c(c(x)) <-45|[]- a(a(x)) -12|[]-> b(b(x))
       a(c(c(x10802))) <-45|0[]- a(a(a(x10802))) -12|[]-> b(b(a(x10802)))
       c(c(x)) <-45|[]- a(a(x)) -21|[]-> b(a(x))
       a(c(c(x10804))) <-45|0[]- a(a(a(x10804))) -21|[]-> b(a(a(x10804)))
       c(c(x)) <-45|[]- a(a(x)) -22|[]-> b(c(x))
       a(c(c(x10806))) <-45|0[]- a(a(a(x10806))) -22|[]-> b(c(a(x10806)))
       c(c(c(x10807))) <-45|0[]- c(a(a(x10807))) -26|[]-> a(a(a(x10807)))
       c(c(x)) <-45|[]- a(a(x)) -27|[]-> c(b(x))
       a(c(c(x10809))) <-45|0[]- a(a(a(x10809))) -27|[]-> c(b(a(x10809)))
       c(c(x)) <-45|[]- a(a(x)) -38|[]-> a(c(x))
       a(c(c(x10811))) <-45|0[]- a(a(a(x10811))) -38|[]-> a(c(a(x10811)))
       c(c(c(x10812))) <-45|0[]- c(a(a(x10812))) -42|[]-> b(a(a(x10812)))
       c(c(c(x10813))) <-45|0[]- c(a(a(x10813))) -43|[]-> b(c(a(x10813)))
       c(c(c(x10814))) <-45|0[]- c(a(a(x10814))) -44|[]-> c(b(a(x10814)))
       a(c(c(x10815))) <-45|0[]- a(a(a(x10815))) -45|[]-> c(c(a(x10815)))
       a(b(c(x10816))) <-46|0[]- a(b(b(x10816))) -0|[]-> a(c(b(x10816)))
       a(b(c(x10817))) <-46|0[]- a(b(b(x10817))) -1|[]-> c(c(b(x10817)))
       a(b(c(x10818))) <-46|0[]- a(b(b(x10818))) -2|[]-> c(a(b(x10818)))
       a(b(c(x10819))) <-46|0[]- a(b(b(x10819))) -3|[]-> b(b(b(x10819)))
       b(c(x)) <-46|[]- b(b(x)) -13|[]-> c(a(x))
       b(b(c(x10821))) <-46|0[]- b(b(b(x10821))) -13|[]-> c(a(b(x10821)))
       b(c(x)) <-46|[]- b(b(x)) -14|[]-> b(a(x))
       b(b(c(x10823))) <-46|0[]- b(b(b(x10823))) -14|[]-> b(a(b(x10823)))
       a(b(c(x10824))) <-46|0[]- a(b(b(x10824))) -17|[]-> a(a(b(x10824)))
       c(b(c(x10825))) <-46|0[]- c(b(b(x10825))) -18|[]-> b(c(b(x10825)))
       c(b(c(x10826))) <-46|0[]- c(b(b(x10826))) -24|[]-> a(c(b(x10826)))
       b(c(x)) <-46|[]- b(b(x)) -28|[]-> c(b(x))
       b(b(c(x10828))) <-46|0[]- b(b(b(x10828))) -28|[]-> c(b(b(x10828)))
       c(b(c(x10829))) <-46|0[]- c(b(b(x10829))) -29|[]-> c(c(b(x10829)))
       b(c(x)) <-46|[]- b(b(x)) -31|[]-> c(c(x))
       b(b(c(x10831))) <-46|0[]- b(b(b(x10831))) -31|[]-> c(c(b(x10831)))
       a(b(c(x10832))) <-46|0[]- a(b(b(x10832))) -33|[]-> b(a(b(x10832)))
       a(b(c(x10833))) <-46|0[]- a(b(b(x10833))) -34|[]-> b(c(b(x10833)))
       a(b(c(x10834))) <-46|0[]- a(b(b(x10834))) -35|[]-> c(b(b(x10834)))
       c(b(c(x10835))) <-46|0[]- c(b(b(x10835))) -36|[]-> b(a(b(x10835)))
       c(b(c(x10836))) <-46|0[]- c(b(b(x10836))) -40|[]-> c(a(b(x10836)))
       b(b(c(x10837))) <-46|0[]- b(b(b(x10837))) -46|[]-> b(c(b(x10837)))
       b(c(x)) <-46|[]- b(b(x)) -47|[]-> a(c(x))
       b(b(c(x10839))) <-46|0[]- b(b(b(x10839))) -47|[]-> a(c(b(x10839)))
       c(b(c(x10840))) <-46|0[]- c(b(b(x10840))) -48|[]-> b(b(b(x10840)))
       c(b(c(x10841))) <-46|0[]- c(b(b(x10841))) -49|[]-> a(a(b(x10841)))
       b(c(x)) <-46|[]- b(b(x)) -51|[]-> a(a(x))
       b(b(c(x10843))) <-46|0[]- b(b(b(x10843))) -51|[]-> a(a(b(x10843)))
       a(a(c(x10844))) <-47|0[]- a(b(b(x10844))) -0|[]-> a(c(b(x10844)))
       a(a(c(x10845))) <-47|0[]- a(b(b(x10845))) -1|[]-> c(c(b(x10845)))
       a(a(c(x10846))) <-47|0[]- a(b(b(x10846))) -2|[]-> c(a(b(x10846)))
       a(a(c(x10847))) <-47|0[]- a(b(b(x10847))) -3|[]-> b(b(b(x10847)))
       a(c(x)) <-47|[]- b(b(x)) -13|[]-> c(a(x))
       b(a(c(x10849))) <-47|0[]- b(b(b(x10849))) -13|[]-> c(a(b(x10849)))
       a(c(x)) <-47|[]- b(b(x)) -14|[]-> b(a(x))
       b(a(c(x10851))) <-47|0[]- b(b(b(x10851))) -14|[]-> b(a(b(x10851)))
       a(a(c(x10852))) <-47|0[]- a(b(b(x10852))) -17|[]-> a(a(b(x10852)))
       c(a(c(x10853))) <-47|0[]- c(b(b(x10853))) -18|[]-> b(c(b(x10853)))
       c(a(c(x10854))) <-47|0[]- c(b(b(x10854))) -24|[]-> a(c(b(x10854)))
       a(c(x)) <-47|[]- b(b(x)) -28|[]-> c(b(x))
       b(a(c(x10856))) <-47|0[]- b(b(b(x10856))) -28|[]-> c(b(b(x10856)))
       c(a(c(x10857))) <-47|0[]- c(b(b(x10857))) -29|[]-> c(c(b(x10857)))
       a(c(x)) <-47|[]- b(b(x)) -31|[]-> c(c(x))
       b(a(c(x10859))) <-47|0[]- b(b(b(x10859))) -31|[]-> c(c(b(x10859)))
       a(a(c(x10860))) <-47|0[]- a(b(b(x10860))) -33|[]-> b(a(b(x10860)))
       a(a(c(x10861))) <-47|0[]- a(b(b(x10861))) -34|[]-> b(c(b(x10861)))
       a(a(c(x10862))) <-47|0[]- a(b(b(x10862))) -35|[]-> c(b(b(x10862)))
       c(a(c(x10863))) <-47|0[]- c(b(b(x10863))) -36|[]-> b(a(b(x10863)))
       c(a(c(x10864))) <-47|0[]- c(b(b(x10864))) -40|[]-> c(a(b(x10864)))
       a(c(x)) <-47|[]- b(b(x)) -46|[]-> b(c(x))
       b(a(c(x10866))) <-47|0[]- b(b(b(x10866))) -46|[]-> b(c(b(x10866)))
       b(a(c(x10867))) <-47|0[]- b(b(b(x10867))) -47|[]-> a(c(b(x10867)))
       c(a(c(x10868))) <-47|0[]- c(b(b(x10868))) -48|[]-> b(b(b(x10868)))
       c(a(c(x10869))) <-47|0[]- c(b(b(x10869))) -49|[]-> a(a(b(x10869)))
       a(c(x)) <-47|[]- b(b(x)) -51|[]-> a(a(x))
       b(a(c(x10871))) <-47|0[]- b(b(b(x10871))) -51|[]-> a(a(b(x10871)))
       b(b(b(x10872))) <-48|0[]- b(c(b(x10872))) -5|[]-> a(a(b(x10872)))
       b(b(b(x10873))) <-48|0[]- b(c(b(x10873))) -6|[]-> c(b(b(x10873)))
       a(b(b(x10874))) <-48|0[]- a(c(b(x10874))) -7|[]-> c(b(b(x10874)))
       a(b(b(x10875))) <-48|0[]- a(c(b(x10875))) -8|[]-> c(c(b(x10875)))
       c(b(b(x10876))) <-48|0[]- c(c(b(x10876))) -15|[]-> a(c(b(x10876)))
       c(b(b(x10877))) <-48|0[]- c(c(b(x10877))) -16|[]-> c(a(b(x10877)))
       b(b(x)) <-48|[]- c(b(x)) -18|[]-> b(c(x))
       a(b(b(x10879))) <-48|0[]- a(c(b(x10879))) -19|[]-> b(c(b(x10879)))
       b(b(b(x10880))) <-48|0[]- b(c(b(x10880))) -20|[]-> b(a(b(x10880)))
       b(b(b(x10881))) <-48|0[]- b(c(b(x10881))) -23|[]-> a(c(b(x10881)))
       b(b(x)) <-48|[]- c(b(x)) -24|[]-> a(c(x))
       a(b(b(x10883))) <-48|0[]- a(c(b(x10883))) -25|[]-> c(a(b(x10883)))
       b(b(x)) <-48|[]- c(b(x)) -29|[]-> c(c(x))
       c(b(b(x10885))) <-48|0[]- c(c(b(x10885))) -30|[]-> b(b(b(x10885)))
       c(b(b(x10886))) <-48|0[]- c(c(b(x10886))) -32|[]-> a(a(b(x10886)))
       b(b(x)) <-48|[]- c(b(x)) -36|[]-> b(a(x))
       a(b(b(x10888))) <-48|0[]- a(c(b(x10888))) -37|[]-> b(a(b(x10888)))
       b(b(b(x10889))) <-48|0[]- b(c(b(x10889))) -39|[]-> c(a(b(x10889)))
       b(b(x)) <-48|[]- c(b(x)) -40|[]-> c(a(x))
       a(b(b(x10891))) <-48|0[]- a(c(b(x10891))) -41|[]-> a(a(b(x10891)))
       b(b(x)) <-48|[]- c(b(x)) -49|[]-> a(a(x))
       c(b(b(x10893))) <-48|0[]- c(c(b(x10893))) -50|[]-> c(b(b(x10893)))
       c(b(b(x10894))) <-48|0[]- c(c(b(x10894))) -52|[]-> b(a(b(x10894)))
       c(b(b(x10895))) <-48|0[]- c(c(b(x10895))) -53|[]-> b(c(b(x10895)))
       b(a(a(x10896))) <-49|0[]- b(c(b(x10896))) -5|[]-> a(a(b(x10896)))
       b(a(a(x10897))) <-49|0[]- b(c(b(x10897))) -6|[]-> c(b(b(x10897)))
       a(a(a(x10898))) <-49|0[]- a(c(b(x10898))) -7|[]-> c(b(b(x10898)))
       a(a(a(x10899))) <-49|0[]- a(c(b(x10899))) -8|[]-> c(c(b(x10899)))
       c(a(a(x10900))) <-49|0[]- c(c(b(x10900))) -15|[]-> a(c(b(x10900)))
       c(a(a(x10901))) <-49|0[]- c(c(b(x10901))) -16|[]-> c(a(b(x10901)))
       a(a(x)) <-49|[]- c(b(x)) -18|[]-> b(c(x))
       a(a(a(x10903))) <-49|0[]- a(c(b(x10903))) -19|[]-> b(c(b(x10903)))
       b(a(a(x10904))) <-49|0[]- b(c(b(x10904))) -20|[]-> b(a(b(x10904)))
       b(a(a(x10905))) <-49|0[]- b(c(b(x10905))) -23|[]-> a(c(b(x10905)))
       a(a(x)) <-49|[]- c(b(x)) -24|[]-> a(c(x))
       a(a(a(x10907))) <-49|0[]- a(c(b(x10907))) -25|[]-> c(a(b(x10907)))
       a(a(x)) <-49|[]- c(b(x)) -29|[]-> c(c(x))
       c(a(a(x10909))) <-49|0[]- c(c(b(x10909))) -30|[]-> b(b(b(x10909)))
       c(a(a(x10910))) <-49|0[]- c(c(b(x10910))) -32|[]-> a(a(b(x10910)))
       a(a(x)) <-49|[]- c(b(x)) -36|[]-> b(a(x))
       a(a(a(x10912))) <-49|0[]- a(c(b(x10912))) -37|[]-> b(a(b(x10912)))
       b(a(a(x10913))) <-49|0[]- b(c(b(x10913))) -39|[]-> c(a(b(x10913)))
       a(a(x)) <-49|[]- c(b(x)) -40|[]-> c(a(x))
       a(a(a(x10915))) <-49|0[]- a(c(b(x10915))) -41|[]-> a(a(b(x10915)))
       a(a(x)) <-49|[]- c(b(x)) -48|[]-> b(b(x))
       c(a(a(x10917))) <-49|0[]- c(c(b(x10917))) -50|[]-> c(b(b(x10917)))
       c(a(a(x10918))) <-49|0[]- c(c(b(x10918))) -52|[]-> b(a(b(x10918)))
       c(a(a(x10919))) <-49|0[]- c(c(b(x10919))) -53|[]-> b(c(b(x10919)))
       b(c(b(x10920))) <-50|0[]- b(c(c(x10920))) -5|[]-> a(a(c(x10920)))
       b(c(b(x10921))) <-50|0[]- b(c(c(x10921))) -6|[]-> c(b(c(x10921)))
       a(c(b(x10922))) <-50|0[]- a(c(c(x10922))) -7|[]-> c(b(c(x10922)))
       a(c(b(x10923))) <-50|0[]- a(c(c(x10923))) -8|[]-> c(c(c(x10923)))
       c(b(x)) <-50|[]- c(c(x)) -15|[]-> a(c(x))
       c(c(b(x10925))) <-50|0[]- c(c(c(x10925))) -15|[]-> a(c(c(x10925)))
       c(b(x)) <-50|[]- c(c(x)) -16|[]-> c(a(x))
       c(c(b(x10927))) <-50|0[]- c(c(c(x10927))) -16|[]-> c(a(c(x10927)))
       a(c(b(x10928))) <-50|0[]- a(c(c(x10928))) -19|[]-> b(c(c(x10928)))
       b(c(b(x10929))) <-50|0[]- b(c(c(x10929))) -20|[]-> b(a(c(x10929)))
       b(c(b(x10930))) <-50|0[]- b(c(c(x10930))) -23|[]-> a(c(c(x10930)))
       a(c(b(x10931))) <-50|0[]- a(c(c(x10931))) -25|[]-> c(a(c(x10931)))
       c(b(x)) <-50|[]- c(c(x)) -30|[]-> b(b(x))
       c(c(b(x10933))) <-50|0[]- c(c(c(x10933))) -30|[]-> b(b(c(x10933)))
       c(b(x)) <-50|[]- c(c(x)) -32|[]-> a(a(x))
       c(c(b(x10935))) <-50|0[]- c(c(c(x10935))) -32|[]-> a(a(c(x10935)))
       a(c(b(x10936))) <-50|0[]- a(c(c(x10936))) -37|[]-> b(a(c(x10936)))
       b(c(b(x10937))) <-50|0[]- b(c(c(x10937))) -39|[]-> c(a(c(x10937)))
       a(c(b(x10938))) <-50|0[]- a(c(c(x10938))) -41|[]-> a(a(c(x10938)))
       c(c(b(x10939))) <-50|0[]- c(c(c(x10939))) -50|[]-> c(b(c(x10939)))
       c(b(x)) <-50|[]- c(c(x)) -52|[]-> b(a(x))
       c(c(b(x10941))) <-50|0[]- c(c(c(x10941))) -52|[]-> b(a(c(x10941)))
       c(b(x)) <-50|[]- c(c(x)) -53|[]-> b(c(x))
       c(c(b(x10943))) <-50|0[]- c(c(c(x10943))) -53|[]-> b(c(c(x10943)))
       a(a(a(x10944))) <-51|0[]- a(b(b(x10944))) -0|[]-> a(c(b(x10944)))
       a(a(a(x10945))) <-51|0[]- a(b(b(x10945))) -1|[]-> c(c(b(x10945)))
       a(a(a(x10946))) <-51|0[]- a(b(b(x10946))) -2|[]-> c(a(b(x10946)))
       a(a(a(x10947))) <-51|0[]- a(b(b(x10947))) -3|[]-> b(b(b(x10947)))
       a(a(x)) <-51|[]- b(b(x)) -13|[]-> c(a(x))
       b(a(a(x10949))) <-51|0[]- b(b(b(x10949))) -13|[]-> c(a(b(x10949)))
       a(a(x)) <-51|[]- b(b(x)) -14|[]-> b(a(x))
       b(a(a(x10951))) <-51|0[]- b(b(b(x10951))) -14|[]-> b(a(b(x10951)))
       a(a(a(x10952))) <-51|0[]- a(b(b(x10952))) -17|[]-> a(a(b(x10952)))
       c(a(a(x10953))) <-51|0[]- c(b(b(x10953))) -18|[]-> b(c(b(x10953)))
       c(a(a(x10954))) <-51|0[]- c(b(b(x10954))) -24|[]-> a(c(b(x10954)))
       a(a(x)) <-51|[]- b(b(x)) -28|[]-> c(b(x))
       b(a(a(x10956))) <-51|0[]- b(b(b(x10956))) -28|[]-> c(b(b(x10956)))
       c(a(a(x10957))) <-51|0[]- c(b(b(x10957))) -29|[]-> c(c(b(x10957)))
       a(a(x)) <-51|[]- b(b(x)) -31|[]-> c(c(x))
       b(a(a(x10959))) <-51|0[]- b(b(b(x10959))) -31|[]-> c(c(b(x10959)))
       a(a(a(x10960))) <-51|0[]- a(b(b(x10960))) -33|[]-> b(a(b(x10960)))
       a(a(a(x10961))) <-51|0[]- a(b(b(x10961))) -34|[]-> b(c(b(x10961)))
       a(a(a(x10962))) <-51|0[]- a(b(b(x10962))) -35|[]-> c(b(b(x10962)))
       c(a(a(x10963))) <-51|0[]- c(b(b(x10963))) -36|[]-> b(a(b(x10963)))
       c(a(a(x10964))) <-51|0[]- c(b(b(x10964))) -40|[]-> c(a(b(x10964)))
       a(a(x)) <-51|[]- b(b(x)) -46|[]-> b(c(x))
       b(a(a(x10966))) <-51|0[]- b(b(b(x10966))) -46|[]-> b(c(b(x10966)))
       a(a(x)) <-51|[]- b(b(x)) -47|[]-> a(c(x))
       b(a(a(x10968))) <-51|0[]- b(b(b(x10968))) -47|[]-> a(c(b(x10968)))
       c(a(a(x10969))) <-51|0[]- c(b(b(x10969))) -48|[]-> b(b(b(x10969)))
       c(a(a(x10970))) <-51|0[]- c(b(b(x10970))) -49|[]-> a(a(b(x10970)))
       b(a(a(x10971))) <-51|0[]- b(b(b(x10971))) -51|[]-> a(a(b(x10971)))
       b(b(a(x10972))) <-52|0[]- b(c(c(x10972))) -5|[]-> a(a(c(x10972)))
       b(b(a(x10973))) <-52|0[]- b(c(c(x10973))) -6|[]-> c(b(c(x10973)))
       a(b(a(x10974))) <-52|0[]- a(c(c(x10974))) -7|[]-> c(b(c(x10974)))
       a(b(a(x10975))) <-52|0[]- a(c(c(x10975))) -8|[]-> c(c(c(x10975)))
       b(a(x)) <-52|[]- c(c(x)) -15|[]-> a(c(x))
       c(b(a(x10977))) <-52|0[]- c(c(c(x10977))) -15|[]-> a(c(c(x10977)))
       b(a(x)) <-52|[]- c(c(x)) -16|[]-> c(a(x))
       c(b(a(x10979))) <-52|0[]- c(c(c(x10979))) -16|[]-> c(a(c(x10979)))
       a(b(a(x10980))) <-52|0[]- a(c(c(x10980))) -19|[]-> b(c(c(x10980)))
       b(b(a(x10981))) <-52|0[]- b(c(c(x10981))) -20|[]-> b(a(c(x10981)))
       b(b(a(x10982))) <-52|0[]- b(c(c(x10982))) -23|[]-> a(c(c(x10982)))
       a(b(a(x10983))) <-52|0[]- a(c(c(x10983))) -25|[]-> c(a(c(x10983)))
       b(a(x)) <-52|[]- c(c(x)) -30|[]-> b(b(x))
       c(b(a(x10985))) <-52|0[]- c(c(c(x10985))) -30|[]-> b(b(c(x10985)))
       b(a(x)) <-52|[]- c(c(x)) -32|[]-> a(a(x))
       c(b(a(x10987))) <-52|0[]- c(c(c(x10987))) -32|[]-> a(a(c(x10987)))
       a(b(a(x10988))) <-52|0[]- a(c(c(x10988))) -37|[]-> b(a(c(x10988)))
       b(b(a(x10989))) <-52|0[]- b(c(c(x10989))) -39|[]-> c(a(c(x10989)))
       a(b(a(x10990))) <-52|0[]- a(c(c(x10990))) -41|[]-> a(a(c(x10990)))
       b(a(x)) <-52|[]- c(c(x)) -50|[]-> c(b(x))
       c(b(a(x10992))) <-52|0[]- c(c(c(x10992))) -50|[]-> c(b(c(x10992)))
       c(b(a(x10993))) <-52|0[]- c(c(c(x10993))) -52|[]-> b(a(c(x10993)))
       b(a(x)) <-52|[]- c(c(x)) -53|[]-> b(c(x))
       c(b(a(x10995))) <-52|0[]- c(c(c(x10995))) -53|[]-> b(c(c(x10995)))
       b(b(c(x10996))) <-53|0[]- b(c(c(x10996))) -5|[]-> a(a(c(x10996)))
       b(b(c(x10997))) <-53|0[]- b(c(c(x10997))) -6|[]-> c(b(c(x10997)))
       a(b(c(x10998))) <-53|0[]- a(c(c(x10998))) -7|[]-> c(b(c(x10998)))
       a(b(c(x10999))) <-53|0[]- a(c(c(x10999))) -8|[]-> c(c(c(x10999)))
       b(c(x)) <-53|[]- c(c(x)) -15|[]-> a(c(x))
       c(b(c(x11001))) <-53|0[]- c(c(c(x11001))) -15|[]-> a(c(c(x11001)))
       b(c(x)) <-53|[]- c(c(x)) -16|[]-> c(a(x))
       c(b(c(x11003))) <-53|0[]- c(c(c(x11003))) -16|[]-> c(a(c(x11003)))
       a(b(c(x11004))) <-53|0[]- a(c(c(x11004))) -19|[]-> b(c(c(x11004)))
       b(b(c(x11005))) <-53|0[]- b(c(c(x11005))) -20|[]-> b(a(c(x11005)))
       b(b(c(x11006))) <-53|0[]- b(c(c(x11006))) -23|[]-> a(c(c(x11006)))
       a(b(c(x11007))) <-53|0[]- a(c(c(x11007))) -25|[]-> c(a(c(x11007)))
       b(c(x)) <-53|[]- c(c(x)) -30|[]-> b(b(x))
       c(b(c(x11009))) <-53|0[]- c(c(c(x11009))) -30|[]-> b(b(c(x11009)))
       b(c(x)) <-53|[]- c(c(x)) -32|[]-> a(a(x))
       c(b(c(x11011))) <-53|0[]- c(c(c(x11011))) -32|[]-> a(a(c(x11011)))
       a(b(c(x11012))) <-53|0[]- a(c(c(x11012))) -37|[]-> b(a(c(x11012)))
       b(b(c(x11013))) <-53|0[]- b(c(c(x11013))) -39|[]-> c(a(c(x11013)))
       a(b(c(x11014))) <-53|0[]- a(c(c(x11014))) -41|[]-> a(a(c(x11014)))
       b(c(x)) <-53|[]- c(c(x)) -50|[]-> c(b(x))
       c(b(c(x11016))) <-53|0[]- c(c(c(x11016))) -50|[]-> c(b(c(x11016)))
       b(c(x)) <-53|[]- c(c(x)) -52|[]-> b(a(x))
       c(b(c(x11018))) <-53|0[]- c(c(c(x11018))) -52|[]-> b(a(c(x11018)))
       c(b(c(x11019))) <-53|0[]- c(c(c(x11019))) -53|[]-> b(c(c(x11019)))
      Closedness Processor (*strongly -- <=7 steps*):
       
       Qed