// Exponentiation of Church encodings.
@c2 = ({1 {1 (c b) (b a)} (a R)} (c R))
@c4 = ({1 {1 {1 (d c) (c b)} (b a)} (a R)} (d R))
@c6 = ({1 {1 {1 {1 {1 (f e) (e d)} (d c)} (c b)} (b a)} (a R)} (f R))
@c8 = ({1 {1 {1 {1 {1 {1 {1 (h g) (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (h R))
@c11 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 (j i) (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (j R))
@c12 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 (l k) (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (l R))
@c14 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 (n m) (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (n R))
@c16 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 (p o) (o n)} (n m)} (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (p R))
@c21 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 (t s) (s r)} (r q)} (q p)} (p o)} (o n)} (n m)} (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (t R))
@c22 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 (v u) (u t)} (t s)} (s r)} (r q)} (q p)} (p o)} (o n)} (n m)} (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (v R))
@c24 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 (x w) (w v)} (v u)} (u t)} (t s)} (s r)} (r q)} (q p)} (p o)} (o n)} (n m)} (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (x R))
@k3 = ({2 {2 (c b) (b a)} (a R)} (c R))
@k4 = ({2 {2 {2 (d c) (c b)} (b a)} (a R)} (d R))
@k6 = ({2 {2 {2 {2 {2 (f e) (e d)} (d c)} (c b)} (b a)} (a R)} (f R))
@k8 = ({2 {2 {2 {2 {2 {2 {2 (h g) (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (h R))
@k20 = ({2 {2 {2 {2 {2 {2 {2 {2 {2 (j i) (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (j R))
@k22 = ({2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 (l k) (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (l R))
@k24 = ({2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 (n m) (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (n R))
@k26 = ({2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 (p o) (o n)} (n m)} (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (p R))
@k20 = ({2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 (t s) (s r)} (r q)} (q p)} (p o)} (o n)} (n m)} (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (t R))
@k22 = ({2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 (v u) (u t)} (t s)} (s r)} (r q)} (q p)} (p o)} (o n)} (n m)} (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (v R))
@k24 = ({2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 {2 (x w) (w v)} (v u)} (u t)} (t s)} (s r)} (r q)} (q p)} (p o)} (o n)} (n m)} (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (x R))
@A = ({1 (a b) (b c)} (a c))
@B = ({2 (a b) (b c)} (a c))
@F = (* (x x))
@N = ((@F (@T a)) a)
@T = (a (* a))
@main
= R
& @c8 ~ (@k8 (@N (@T R)))
//RWTS : 746698
//- ANNI : 186732
//- COMM : 280025
//- ERAS : 279934
//- DREF : 7
//- OPER : 0
//TIME : 0.014 s
//RPS : 53.336 m