Script started on Mon 06 Aug 2007 08:51:48 BST
frmb@tadpole:~/toys/lambda$ ./lambda 
Fred's Lambda-Calculus Thing (version 0.2)
: I = \x.x
: K = \xy.x
: S = \xyz.(xz(yz))
: B = \xyz.(x(yz))
: C = \xyz.(xzy)
: Y = \f.((\x.(f(xx)))(\x.(f(xx))))
: T = K
: F = \xy.y
: _CA = \mnsz.(ms(nsz))
: _CM = \mns.(m(ns))
: _CE = \mn.(nm)
: _if = \x.x
: _true = T
: _false = F
: _nonf = (\x.(xx) \y.(yy))
: _explode = (\x.(xx) \q.(qqq))
: _swap = \f.(}(f),{(f))
: _merge = \f.(( {({(f)) , {(}(f)) ),( }({(f)) , }(}(f)) ))
: _apply = \f.({(f)}(f))
: _and = \fg.(fgF)
: _imp = \fg.(fgK)
: _or = \fg.(fK(gKF))
: _not = \f.(fFK)
: _xor = \fg.(f(gFK)(gKF))
: _cons = \xys.(sxy)
: _nil = \x.K
: _isnil = \p.(p (\xy.F))
: _hd = \p.(p K)
: _tl = \p.(p F)
: _fix = ( (\xy.(y(xxy))) (\xy.(y(xxy))) )
: _nlparta = ("cons" a ("cons" b ("cons" c "nil")))
: _nlpartb = ("cons" d ("cons" e "nil"))
: _nlpartc = ("cons" f "nil")
: _nllist = ("cons" "nlparta" ("cons" "nlpartb" ("cons" "nlpartc" "nil")))
: :"nllist"
(\s.(s (\s.(s a (\s.(s b (\s.(s c (\xxy.x))))))) (\s.(s (\s.(s d (\s.(s e (\xxy.x))))) (\s.(s (\s.(s f (\xxy.x))) (\xxy.x)))))))
: _nicelist = "@"
: _shortlist = ("cons" ("cons" a "nil") "nil")
: _numblist = ("cons" '1 ("cons" '2 ("cons" '3 "nil")))
: :"numblist"
(\s.(s (\xy.(x y)) (\s.(s (\xy.(x (x y))) (\s.(s (\xy.(x (x (x y)))) (\xxy.x)))))))
: _numberlist = "@"
: _fst = \p.{(p)
: _snd = \p.}(p)
: _select = \nl.("fst" ((n "snd") l))
: _joining = \fxy.(("isnil" x) y ("cons" ("hd" x) (f ("tl" x) y) ))
: _join = ("fix" "joining")
: _flattening = \fl.(("isnil" l) l ("join" ("hd" l) (f ("tl" l))) )
: _flatten = ("fix" "flattening")
: _mapping = \rfl.(("isnil" l) l ("cons" (f ("hd" l)) (r f ("tl" l)) ))
: _map = ("fix" "mapping")
: _timestwo = \x.("CM" '2 x)
: _iszero = \n.(n (KF) K)
: _INturtape = ("cons" '1 ("cons" "nil" ("cons" '1 ("cons" '0 "nil"))))
: :_INturtape
(\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x)))))))))
: _turtape = @
: _INleftsym = \t.("hd" ("hd" ("tl" t)))
: _INrightsym = \t.("hd" ("tl" ("tl" t)))
: _INlefttape = \t.("hd" ("tl" t))
: _INrighttape = \t.("tl" ("tl" t))
: :_INleftsym
(\t.(t (\xy.y) (\xy.x) (\xy.x)))
: _leftsym = @
: :_INrightsym
(\t.(t (\xy.y) (\xy.y) (\xy.x)))
: _rightsym = @
: :_INlefttape
(\t.(t (\xy.y) (\xy.x)))
== not
: _lefttape = @
: :_INrighttape
(\t.(t (\xy.y) (\xy.y)))
: _righttape = @
: _INreadsym = \t.("hd" t)
: _INwritesym = \st.("cons" s ("cons" ("lefttape" t) ("righttape" t)))
: :_INreadsym
(\t.(t (\xy.x)))
== hd
: _readsym = @
: :_INwritesym
(\sta.(a s (\s.(s t (\xy.y) (\xy.x) (t (\xy.y) (\xy.y))))))
: _writesym = @
: _INtapeleft = \t.("cons" ("rightsym" t) ("cons" ("cons" ("readsym" t) ("lefttape" t)) ("tl" ("righttape" t))))
: _INtaperight = \t.("cons" ("leftsym" t) ("cons" ("tl" ("lefttape" t)) ("cons" ("readsym" t) ("righttape" t))))
: :_INtapeleft
(\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y))))))
: _tapeleft = @
: :_INtaperight
(\ts.(s t (\xy.y) (\xy.x) (\xy.x) (\s.(s t (\xy.y) (\xy.x) (\xy.y) (\s.(s t (\xy.x) (t (\xy.y) (\xy.y))))))))
: _taperight = @
: _churchadd = \xy.((\mnsz.(m s (n s z))) x y)
: _addadjacent = \t.("churchadd" ("readsym" t) ("readsym" ("tapeleft" t)))
: _turprogram = \t.("writesym" ("addadjacent" t) ("tapeleft" ("tapeleft" t)))
: _INresulttape = ("cons" '2 ("cons" ("cons" '1 ("cons" '1 "nil")) "nil"))
: :_INresulttape
(\s.(s (\xy.(x (x y))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) (\xxy.x)))))
: _resulttape = @
: /von
verbose beta-reduction is on.
: /eon
verbose eta-reduction is on.
> :("turpgro    program" "turtape")
    ((\t.((\sta.(a s (\s.(s t (\xy.y) (\xy.x) (t (\xy.y) (\xy.y)))))) (\t.((\xy.((\mnsz.(m s (n s z))) x y)) (\t.(t (\xy.x))) t ((\t.(t (\xy.x))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) t)))) t ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) t)))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))))
-b> ((\sta.(a s (\s.(s t (\xy.y) (\xy.x) (t (\xy.y) (\xy.y)))))) (\t.((\xy.((\mnsz.(m s (n s z))) x y)) (\t.(t (\xy.x))) t ((\t.(t (\xy.x))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) t)))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))))))
-b> ((\ta.(a (\t.((\xy.((\mnsz.(m s (n s z))) x y)) (\t.(t (\xy.x))) t ((\t.(t (\xy.x))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) t)))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\s.(s t (\xy.y) (\xy.x) (t (\xy.y) (\xy.y)))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))))))
-b> (\a.(a (\t.((\xy.((\mnsz.(m s (n s z))) x y)) (\t.(t (\xy.x))) t ((\t.(t (\xy.x))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) t)))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\xy.((\mnsz.(m s (n s z))) x y)) (\t.(t (\xy.x))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\t.(t (\xy.x))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\y.((\mnsz.(m s (n s z))) (\t.(t (\xy.x))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) y)) (\t.(t (\xy.x))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\mnsz.(m s (n s z))) (\t.(t (\xy.x))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\t.(t (\xy.x))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\nsz.((\t.(t (\xy.x))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) s (n s z))) (\t.(t (\xy.x))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.((\t.(t (\xy.x))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) s ((\t.(t (\xy.x))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) s ((\t.(t (\xy.x))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.((\xy.x) (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) s ((\t.(t (\xy.x))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.((\yxy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) s ((\t.(t (\xy.x))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.((\xy.(x y)) s ((\t.(t (\xy.x))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.((\y.(s y)) ((\t.(t (\xy.x))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\t.(t (\xy.x))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))))) (\xy.x) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\xy.x) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\y.((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x))) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\xy.y) (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) (\xy.y) (\xy.x) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\y.y) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) (\xy.y) (\xy.x) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) (\xy.y) (\xy.x) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\xy.y) (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))) (\xy.x) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\y.y) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))) (\xy.x) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))) (\xy.x) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\xy.x) (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\yxy.(x y)) (\s.(s (\xy.y) (\xxy.x))) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\xy.(x y)) s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s ((\y.(s y)) z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\xy.y) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\y.y) (\s.(s (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\xy.x) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\ys.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.x) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\y.((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x))) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.y) (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\y.y) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) (\xy.y) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.y) (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\y.y) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.x) (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\yxy.(x y)) (\s.(s (\xy.y) (\xxy.x))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) ((\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) ((\xy.y) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) ((\y.y) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) ((\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) ((\xy.x) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) ((\ys.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.x) (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\yxy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) ((\xy.y) (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) (\xy.x)))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) ((\y.y) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) (\xy.x)))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) ((\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) (\xy.x)))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) ((\xy.x) (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x)))))))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) ((\yxxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x)))))))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\xy.y) (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\y.y) (\s.(s (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\s.(s (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\xy.y) (\s.(s (\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\y.y) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\ts.(s t (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s t (\xy.x) (t (\xy.y) (\xy.x)))) (t (\xy.y) (\xy.y) (\xy.y)))))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))))) (\xy.y) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\xy.y) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.x) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\y.y) (\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\s.(s (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y)))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\xy.y) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.x) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.x)))) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\y.y) (\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\s.(s (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))))) (\xy.y) (\xy.y) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\xy.y) (\xy.(x y)) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) (\xy.y) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\y.y) (\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) (\xy.y) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\s.(s (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))))) (\xy.y) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\xy.y) (\xxy.x) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\y.y) (\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\s.(s (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))))) (\xy.y) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\xy.y) (\xy.(x y)) (\s.(s (\xy.y) (\xxy.x))) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\y.y) (\s.(s (\xy.y) (\xxy.x))) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\s.(s (\xy.y) (\xxy.x))) (\xy.y))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\xy.y) (\xy.y) (\xxy.x))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) ((\y.y) (\xxy.x))))))
-b> (\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) (\xxy.x)))))
(\a.(a (\sz.(s (s z))) (\s.(s (\s.(s (\xy.(x y)) (\s.(s (\xy.(x y)) (\xxy.x))))) (\xxy.x)))))
== resulttape
> 
frmb@tadpole:~/toys/lambda$ 
Script done on Mon 06 Aug 2007 08:52:04 BST