if (if true then false else false) then (if true then true else false) else
if true then false else false ;;

(\x5.
   (if (if x5 then x5 else x5) then (\x7. x5) else (\x6. true))
     (if (if false then false else true) then (if true then x5 else x5) else
      if x5 then false else false))
  ((if (if (if true then false else false) then false else false) then
    (if (if true then false else true) then (\x4. true) else (\x3. true))
    else (\x2. if x2 then true else x2))
     ((if true then (\x1. true) else (\x0. false))
        (if (if true then false else true) then
         (if false then false else false) else if true then false else true))) ;;

(if (if false then true else true) then (\x1. true) else (\x0. false))
  (if (if false then true else true) then (if false then true else false)
   else if false then true else true) ;;

if (if true then false else true) then (if false then false else true) else
if true then true else false ;;

if (if false then false else false) then false else
if false then true else false ;;

(\x2. if true then (if x2 then false else true) else if x2 then x2 else true)
  ((if (if true then true else false) then (\x1. false) else (\x0. false))
     (if false then (if true then true else false) else
      if true then true else true)) ;;

(if true then (\x1. true) else (\x0. false))
  (if (if false then true else true) then (if true then false else false)
   else if false then true else false) ;;

if (if false then true else false) then (if true then false else false) else
if false then true else true ;;

(if
 (if true then (if true then false else true) else
  if true then false else true)
 then (if (if true then false else false) then (\x3. true) else (\x2. true))
 else if (if false then true else false) then (\x1. true) else (\x0. x0))
  (if (if true then true else false) then (if true then true else true) else
   if false then true else true) ;;

(\x0. if x0 then x0 else true)
  (if (if false then true else true) then (if false then true else false)
   else if true then true else true) ;;

if (if true then false else true) then (if true then true else false) else
if true then true else true ;;

if (if true then true else false) then true else if true then true else false ;;

(\x6. if true then x6 else if x6 then x6 else x6)
  ((if (if true then true else true) then (\x5. x5) else (\x4. x4))
     (if true then (\x3. false) else (\x2. true))
     ((\x1. true) (\x0. if true then false else false))) ;;

if (if false then true else false) then (if true then false else true) else
if true then true else false ;;

if (if true then true else true) then (if false then false else false) else
if true then true else true ;;

(if
 (if (if true then false else true) then (if true then true else false) else
  if false then false else false)
 then (if false then (\x4. true) else (\x3. true)) else
 (\x2. if true then false else x2))
  ((if (if true then false else true) then (\x1. false) else (\x0. true))
     (if (if false then true else true) then (if true then false else true)
      else if false then true else false)) ;;

if (if true then false else true) then (\x1. false) else (\x0. x0) ;;

(if
 (if (if false then false else true) then (if false then true else true) else
  true)
 then (if (if false then false else false) then (\x9. false) else (\x8. x8))
 else if true then (\x7. true) else (\x6. false))
  ((if
    (if (if false then false else true) then (if true then false else false)
     else if false then false else true)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. true))
     ((if false then (\x1. x1) else (\x0. x0))
        (if (if true then true else true) then
         (if true then false else false) else if true then true else false))) ;;

if (if false then false else false) then false else
if false then false else true ;;

if
(\x3. if x3 then false else x3)
  (if (if false then true else true) then true else
   if false then false else true)
then
(\x2. if false then false else false)
  (if (if true then false else true) then (if true then true else false) else
   if false then true else true)
else
(if (if true then true else true) then (\x1. false) else (\x0. x0))
  (if false then (if true then false else true) else
   if false then false else true) ;;

if (if true then true else true) then (if false then false else false) else
if true then true else false ;;

(if (if true then false else false) then (\x1. false) else (\x0. false))
  (if true then (if false then true else false) else
   if true then true else true) ;;

(if
 (if (if true then true else true) then true else
  if true then false else true)
 then (if (if false then true else true) then (\x3. x3) else (\x2. true))
 else if false then (\x1. false) else (\x0. false))
  (if
   (if (if false then true else true) then (if true then false else false)
    else if true then true else true)
   then
   (if true then (if true then false else false) else
    if true then true else true)
   else
   if (if false then false else false) then (if false then true else false)
   else if true then true else true) ;;

(\x2. (\x3. x2) (if true then x2 else x2))
  ((if (if true then true else false) then (\x1. false) else (\x0. false))
     (if (if true then true else true) then false else
      if true then false else false)) ;;

(if (\x12. x12) (if true then false else true) then
 (if (if false then false else false) then (\x11. x11) else (\x10. x10)) else
 if (if true then true else true) then (\x9. x9) else (\x8. x8))
  ((\x6. \x7. x7) ((\x5. x5) (if false then true else false)))
  ((\x3. (\x4. true) (if x3 then x3 else false))
     ((if (if true then false else false) then (\x2. x2) else (\x1. x1))
        ((\x0. false) (if false then true else false)))) ;;

\x0.
  if (if x0 then true else x0) then (if false then false else true) else
  if false then true else false ;;

if
(if
 (if (if false then false else false) then false else
  if true then true else false)
 then (if (if true then false else false) then (\x16. x16) else (\x15. true))
 else if (if false then false else true) then (\x14. false) else (\x13. true))
  ((if (if true then false else true) then (\x12. x12) else (\x11. false))
     (if (if true then false else true) then (if false then false else false)
      else if false then true else false))
then
(if
 (if (if true then true else true) then (if false then false else false) else
  if false then true else false)
 then (if (if true then false else true) then (\x10. x10) else (\x9. true))
 else if (if true then false else false) then (\x8. false) else (\x7. false))
  ((if (if false then true else true) then (\x6. true) else (\x5. x5))
     (if (if true then false else true) then (if false then true else true)
      else if true then false else true))
else
(if (if false then true else false) then (\x4. x4) else (\x3. x3))
  (\x2. if true then true else false)
  ((if (if true then true else true) then (\x1. true) else (\x0. x0))
     (if (if false then true else false) then (if true then false else false)
      else true)) ;;

\x0.
  (\x1. if x0 then false else false)
    (if (if true then false else false) then (if true then true else false)
     else if true then true else x0) ;;

(\x6.
   if (if false then x6 else false) then (if false then x6 else x6) else
   false)
  (if
   (if (if true then false else false) then (\x5. false) else (\x4. false))
     (if true then (if false then false else false) else
      if false then false else false)
   then
   (if (if false then false else true) then (\x3. true) else (\x2. x2))
     (if (if false then false else true) then (if true then false else false)
      else false)
   else
   (if true then (\x1. true) else (\x0. true))
     (if false then (if true then true else false) else false)) ;;

if true then (if false then false else true) else true ;;

(if (if true then false else false) then (\x3. false) else (\x2. x2))
  ((if (if true then true else false) then (\x1. true) else (\x0. true))
     (if false then (if false then true else false) else
      if false then true else true)) ;;

if
(if (if true then false else true) then (\x5. true) else (\x4. false))
  (if (if true then true else true) then (\x3. true) else (\x2. true))
then
(\x1. if false then false else false)
  (if (if true then false else true) then (if true then true else false) else
   if false then true else true)
else
(\x0. if true then true else x0)
  (if (if true then false else true) then (if true then false else true) else
   if false then true else true) ;;

\x0.
  if (if true then false else false) then (if false then false else true)
  else if true then false else false ;;

(\x1. \x2. x2) ((\x0. x0) (if true then true else false)) ;;

(if (\x10. x10) (if true then false else true) then
 (if (if false then false else false) then (\x9. x9) else (\x8. x8)) else
 if (if true then true else true) then (\x7. x7) else (\x6. x6))
  ((\x4. \x5. x5) ((\x3. x3) (if false then true else false)))
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if false then (\x1. true) else (\x0. x0))
        (if (if true then true else true) then false else
         if false then false else true))) ;;

(if
 (if
  (if (if false then false else false) then (if true then false else false)
   else if true then false else true)
  then
  (if (if true then true else true) then (if false then false else false)
   else if false then true else true)
  else
  if (if true then true else false) then true else
  if false then false else false)
 then
 (if
  (if (if false then true else false) then (if true then false else false)
   else if false then false else false)
  then (if (if false then true else true) then (\x7. true) else (\x6. x6))
  else if (if false then false else true) then (\x5. false) else (\x4. x4))
 else
 if
 (if (if false then false else true) then (if true then true else true) else
  if true then true else false)
 then (\x3. if true then false else false) else
 if (if false then false else false) then (\x2. x2) else (\x1. x1))
  ((\x0. if x0 then x0 else true)
     (if (if false then true else true) then (if false then false else true)
      else true)) ;;

(if
 (if (if false then true else false) then (if false then true else false)
  else if false then false else true)
 then (if (if true then true else false) then (\x6. false) else (\x5. x5))
 else if false then (\x4. false) else (\x3. false))
  ((if (if false then true else false) then (\x2. false) else (\x1. false))
     (\x0. if x0 then true else false)) ;;

\x0.
  if
  (if (if false then true else true) then (if false then x0 else true) else
   if false then false else x0)
  then
  (if (if x0 then x0 else true) then (if false then false else false) else x0)
  else
  if (if false then true else true) then (if true then true else false) else
  if false then x0 else true ;;

(if (if false then true else false) then (\x1. false) else (\x0. true))
  (if true then (if true then false else true) else
   if true then true else true) ;;

if (if (if true then true else true) then false else true) then
(\x0. true) (if false then true else true) else
if false then (if false then false else false) else
if false then true else false ;;

(if (if false then true else false) then (\x1. false) else (\x0. false))
  (if (if false then false else true) then (if false then false else false)
   else if false then false else true) ;;

(if (if true then true else true) then (\x1. false) else (\x0. x0))
  (if (if true then true else true) then true else
   if true then false else true) ;;

(if
 (if (if false then true else true) then (\x12. true) else (\x11. false))
   (if (if true then false else true) then (\x10. false) else (\x9. x9))
 then
 (if
  (if (if false then false else false) then true else
   if false then false else true)
  then (if (if true then false else true) then (\x8. x8) else (\x7. x7)) else
  if (if true then false else false) then (\x6. false) else (\x5. false))
 else (\x4. if x4 then false else false))
  ((if (if (if true then false else false) then false else false) then
    (if (if true then false else true) then (\x3. true) else (\x2. true))
    else (\x1. if x1 then true else x1))
     ((\x0. false)
        (if (if true then true else false) then false else
         if false then false else true))) ;;

(\x0. if false then x0 else x0)
  (if true then (if false then true else true) else true) ;;

(if (if false then true else false) then (\x1. false) else (\x0. false))
  (if (if false then false else true) then (if true then false else true)
   else true) ;;

(\x0. if false then x0 else x0)
  (if (if false then true else true) then false else
   if false then false else false) ;;

(if
 (if (if false then true else true) then (if false then true else false) else
  if false then true else true)
 then (if (if false then false else true) then (\x5. x5) else (\x4. true))
 else if (if true then false else true) then (\x3. x3) else (\x2. true))
  ((if (if true then true else true) then (\x1. true) else (\x0. false))
     (if (if false then false else true) then (if false then true else false)
      else if true then false else false)) ;;

(if (if true then true else false) then (\x1. true) else (\x0. false))
  (if (if true then true else true) then true else
   if true then false else true) ;;

(if (if true then true else false) then (\x1. true) else (\x0. false))
  (if (if true then true else false) then (if true then false else false)
   else if true then false else true) ;;

(if (if false then false else true) then (\x1. false) else (\x0. false))
  (if (if true then false else false) then (if false then false else true)
   else if false then true else true) ;;

\x0.
  if (if x0 then x0 else true) then (if x0 then x0 else false) else
  if true then true else x0 ;;

(if
 (if (if false then true else false) then (if true then false else false)
  else if false then false else true)
 then (\x6. if false then x6 else x6) else
 if false then (\x5. x5) else (\x4. x4))
  (\x3.
     if (if true then false else true) then x3 else if false then x3 else x3)
  ((\x2.
      if (if x2 then false else true) then (if x2 then false else x2) else x2)
     ((if (if false then true else true) then (\x1. true) else (\x0. false))
        (if (if false then true else true) then true else
         if false then false else true))) ;;

(if
 (if (if true then true else false) then (\x8. true) else (\x7. true))
   (if (if false then true else false) then false else
    if true then true else false)
 then (\x5. (\x6. false) (if true then x5 else true)) else
 if true then (\x4. x4) else (\x3. true))
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if false then (\x1. true) else (\x0. x0))
        (if (if true then true else true) then false else
         if false then false else true))) ;;

(\x2. \x3. if x3 then x3 else false)
  (if (if true then false else false) then false else
   if true then true else true)
  ((\x0. (\x1. x0) true)
     (if true then false else if false then true else true)) ;;

(if
 (if (if true then false else true) then (if true then false else false) else
  if true then false else false)
 then (if (if true then false else false) then (\x6. false) else (\x5. x5))
 else if false then (\x4. false) else (\x3. false))
  ((\x2. false)
     (if (if true then false else true) then (\x1. false) else (\x0. x0))) ;;

(if (if true then true else true) then (\x1. false) else (\x0. false))
  (if (if false then false else false) then (if false then false else true)
   else if false then true else true) ;;

(if
 (if (if false then true else false) then (if true then false else false)
  else if false then true else true)
 then (if (if true then false else false) then (\x4. false) else (\x3. x3))
 else if false then (\x2. x2) else (\x1. x1))
  ((\x0. x0) (if true then true else if true then true else false)) ;;

(\x2. \x3. true)
  (if (if true then true else true) then false else
   if false then false else false)
  ((if (if true then true else false) then (\x1. false) else (\x0. x0))
     (if true then false else if true then false else false)) ;;

if (if true then true else false) then (if true then true else false) else
if false then false else true ;;

(if
 (if (if false then true else false) then (if false then true else false)
  else if false then false else true)
 then (if false then (\x5. x5) else (\x4. false)) else
 if (if false then true else true) then (\x3. false) else (\x2. true))
  ((if (if false then false else false) then (\x1. x1) else (\x0. true))
     (if false then (if true then false else true) else
      if false then true else false)) ;;

(\x2.
   if (if false then true else x2) then (if true then true else false) else
   if x2 then true else x2)
  ((if (if false then false else false) then (\x1. x1) else (\x0. true))
     (if (if false then false else false) then (if true then true else false)
      else if true then false else false)) ;;

(\x0. if x0 then false else x0)
  (if (if false then true else false) then false else
   if true then true else true) ;;

(\x6.
   (if (if x6 then false else false) then (\x8. true) else (\x7. true))
     (if (if true then true else true) then (if x6 then true else false) else
      if true then x6 else false))
  ((if (if false then (if true then true else false) else true) then
    (if (if false then true else true) then (\x5. false) else (\x4. x4)) else
    if false then (\x3. false) else (\x2. true))
     ((if true then (\x1. x1) else (\x0. false))
        (if true then false else true))) ;;

(\x0. false)
  (if (if false then true else true) then (if false then true else false)
   else if true then true else true) ;;

if (if true then false else false) then (if true then false else true) else
if true then true else true ;;

if
(if (if true then true else true) then (if false then false else true) else
 if true then false else false)
then
(if (if true then true else false) then (if false then false else false) else
 if true then false else true)
else
if (if false then false else false) then (if false then true else false) else
if false then false else false ;;

\x0.
  (\x1. \x2. x2)
    (if (if x0 then false else false) then (if true then true else true) else
     if x0 then true else x0) ;;

(if
 (if (if false then true else true) then (if false then true else false) else
  if false then true else true)
 then (if (if false then false else true) then (\x6. x6) else (\x5. true))
 else if (if true then false else true) then (\x4. x4) else (\x3. true))
  ((if (if false then false else false) then (\x2. true) else (\x1. true))
     (\x0. if x0 then true else x0)) ;;

(if
 (if (if true then false else true) then (if false then false else false)
  else if false then false else true)
 then (if false then (\x3. x3) else (\x2. false)) else
 (\x1. if x1 then true else x1))
  ((\x0. if x0 then true else false)
     (if (if false then true else false) then (if false then true else false)
      else if true then true else false)) ;;

(if
 (if true then (if true then false else true) else
  if true then false else true)
 then (if (if true then true else false) then (\x4. true) else (\x3. true))
 else if false then (\x2. x2) else (\x1. true))
  ((\x0. if x0 then true else false)
     (if (if true then false else false) then (if false then false else true)
      else true)) ;;

(\x8. \x9. false)
  (if (if true then false else true) then (\x7. true) else (\x6. x6))
  ((if
    (if (if true then true else true) then (if false then true else false)
     else if false then false else false)
    then (if false then (\x5. true) else (\x4. true)) else
    if (if true then false else true) then (\x3. true) else (\x2. true))
     ((if (if false then false else true) then (\x1. false) else (\x0. true))
        (if (if false then false else false) then
         (if false then false else true) else if false then false else true))) ;;

(if
 (if (if true then false else false) then (if true then true else false) else
  if false then true else false)
 then (\x7. if true then false else false) else
 if true then (\x6. true) else (\x5. false))
  ((if false then (\x4. x4) else (\x3. x3))
     (if (if false then true else false) then (\x2. false) else (\x1. x1))
     ((\x0. false)
        (if (if true then true else false) then false else
         if false then false else true))) ;;

(\x1. \x2. if true then true else x2)
  ((\x0. if true then true else true)
     (if (if false then false else true) then false else
      if false then true else true)) ;;

if (if false then false else false) then false else
if false then false else false ;;

(if
 (if (if false then false else false) then (\x12. true) else (\x11. true))
   (if (if true then true else true) then (if false then true else true) else
    if false then false else true)
 then
 (if
  (if (if false then true else false) then (if true then false else false)
   else if false then false else false)
  then (if (if false then true else true) then (\x10. true) else (\x9. x9))
  else if (if false then false else true) then (\x8. false) else (\x7. x7))
 else
 if
 (if (if true then true else true) then false else
  if false then true else false)
 then (if (if true then true else true) then (\x6. true) else (\x5. x5)) else
 if (if false then false else false) then (\x4. true) else (\x3. x3))
  ((\x2. x2)
     (if (if false then true else false) then (\x1. false) else (\x0. false))
     (if (if true then false else false) then (if false then true else false)
      else true)) ;;

\x0.
  if
  (if (if true then false else false) then (if x0 then true else false) else
   x0)
  then
  (if (if false then x0 else false) then (if true then x0 else false) else
   if false then false else false)
  else
  if (if false then true else true) then (if true then true else false) else
  if false then x0 else true ;;

(\x6. \x7. if x7 then x7 else false)
  ((if (if false then true else true) then (\x5. true) else (\x4. x4))
     (if (if false then true else false) then (if false then false else true)
      else if false then true else true))
  ((\x2. \x3. false) (if true then false else if false then true else true)
     ((if (if true then false else true) then (\x1. true) else (\x0. false))
        (if (if true then true else false) then
         (if true then false else true) else if true then false else true))) ;;

(if
 (if (if true then true else true) then true else
  if true then false else true)
 then (if (if true then false else false) then (\x5. false) else (\x4. x4))
 else if (if false then false else true) then (\x3. true) else (\x2. x2))
  ((if (if true then true else false) then (\x1. x1) else (\x0. false))
     (if true then (if true then false else true) else
      if true then true else false)) ;;

(\x5. \x6. false)
  (if (if false then true else true) then (if true then false else true) else
   if false then true else true)
  (if
   (if (if false then false else false) then (\x4. x4) else (\x3. true))
     (if (if false then true else true) then (if true then false else false)
      else true)
   then
   (\x2. x2)
     (if (if false then false else false) then
      (if true then false else false) else if false then true else true)
   else
   (if true then (\x1. true) else (\x0. false))
     (if (if false then false else false) then (if true then true else true)
      else if false then true else true)) ;;

(if
 (if (if true then false else false) then (if true then true else false) else
  if false then true else false)
 then (\x7. if true then false else false) else
 if true then (\x6. true) else (\x5. false))
  ((if (if (if true then false else false) then false else false) then
    (if (if false then true else true) then (\x4. true) else (\x3. false))
    else if (if true then false else false) then (\x2. x2) else (\x1. false))
     ((\x0. false) (if (if true then false else false) then true else false))) ;;

if (if true then true else false) then (if true then false else false) else
if false then true else true ;;

(\x1. \x2. true)
  (if true then (if true then true else false) else
   if true then false else true)
  ((\x0. if x0 then true else x0)
     (if true then (if true then false else true) else
      if true then true else false)) ;;

(if (if true then false else true) then (\x1. true) else (\x0. false))
  (if (if false then false else true) then (if false then false else false)
   else if false then true else false) ;;

(if (if false then false else false) then (\x1. true) else (\x0. false))
  (if (if false then true else true) then (if false then true else false)
   else if false then true else false) ;;

(if
 (if false then (\x10. true) else (\x9. x9))
   (if (if true then true else true) then (if false then true else true) else
    if false then false else true)
 then
 (\x8.
    if false then (if true then false else false) else
    if x8 then true else x8)
 else if true then (\x7. x7) else (\x6. true))
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. x2))
     ((if (if false then false else true) then (\x1. true) else (\x0. false))
        (if (if false then false else false) then
         (if true then false else false) else false))) ;;

\x0.
  if (if x0 then false else x0) then (if x0 then true else true) else
  if true then false else false ;;

(\x5.
   if (if false then x5 else false) then (if x5 then true else x5) else
   if true then false else true)
  ((if false then (\x4. x4) else (\x3. x3))
     (if (if false then true else false) then (\x2. false) else (\x1. x1))
     ((\x0. if true then true else x0)
        (if true then false else if true then true else false))) ;;

if (if false then true else true) then (if true then false else false) else
if true then false else false ;;

(if (if true then false else true) then (\x1. false) else (\x0. false))
  (if (if false then true else true) then (if false then true else false)
   else if false then true else false) ;;

\x0.
  if (if x0 then true else x0) then (if x0 then false else true) else
  if false then true else false ;;

(\x6. if true then x6 else if x6 then x6 else x6)
  ((if (\x5. true) (\x4. true) then (\x3. if true then true else x3) else
    (\x2. if x2 then true else x2))
     ((if (if true then false else true) then (\x1. x1) else (\x0. x0))
        (if true then false else if true then true else false))) ;;

(if
 (if true then (if true then false else true) else
  if true then false else true)
 then (if (if true then true else false) then (\x5. true) else (\x4. true))
 else if false then (\x3. x3) else (\x2. true))
  ((if true then (\x1. true) else (\x0. x0))
     (if (if false then true else false) then false else
      if false then true else true)) ;;

(if
 (if (if true then false else true) then (if false then false else false)
  else if false then false else true)
 then (if (if true then true else false) then (\x4. false) else (\x3. x3))
 else if false then (\x2. x2) else (\x1. x1))
  ((\x0. false)
     (if (if true then false else false) then (if true then true else false)
      else if false then true else false)) ;;

(\x4.
   if (if false then true else x4) then (if true then x4 else true) else
   if x4 then false else true)
  ((\x2. \x3. true)
     (if (if true then true else true) then (if false then true else true)
      else if false then false else false)
     ((if (if false then false else false) then (\x1. x1) else (\x0. true))
        (if false then (if false then false else true) else
         if true then false else false))) ;;

if (if false then true else true) then (if false then false else false) else
true ;;

(\x3.
   if (if false then true else x3) then (if true then x3 else true) else
   if x3 then false else true)
  ((\x2.
      if (if x2 then x2 else true) then (if x2 then x2 else x2) else
      if x2 then false else false)
     ((if true then (\x1. false) else (\x0. true))
        (if (if true then false else false) then
         (if false then false else true) else if false then false else false))) ;;

if (if false then true else true) then (if false then false else false) else
false ;;

(if (if false then false else false) then (\x1. true) else (\x0. x0))
  (if (if false then false else false) then true else
   if true then true else true) ;;

if (if true then false else false) then true else
if false then true else false ;;

\x0.
  if (if x0 then true else x0) then (if x0 then true else true) else
  if true then true else x0 ;;

(\x1. \x2. true)
  ((\x0. if false then x0 else x0)
     (if true then true else if false then true else true)) ;;

if (if true then true else true) then (if true then false else false) else
if false then true else false ;;

\x0.
  \x1.
    (if (if true then false else false) then (if x1 then x0 else x0) else
     (\x3. x3)) ((\x2. x2) (if true then true else x1)) ;;

if (if false then false else true) then (if false then true else false) else
if false then true else true ;;

(\x2. \x3. true) (if false then (\x1. true) else (\x0. false)) ;;

\x0.
  (if (if x0 then x0 else x0) then (\x2. false) else (\x1. x1))
    (if (if true then x0 else x0) then (if false then true else x0) else
     if true then true else x0) ;;

(if (if true then false else false) then (\x1. true) else (\x0. true))
  (if (if true then false else true) then (if false then true else true) else
   true) ;;

if (if false then true else false) then (if false then false else false) else
if true then true else false ;;

(\x1.
   if (if x1 then true else true) then (if false then x1 else x1) else
   if x1 then true else true)
  ((\x0. if false then x0 else x0)
     (if true then (if false then false else true) else
      if false then true else true)) ;;

if true then (if false then false else false) else
if true then true else true ;;

(if
 (if (if false then true else true) then (if false then true else false) else
  if false then true else true)
 then (if (if false then false else true) then (\x4. x4) else (\x3. true))
 else if (if true then false else true) then (\x2. x2) else (\x1. true))
  ((\x0. x0) (if true then true else if true then true else false)) ;;

if (if true then true else true) then (if true then false else true) else
if false then true else true ;;

if (if true then true else true) then (\x1. x1) else (\x0. false) ;;

if
(if (if false then true else true) then (if true then false else true) else
 if false then true else false)
then
(if (if true then false else false) then (if true then true else true) else
 false)
else if false then (if true then true else true) else true ;;

(if
 (\x11. if true then true else x11)
   (if false then (if true then true else true) else
    if true then false else true)
 then (\x9. (\x10. false) (if true then x9 else true)) else
 if
 (if (if true then true else true) then false else
  if false then true else false)
 then (if (if true then true else true) then (\x8. true) else (\x7. x7)) else
 if (if false then false else false) then (\x6. true) else (\x5. x5))
  (if
   (\x4. if x4 then true else x4)
     (if (if false then true else false) then (if true then false else false)
      else if false then true else false)
   then
   (if true then (\x3. false) else (\x2. true))
     (if false then (if false then false else true) else true)
   else
   (if true then (\x1. x1) else (\x0. true))
     (if (if true then false else false) then (if true then false else true)
      else if false then true else true)) ;;

(if (if true then false else true) then (\x1. false) else (\x0. x0))
  (if (if false then true else false) then true else
   if false then false else false) ;;

if (if true then false else false) then true else if true then true else true ;;

(if (if true then true else true) then (\x1. x1) else (\x0. x0))
  (if (if true then true else false) then (if false then false else true)
   else if true then true else true) ;;

(\x1.
   if (if true then x1 else false) then (if x1 then false else x1) else
   if x1 then true else true)
  ((\x0. false)
     (if (if true then false else false) then (if true then true else false)
      else if false then true else false)) ;;

\x0.
  if (if true then false else true) then (if false then false else true) else
  if x0 then false else true ;;

(if
 (if (if false then false else false) then (\x15. true) else (\x14. true))
   (if (if true then true else true) then (if false then true else true) else
    if false then false else true)
 then
 (if (\x13. false) (if false then true else false) then
  (if (if false then false else false) then (\x12. true) else (\x11. true))
  else
  if (if false then false else false) then (\x10. true) else (\x9. false))
 else
 (if false then (\x8. x8) else (\x7. x7))
   (if (if true then true else true) then (\x6. x6) else (\x5. true)))
  ((\x4. x4)
     (if (if true then false else true) then (\x3. true) else (\x2. true))
     ((if false then (\x1. false) else (\x0. false))
        (if (if true then true else true) then
         (if false then false else true) else if false then true else true))) ;;

(if
 (if (if false then true else false) then false else
  if false then false else true)
 then (\x8. if true then false else false) else
 if (if false then true else false) then (\x7. true) else (\x6. true))
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. x2))
     ((if (if false then false else true) then (\x1. true) else (\x0. false))
        (if (if false then false else false) then
         (if true then false else false) else false))) ;;

\x0.
  (if (if x0 then x0 else x0) then (\x2. false) else (\x1. true))
    (if (if false then x0 else x0) then x0 else if x0 then false else true) ;;

(\x0. \x1. x1) (if false then (if true then true else true) else true)
  (if (if true then true else false) then (if false then true else false)
   else if true then true else false) ;;

(if (if true then false else false) then (\x1. true) else (\x0. true))
  (if (if true then true else true) then (if false then false else false)
   else if true then true else true) ;;

(if (if true then true else true) then (\x6. x6) else (\x5. x5))
  (\x4. if true then true else false)
  ((if
    (if (if false then false else true) then (if true then false else false)
     else if false then false else true)
    then
    (if (if false then true else true) then (\x3. true) else (\x2. false))
    else if (if false then true else false) then (\x1. true) else (\x0. x0))
     (if (if true then false else true) then (if false then true else true)
      else if true then false else false)) ;;

(\x6. \x7. x6) (if false then false else false)
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then
    (if (if false then true else true) then (\x5. true) else (\x4. false))
    else if (if false then true else false) then (\x3. x3) else (\x2. false))
     ((if false then (\x1. false) else (\x0. false))
        (if (if true then true else true) then
         (if false then false else true) else if false then true else true))) ;;

(if (if true then true else false) then (\x1. true) else (\x0. false))
  (if (if false then true else true) then (if false then true else false)
   else if false then true else true) ;;

(if (if true then false else false) then (\x1. x1) else (\x0. x0))
  (if false then (if false then false else true) else
   if true then false else true) ;;

(\x2. (\x3. x2) x2)
  ((if (if false then false else false) then (\x1. x1) else (\x0. true))
     (if true then (if false then false else false) else true)) ;;

(\x3.
   if (if x3 then false else x3) then (if false then false else false) else
   if false then x3 else true)
  ((\x2. false)
     (if (if true then false else true) then (\x1. false) else (\x0. x0))) ;;

(if (if true then false else true) then (\x1. x1) else (\x0. true))
  (if (if true then true else true) then (if true then false else false) else
   if true then true else true) ;;

if true then (if true then true else true) else if true then true else true ;;

\x0.
  (\x1. if false then x0 else x0)
    (if (if true then x0 else x0) then (if false then true else x0) else
     if x0 then true else true) ;;

\x0.
  if (if x0 then false else false) then (if false then x0 else false) else
  if true then false else false ;;

if (if false then true else true) then (if false then true else false) else
if true then true else true ;;

\x0.
  if (if x0 then false else false) then (if x0 then x0 else true) else
  if true then false else false ;;

(if
 (if (if false then true else false) then (if true then false else false)
  else if false then true else true)
 then (if (if true then true else false) then (\x5. false) else (\x4. x4))
 else if (if true then false else true) then (\x3. x3) else (\x2. true))
  ((if (if true then true else false) then (\x1. false) else (\x0. false))
     (if false then (if true then true else false) else
      if true then true else true)) ;;

(if
 (if (if false then true else true) then (if false then true else false) else
  if false then true else true)
 then (if (if true then false else false) then (\x5. true) else (\x4. true))
 else if (if false then false else true) then (\x3. true) else (\x2. x2))
  ((if (if true then true else false) then (\x1. false) else (\x0. false))
     (if false then (if true then true else false) else
      if true then true else true)) ;;

(if false then (\x1. x1) else (\x0. false))
  (if (if false then true else false) then (if false then false else true)
   else true) ;;

(\x0. \x1. x0)
  (if false then (if false then false else true) else
   if false then false else true) ;;

if
(\x8.
   if (if false then x8 else x8) then (if true then true else false) else
   if x8 then false else false)
  ((if (if false then true else false) then (\x7. true) else (\x6. false))
     (if true then (if false then false else false) else
      if true then true else false))
then
(\x5.
   if (if x5 then x5 else x5) then (if x5 then true else true) else
   if true then true else false)
  ((\x4. if x4 then false else true)
     (if (if true then false else false) then (if true then false else false)
      else if true then true else true))
else
(if
 (if (if false then false else false) then (if false then true else false)
  else true)
 then (if (if false then true else false) then (\x3. true) else (\x2. true))
 else if (if false then false else true) then (\x1. false) else (\x0. x0))
  (if
   (if (if false then true else false) then (if false then false else false)
    else if false then false else true)
   then
   (if (if false then false else true) then (if true then true else true)
    else if false then true else true)
   else
   if (if false then false else false) then (if false then false else false)
   else true) ;;

\x0.
  (if (if x0 then true else false) then (\x3. x3) else (\x2. true))
    ((\x1. if true then x0 else false)
       (if (if false then false else false) then
        (if false then false else false) else if true then true else x0)) ;;

(\x2.
   if (if x2 then true else true) then (if false then false else x2) else
   if x2 then false else false)
  ((if (if true then true else false) then (\x1. false) else (\x0. true))
     (if (if true then false else true) then (if true then false else true)
      else if false then true else true)) ;;

(if (if true then true else true) then (\x7. x7) else (\x6. x6))
  (\x5. if true then true else false)
  ((if (if (if true then false else false) then false else false) then
    (if (if true then false else true) then (\x4. true) else (\x3. true))
    else (\x2. if x2 then true else x2))
     ((if (if true then true else true) then (\x1. true) else (\x0. true))
        (if (if false then false else true) then
         (if true then false else false) else if true then true else true))) ;;

if (if true then true else true) then (if true then true else true) else
false ;;

if (if true then true else true) then (\x1. x1) else (\x0. true) ;;

if
(\x3. if true then true else true)
  (if false then (if false then true else true) else
   if true then true else false)
then
(if (if false then false else false) then (\x2. true) else (\x1. false))
  (if (if true then false else false) then (if false then false else false)
   else if false then true else true)
else
(\x0. if x0 then true else false)
  (if (if false then false else false) then true else true) ;;

if (if true then true else false) then true else if false then true else true ;;

\x0.
  (\x1. \x2. false)
    (if (if true then x0 else true) then (if x0 then x0 else x0) else
     if true then false else false) ;;

\x0.
  if (if x0 then false else x0) then (if false then false else true) else
  if false then x0 else true ;;

(\x2. \x3. x3)
  (if (if true then true else false) then (\x1. false) else (\x0. x0))
  (if
   (if (if true then true else false) then (if true then true else true) else
    true)
   then (if (if false then true else true) then true else true) else
   if (if true then false else false) then (if true then false else true)
   else if true then false else true) ;;

\x0.
  if (if true then x0 else true) then (if true then true else x0) else
  if true then false else false ;;

if
(if
 (if (if false then false else false) then false else
  if true then true else false)
 then (if (if true then false else false) then (\x14. x14) else (\x13. true))
 else if (if false then false else true) then (\x12. false) else (\x11. true))
  ((if (if true then false else true) then (\x10. x10) else (\x9. false))
     (if (if true then false else true) then (if false then false else false)
      else if false then true else false))
then
(if
 (if (if true then true else false) then (if false then false else true) else
  false)
 then (if (if true then false else true) then (\x8. x8) else (\x7. true))
 else if (if true then false else true) then (\x6. true) else (\x5. true))
  ((if false then (\x4. false) else (\x3. true))
     (if true then (if false then true else true) else
      if false then true else false))
else
(\x2.
   if (if true then true else true) then (if false then false else false)
   else if true then x2 else true)
  ((if (if true then true else true) then (\x1. false) else (\x0. false))
     (if (if false then false else false) then
      (if false then false else false) else if true then false else false)) ;;

if (if (if true then true else true) then false else true) then
(if (if true then false else false) then (if false then false else false)
 else if false then true else false)
else
if (if false then true else false) then (if false then false else true) else
if true then false else true ;;

(if
 (if (if false then true else true) then (if false then true else false) else
  if false then true else true)
 then (if (if true then false else false) then (\x4. true) else (\x3. true))
 else if (if false then false else true) then (\x2. true) else (\x1. x1))
  ((\x0. false)
     (if (if true then false else true) then (if false then true else false)
      else if false then true else false)) ;;

(\x4.
   (if (if true then x4 else true) then (\x6. true) else (\x5. true))
     (if (if true then true else false) then (if x4 then false else x4) else
      x4))
  ((\x2. \x3. true)
     (if (if true then true else true) then (if false then true else true)
      else if false then false else false)
     ((if (if false then false else false) then (\x1. x1) else (\x0. true))
        (if false then (if false then false else true) else
         if true then false else false))) ;;

\x0. if false then true else true ;;

if true then (if true then false else false) else
if true then false else false ;;

(if
 (if (if false then true else false) then (if true then false else false)
  else if false then false else true)
 then (\x9. if false then x9 else x9) else
 if false then (\x8. x8) else (\x7. x7))
  (\x6.
     if (if true then false else true) then x6 else if false then x6 else x6)
  ((if
    (if (if true then true else true) then true else
     if false then true else true)
    then (if (if false then true else true) then (\x5. false) else (\x4. x4))
    else if true then (\x3. x3) else (\x2. x2))
     ((if (if false then false else true) then (\x1. true) else (\x0. false))
        (if (if false then false else false) then
         (if true then false else false) else false))) ;;

if (if false then false else false) then (if false then false else false)
else false ;;

(\x2. \x3. x3) (if false then (if true then true else true) else true)
  ((if (if false then false else false) then (\x1. x1) else (\x0. true))
     (if (if true then false else true) then (if true then true else false)
      else if true then false else false)) ;;

(if false then (\x1. false) else (\x0. true))
  (if (if true then false else true) then (if false then true else false)
   else if false then true else true) ;;

(if
 (if (if true then false else true) then (if true then true else false) else
  if false then false else false)
 then (if (if true then false else false) then (\x5. true) else (\x4. true))
 else (\x3. if x3 then true else x3))
  ((if (if true then true else false) then (\x2. true) else (\x1. true))
     ((\x0. false) true)) ;;

if
(if (if false then true else true) then (if true then true else false) else
 if true then true else true)
then
(if (if false then true else false) then (if false then false else true) else
 if false then true else false)
else
if (if false then true else false) then (if false then false else true) else
if true then false else true ;;

(\x0. \x1. x0) (if false then false else true) ;;

(\x3.
   if false then (if false then false else false) else
   if false then x3 else true)
  ((if true then (\x2. false) else (\x1. true))
     (\x0. if x0 then false else false)) ;;

if
(\x3. if false then false else x3)
  (if (if true then true else false) then (if false then true else false)
   else if true then false else false)
then (\x1. (\x2. false) (if true then x1 else x1)) else
(\x0.
   if (if false then x0 else true) then (if false then x0 else true) else
   if x0 then false else x0) ;;

\x0.
  \x1.
    if (if false then x1 else x1) then (if x1 then true else true) else
    if x0 then x0 else true ;;

(if false then (\x1. false) else (\x0. false))
  (if (if false then false else false) then false else true) ;;

if true then (if false then true else true) else if false then true else true ;;

if (if true then true else true) then (if false then false else false) else
if false then true else false ;;

\x0.
  if
  (\x5. if true then true else x5)
    (if (if x0 then false else false) then (if x0 then x0 else true) else
     if false then x0 else false)
  then
  (if (if x0 then x0 else x0) then (\x4. x4) else (\x3. x3))
    (if (if x0 then true else x0) then (if x0 then false else false) else
     if x0 then false else false)
  else
  (if (if false then false else x0) then (\x2. true) else (\x1. true))
    (if (if true then true else x0) then (if x0 then x0 else false) else
     if true then false else false) ;;

if (if false then false else true) then (\x1. false) else (\x0. false) ;;

if (if true then false else true) then true else if true then true else true ;;

(\x8. \x9. if x9 then x9 else false)
  ((if (if false then true else true) then (\x7. true) else (\x6. x6))
     (if (if false then true else false) then (if false then false else true)
      else if false then true else true))
  ((if (if false then (if true then true else false) else true) then
    (if (if false then true else true) then (\x5. false) else (\x4. x4)) else
    if false then (\x3. false) else (\x2. true))
     ((if false then (\x1. x1) else (\x0. x0))
        (if (if true then true else true) then
         (if true then false else false) else if true then true else false))) ;;

(if (if false then false else true) then (\x1. false) else (\x0. false))
  (if (if false then false else false) then true else
   if true then true else true) ;;

if (if false then true else true) then (if true then false else false) else
if true then false else true ;;

(\x0. (\x1. x0) (if true then x0 else x0))
  (if
   (if (if true then true else false) then (if false then false else true)
    else false)
   then (if false then true else true) else
   if (if true then false else false) then (if false then true else true)
   else if true then true else true) ;;

(\x1.
   if (if x1 then true else false) then (if x1 then x1 else true) else
   if false then x1 else false)
  ((\x0. if true then true else true)
     (if (if false then false else true) then
      (if false then false else false) else if false then false else false)) ;;

(if (if true then false else false) then (\x4. x4) else (\x3. x3))
  (if (if true then false else false) then (\x2. true) else (\x1. x1))
  ((\x0. x0) (if true then false else if true then false else false)) ;;

if (if true then false else false) then false else
if false then true else false ;;

(if
 (if false then (\x9. x9) else (\x8. x8))
   (if (if false then true else false) then (if true then true else true)
    else if true then false else false)
 then
 (if
  (if (if true then true else true) then (if true then true else false) else
   if true then false else true)
  then
  (if (if false then false else false) then (\x7. true) else (\x6. true))
  else if (if false then false else false) then (\x5. true) else (\x4. false))
 else
 (\x3.
    if (if true then true else true) then (if true then false else true) else
    if true then x3 else true))
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if false then (\x1. true) else (\x0. x0))
        (if (if true then true else true) then false else
         if false then false else true))) ;;

if true then (if false then true else true) else
if false then true else false ;;

if (if false then false else true) then (if true then true else false) else
if false then false else false ;;

(if
 (if
  (if (if false then false else false) then (if true then false else false)
   else if true then false else true)
  then
  (if (if true then true else true) then (if false then false else false)
   else if false then true else true)
  else
  if (if true then true else false) then true else
  if false then false else false)
 then
 (\x9.
    if false then (if x9 then x9 else false) else
    if false then false else false)
 else
 if
 (if (if true then true else true) then false else
  if false then true else false)
 then (if (if true then true else true) then (\x8. true) else (\x7. x7)) else
 if (if false then false else false) then (\x6. true) else (\x5. x5))
  ((if
    (if (if true then true else true) then (if false then true else false)
     else if false then false else false)
    then
    (if (if true then true else true) then (\x4. true) else (\x3. false))
    else if false then (\x2. false) else (\x1. true))
     ((\x0. false)
        (if (if true then true else true) then true else
         if false then true else true))) ;;

(\x2. \x3. true)
  (if true then (if true then true else false) else
   if true then false else true)
  ((\x1. if false then false else true) (\x0. if x0 then true else false)) ;;

\x0. (\x2. if false then x0 else x2) (\x1. if false then false else x1) ;;

if (if false then false else true) then false else
if true then false else false ;;

(\x5.
   (\x6. if false then x6 else x6)
     (if (if false then false else true) then true else
      if false then x5 else true))
  (if
   (if (if true then false else false) then (\x4. false) else (\x3. false))
     (if true then (if false then false else false) else
      if false then false else false)
   then
   (\x2. if x2 then x2 else x2)
     (if (if true then false else false) then true else true)
   else
   (if true then (\x1. true) else (\x0. true))
     (if false then (if true then true else false) else false)) ;;

(\x2. \x3. x2)
  (if (if true then false else false) then (if true then true else false)
   else if true then true else false)
  ((if (if false then false else false) then (\x1. x1) else (\x0. true))
     (if false then (if true then false else true) else
      if false then true else false)) ;;

\x0.
  if (if x0 then x0 else true) then (if false then false else true) else
  if false then x0 else true ;;

if (if true then false else false) then (if false then false else false) else
if false then false else false ;;

if (if true then true else true) then (if true then true else false) else
if true then true else true ;;

(\x5. \x6. if x6 then x6 else false)
  (if (if true then false else false) then false else
   if true then true else true)
  (if
   (if (if false then false else false) then (\x4. x4) else (\x3. true))
     (if (if false then true else true) then (if true then false else false)
      else true)
   then
   (\x2. x2)
     (if (if false then false else false) then
      (if true then false else false) else if false then true else true)
   else
   (if true then (\x1. true) else (\x0. false))
     (if (if false then false else false) then (if true then true else true)
      else if false then true else true)) ;;

(if true then (\x1. true) else (\x0. false))
  (if (if false then true else false) then true else
   if false then false else false) ;;

if
(\x9.
   if (if true then false else false) then x9 else if false then true else x9)
  ((\x8. if false then x8 else x8)
     (if (if true then false else true) then (if true then true else true)
      else if true then true else true))
then
(if
 (if (if true then true else false) then (if false then false else false)
  else if true then true else false)
 then (if (if false then false else false) then (\x7. x7) else (\x6. true))
 else (\x5. if true then true else true))
  ((if (if false then true else true) then (\x4. true) else (\x3. x3))
     (if (if false then false else false) then
      (if false then true else false) else false))
else
(\x2.
   if (if true then true else true) then (if false then false else false)
   else if true then x2 else true)
  ((if (if true then true else true) then (\x1. false) else (\x0. false))
     (if (if false then false else false) then
      (if false then false else false) else if true then false else false)) ;;

(\x8. \x9. if x9 then x9 else x9)
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then (if (if false then true else true) then (\x7. x7) else (\x6. x6))
    else if (if false then true else false) then (\x5. true) else (\x4. x4))
     ((if (if false then false else true) then (\x3. false) else (\x2. false))
        (if true then (\x1. x1) else (\x0. true)))) ;;

if (if true then true else false) then false else if true then true else true ;;

(if (if true then true else true) then (\x1. x1) else (\x0. false))
  (if (if true then false else true) then (if false then true else false)
   else if false then true else true) ;;

(\x5. \x6. x6) (if false then (\x4. x4) else (\x3. x3))
  ((if (if false then false else false) then (\x2. true) else (\x1. true))
     (\x0. if x0 then true else x0)) ;;

if (if false then true else true) then true else if false then true else true ;;

if
(\x1. if x1 then false else x1)
  (if (if false then true else true) then true else
   if false then false else true)
then
(if (if true then false else false) then (if true then false else false) else
 if false then true else false)
else
(\x0. if x0 then true else false)
  (if (if false then false else false) then true else true) ;;

(if
 (if (if false then false else false) then (\x12. true) else (\x11. false))
   (\x10. if false then true else x10)
 then
 (\x9.
    if false then (if x9 then x9 else false) else
    if false then false else false)
 else
 if
 (if (if false then false else true) then (if true then true else true) else
  if true then true else false)
 then (\x8. if false then x8 else true) else (\x7. if true then x7 else true))
  ((if true then (\x6. x6) else (\x5. x5))
     (if true then (\x4. false) else (\x3. true))
     ((if (if false then false else true) then (\x2. true) else (\x1. false))
        (\x0. true))) ;;

(\x0. \x1. false)
  (if (if false then true else true) then false else
   if false then false else false) ;;

(if
 (if (if true then true else true) then true else
  if true then false else true)
 then (if (if true then true else false) then (\x3. false) else (\x2. x2))
 else (\x1. if true then false else x1))
  ((\x0. if x0 then true else true)
     (if (if false then true else true) then (if false then false else true)
      else if false then false else false)) ;;

(if
 (if (if false then false else true) then (if false then true else true) else
  true)
 then (if (if false then false else false) then (\x8. false) else (\x7. x7))
 else if true then (\x6. true) else (\x5. false))
  ((if (if false then (if true then true else false) else true) then
    (if false then (\x4. true) else (\x3. true)) else
    if (if true then true else true) then (\x2. true) else (\x1. false))
     ((\x0. if true then true else x0)
        (if (if true then true else false) then
         (if true then false else false) else if true then true else false))) ;;

(if
 (if (if false then false else true) then (if false then true else false)
  else if true then false else true)
 then (if (if true then false else false) then (\x11. x11) else (\x10. x10))
 else if (if false then true else false) then (\x9. x9) else (\x8. x8))
  ((\x6. \x7. x7)
     (if (if false then false else true) then
      (if false then false else false) else if true then false else false))
  ((if (if true then true else true) then (\x5. x5) else (\x4. x4))
     (if true then (\x3. false) else (\x2. true))
     ((\x1. true) (\x0. if true then false else false))) ;;

(if (\x9. x9) (if true then false else true) then
 (if (if false then false else false) then (\x8. x8) else (\x7. x7)) else
 if (if true then true else true) then (\x6. x6) else (\x5. x5))
  ((\x3. \x4. x4) ((\x2. x2) (if false then true else false)))
  ((if true then (\x1. false) else (\x0. false))
     (if (if true then false else true) then (if false then true else false)
      else if true then false else false)) ;;

(if (if true then false else true) then (\x1. true) else (\x0. x0))
  (if (if true then false else true) then true else
   if false then false else true) ;;

(if (if true then false else true) then (\x8. x8) else (\x7. x7))
  (\x6. if x6 then true else false)
  ((if (\x5. true) (\x4. true) then (\x3. if true then true else x3) else
    (\x2. if x2 then true else x2))
     ((if (if true then false else true) then (\x1. x1) else (\x0. x0))
        (if true then false else if true then true else false))) ;;

\x0.
  if (if true then false else true) then (if false then true else x0) else
  if true then false else false ;;

if true then true else if true then false else true ;;

if true then (if false then false else false) else
if true then true else false ;;

\x0.
  (if (if x0 then false else false) then (\x2. x0) else (\x1. x0))
    (if (if true then x0 else true) then (if x0 then x0 else x0) else
     if true then false else false) ;;

(\x0. if true then false else x0)
  (if (if false then true else true) then (if true then false else false)
   else if false then true else false) ;;

(if
 (if
  (if (if false then false else false) then (if true then false else false)
   else if true then false else true)
  then
  (if (if true then true else true) then (if false then false else false)
   else if false then true else true)
  else
  if (if true then true else false) then true else
  if false then false else false)
 then
 (if
  (if (if false then true else false) then (if true then false else false)
   else if false then false else false)
  then (if (if false then true else true) then (\x9. true) else (\x8. x8))
  else if (if false then false else true) then (\x7. false) else (\x6. x6))
 else
 if
 (if (if false then false else true) then (if true then true else true) else
  if true then true else false)
 then (\x5. if true then false else false) else
 if (if false then false else false) then (\x4. x4) else (\x3. x3))
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if false then (\x1. true) else (\x0. x0))
        (if (if true then true else true) then false else
         if false then false else true))) ;;

(if (if true then false else true) then (\x1. x1) else (\x0. x0))
  (if (if true then true else false) then false else
   if true then true else true) ;;

(\x3. \x4. false) ((\x2. false) (if false then false else false))
  ((if (if true then true else false) then (\x1. false) else (\x0. x0))
     (if true then false else if true then false else false)) ;;

(if (if true then true else true) then (\x1. x1) else (\x0. x0))
  (if false then (if false then true else false) else
   if false then false else false) ;;

(\x1.
   if false then (if false then false else false) else
   if false then x1 else true)
  ((\x0. false)
     (if (if true then false else false) then (if true then true else false)
      else if false then true else false)) ;;

(if
 (if (if true then false else true) then (if true then true else false) else
  if false then false else false)
 then (if (if true then true else false) then (\x4. false) else (\x3. x3))
 else (\x2. if x2 then true else x2))
  ((if (if false then true else false) then (\x1. true) else (\x0. true))
     (if (if true then true else true) then (if false then false else true)
      else false)) ;;

(\x8. (\x9. true) (if true then x8 else false))
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then (if (if false then true else true) then (\x7. x7) else (\x6. x6))
    else if (if false then true else false) then (\x5. true) else (\x4. x4))
     ((if (if false then false else true) then (\x3. false) else (\x2. false))
        (if true then (\x1. x1) else (\x0. true)))) ;;

if true then (if false then true else false) else false ;;

\x0.
  (if (if x0 then true else false) then (\x2. x2) else (\x1. false))
    (if
     (if (if false then x0 else false) then (if x0 then true else x0) else
      if x0 then false else x0)
     then
     (if (if true then true else false) then (if false then x0 else false)
      else if false then x0 else false)
     else
     if x0 then (if true then true else false) else
     if x0 then true else false) ;;

if
(if (if true then true else true) then (\x5. false) else (\x4. x4))
  (if false then false else false)
then
(if (if false then false else false) then (\x3. true) else (\x2. false))
  (if (if true then false else false) then (if false then false else false)
   else if false then true else true)
else
(if (if false then false else true) then (\x1. false) else (\x0. true))
  (if (if false then true else true) then (if false then true else true) else
   false) ;;

(if (if false then true else true) then (\x5. x5) else (\x4. x4))
  (if true then (\x3. x3) else (\x2. false))
  ((if (if true then true else false) then (\x1. false) else (\x0. false))
     (if (if true then true else true) then false else
      if true then false else false)) ;;

\x0.
  if (if x0 then false else false) then (if x0 then x0 else false) else
  if true then false else false ;;

(\x0. \x1. true)
  (if (if true then true else false) then (if true then false else false)
   else if true then false else true) ;;

(if (if true then true else false) then (\x1. false) else (\x0. false))
  (if (if false then true else true) then (if true then false else false)
   else if false then true else false) ;;

(if (if false then true else true) then (\x1. x1) else (\x0. true))
  (if (if true then true else true) then (if false then false else false)
   else if true then false else true) ;;

(if (if true then false else false) then (\x1. true) else (\x0. false))
  (if false then (if false then false else true) else
   if true then false else true) ;;

if false then (if true then false else false) else
if false then true else false ;;

(\x0. if x0 then x0 else false)
  (if (if true then false else true) then (if false then true else false)
   else if true then true else true) ;;

\x0.
  if (if false then x0 else x0) then (if false then false else true) else
  if false then false else false ;;

if false then (\x1. x1) else (\x0. x0) ;;

if true then (if false then true else true) else false ;;

\x0.
  (if
   (if false then (if true then true else x0) else
    if false then true else true)
   then (\x5. if x5 then x0 else true) else
   if x0 then (\x4. x4) else (\x3. false))
    ((if (if true then true else true) then (\x2. false) else (\x1. true))
       (if (if false then false else false) then
        (if false then false else false) else if true then true else x0)) ;;

(if (if false then true else true) then (\x4. x4) else (\x3. x3))
  (\x2. if true then true else false)
  ((if (if false then false else false) then (\x1. true) else (\x0. false))
     (if true then (if true then true else false) else
      if false then true else true)) ;;

\x0.
  \x1.
    if (if true then false else true) then (if x1 then false else true) else
    if false then false else x1 ;;

(if
 (if (if true then false else true) then (if true then true else false) else
  if false then false else false)
 then (if (if true then true else false) then (\x3. true) else (\x2. true))
 else (\x1. if true then false else x1))
  ((\x0. if true then x0 else x0)
     (if (if false then false else true) then (if true then false else true)
      else if true then true else false)) ;;

if
(\x6. if (if x6 then false else x6) then x6 else if x6 then false else false)
  (if (if false then false else true) then (if true then true else true) else
   if true then false else false)
then
(\x5. if false then true else true)
  (\x4.
     if (if x4 then x4 else false) then (if false then true else x4) else
     if x4 then false else x4)
else
(if
 (if (if false then false else false) then (if false then true else false)
  else true)
 then (if (if false then true else false) then (\x3. true) else (\x2. true))
 else if (if false then false else true) then (\x1. false) else (\x0. x0))
  (if
   (if (if false then true else false) then (if false then false else false)
    else if false then false else true)
   then
   (if (if false then false else true) then (if true then true else true)
    else if false then true else true)
   else
   if (if false then false else false) then (if false then false else false)
   else true) ;;

\x0.
  if (if false then true else true) then (if x0 then true else x0) else
  if true then true else true ;;

if (if false then true else false) then (if true then false else true) else
if false then false else true ;;

if (if false then true else true) then (if false then false else true) else
true ;;

if (if false then false else false) then true else
if true then true else true ;;

\x0.
  \x1.
    if (if false then false else true) then (if x1 then x1 else x1) else
    if x0 then x0 else true ;;

if (if true then false else true) then (if false then false else true) else
if true then false else false ;;

\x0.
  (\x2. x2) (\x1. true)
    (if (if x0 then x0 else false) then (if true then true else true) else
     if x0 then x0 else false) ;;

(\x0. x0) (if true then false else true) ;;

\x0.
  (if (if true then false else x0) then (\x3. x0) else (\x2. true))
    (\x1.
       if (if false then x1 else true) then (if false then true else true)
       else if x0 then false else false) ;;

\x0.
  (\x1. \x2. x2)
    (if (if false then true else false) then (if false then true else x0)
     else if x0 then x0 else false) ;;

if (if true then true else true) then (if true then true else false) else
if true then true else false ;;

(\x0. if false then x0 else x0)
  (if (if true then true else true) then (if false then false else false)
   else if false then false else false) ;;

if (if false then true else true) then (if false then true else false) else
if false then false else false ;;

(\x0. if false then false else false)
  (if (if true then true else true) then false else
   if false then false else false) ;;

(if (if true then false else false) then (\x1. x1) else (\x0. false))
  (if (if true then true else true) then (if false then false else false)
   else if true then true else true) ;;

(\x2.
   if (if x2 then false else false) then (if true then x2 else true) else
   if x2 then false else false)
  ((if (if false then false else true) then (\x1. false) else (\x0. true))
     (if (if true then true else true) then (if true then true else false)
      else if true then true else false)) ;;

(\x1. \x2. x2)
  (if (if false then false else false) then (if true then true else false)
   else true)
  ((\x0. if x0 then x0 else true)
     (if false then true else if true then false else false)) ;;

(\x1.
   if false then (if false then false else x1) else if true then x1 else true)
  ((\x0. x0)
     (if (if false then false else true) then (if true then true else false)
      else if false then true else true)) ;;

if (if false then true else true) then true else
if false then false else false ;;

if
(if (if false then false else true) then (if true then false else true) else
 if true then true else true)
then
(if (if true then false else true) then (if true then true else true) else
 if false then false else true)
else
if false then (if false then false else false) else
if false then true else false ;;

(if
 (if (if false then true else false) then (if true then false else false)
  else if false then true else true)
 then (if false then (\x3. true) else (\x2. true)) else
 if (if false then true else false) then (\x1. true) else (\x0. x0))
  (if
   (if (if true then true else false) then (if false then false else true)
    else false)
   then (if false then true else true) else
   if (if true then false else false) then (if false then true else true)
   else if true then true else true) ;;

(if (if true then false else true) then (\x3. x3) else (\x2. x2))
  (if (if false then true else false) then (\x1. x1) else (\x0. true)) ;;

(if (if false then (if true then true else true) else true) then
 (if false then (\x3. x3) else (\x2. false)) else
 (\x1. if true then false else x1))
  ((\x0. x0) (if true then true else if true then true else false)) ;;

(\x3. \x4. x4)
  (if false then (if true then true else false) else
   if false then true else false)
  ((\x2.
      if (if true then x2 else x2) then (if x2 then x2 else x2) else
      if false then false else true)
     ((if (if true then true else true) then (\x1. false) else (\x0. true))
        (if (if true then true else false) then
         (if false then false else true) else if false then false else true))) ;;

\x0.
  (\x1. if false then x0 else x0)
    (if (if true then x0 else x0) then (if x0 then x0 else x0) else
     if true then true else x0) ;;

\x0.
  (if (if x0 then true else false) then (\x3. x3) else (\x2. true))
    ((\x1. if x0 then x0 else true)
       (if (if x0 then x0 else false) then (if false then x0 else true) else
        if x0 then false else true)) ;;

if false then (if true then false else true) else
if true then false else true ;;

if (if false then true else false) then (if false then true else false) else
if false then false else false ;;

if (if false then true else true) then (if false then true else true) else
if true then true else true ;;

\x0. (\x1. false) (if true then true else true) ;;

(if (if true then true else true) then (\x1. x1) else (\x0. true))
  (if (if false then false else false) then (if false then false else true)
   else true) ;;

\x0. (\x1. x0) (if false then false else x0) ;;

(if (if true then true else false) then (\x1. true) else (\x0. false))
  (if (if false then true else false) then (if false then true else true)
   else if false then false else true) ;;

if (if true then true else true) then false else if true then true else true ;;

if (if true then true else false) then (\x1. false) else (\x0. false) ;;

(if (if true then false else false) then (\x1. x1) else (\x0. true))
  (if (if true then false else true) then (if false then true else false)
   else if false then true else true) ;;

(\x2. \x3. if true then true else x3)
  ((if true then (\x1. false) else (\x0. false))
     (if true then true else if true then true else false)) ;;

(\x3.
   (if (if x3 then x3 else x3) then (\x6. x3) else (\x5. false))
     (\x4. if false then true else x3))
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if false then (\x1. true) else (\x0. x0))
        (if (if true then true else true) then false else
         if false then false else true))) ;;

\x0. \x1. (\x2. false) true ;;

if (if false then false else false) then (if false then false else false)
else if false then true else false ;;

\x0.
  if (if true then false else false) then (if false then true else x0) else
  if true then true else true ;;

(\x1.
   if (if true then x1 else false) then (if x1 then false else x1) else
   if x1 then true else true)
  ((\x0. if x0 then true else false)
     (if (if true then false else false) then (if false then false else true)
      else true)) ;;

(if (if true then false else true) then (\x1. true) else (\x0. x0))
  (if false then (if false then true else false) else
   if false then false else false) ;;

\x0.
  \x1.
    if (if x1 then false else x0) then (if x0 then true else true) else
    if x0 then x0 else false ;;

(if
 (if (if false then false else false) then (if false then false else false)
  else if true then false else true)
 then
 (if (if false then true else false) then (\x7. false) else (\x6. false))
 else (\x5. if true then true else x5))
  (if
   (if (if false then false else false) then (\x4. x4) else (\x3. true))
     (if (if false then true else true) then (if true then false else false)
      else true)
   then
   (\x2. x2)
     (if (if false then false else false) then
      (if true then false else false) else if false then true else true)
   else
   (if true then (\x1. true) else (\x0. false))
     (if (if false then false else false) then (if true then true else true)
      else if false then true else true)) ;;

\x0.
  (if (if x0 then false else x0) then (\x2. x2) else (\x1. false))
    (if true then x0 else false) ;;

if (if false then false else true) then true else
if true then false else true ;;

(\x3. \x4. x4) (if false then (\x2. x2) else (\x1. x1))
  ((\x0. false) (if (if false then true else true) then false else true)) ;;

(if (if false then true else true) then (\x1. x1) else (\x0. true))
  (if (if false then false else true) then (if false then true else false)
   else if false then true else true) ;;

if (if true then true else false) then true else true ;;

if (if false then false else true) then (if true then false else true) else
if true then true else false ;;

(\x0. if false then true else true)
  (if false then (if false then false else true) else
   if true then false else true) ;;

(if (if false then false else false) then (\x2. x2) else (\x1. false))
  ((\x0. if true then x0 else false)
     (if (if true then false else true) then (if true then false else true)
      else true)) ;;

if (if true then true else true) then (if true then true else false) else
if true then false else false ;;

if false then (if false then true else false) else
if false then false else true ;;

(\x2.
   if (if x2 then true else true) then (if false then x2 else x2) else
   if x2 then true else true)
  ((if false then (\x1. false) else (\x0. false))
     (if (if true then false else true) then (if false then false else true)
      else if false then false else false)) ;;

(\x0. if false then false else false)
  (if (if false then true else true) then (if false then true else false)
   else if false then true else false) ;;

(if
 (if (if false then true else false) then (if false then true else false)
  else if false then false else true)
 then (if false then (\x4. x4) else (\x3. false)) else
 if (if false then true else true) then (\x2. false) else (\x1. true))
  ((\x0. if x0 then x0 else true)
     (if true then false else if true then false else false)) ;;

(\x2. \x3. x3)
  (if (if true then true else false) then false else
   if true then true else false)
  ((if (if true then true else false) then (\x1. false) else (\x0. true))
     (if (if false then false else false) then (if true then true else false)
      else false)) ;;

(\x2. \x3. x3)
  (if (if true then false else false) then false else
   if true then true else false)
  ((if (if true then true else false) then (\x1. false) else (\x0. false))
     (if false then (if true then true else false) else
      if true then true else true)) ;;

(if (if true then false else false) then (\x1. false) else (\x0. false))
  (if true then (if false then false else true) else
   if true then false else true) ;;

(\x0. if x0 then x0 else true)
  (if (if true then true else false) then (if true then false else true) else
   if false then true else false) ;;

if true then (if false then true else false) else if true then true else true ;;

(\x0. true) (if true then false else true) ;;

(\x2. \x3. if true then true else x3)
  ((if (if true then false else false) then (\x1. true) else (\x0. false))
     (if (if true then true else false) then (if false then false else true)
      else true)) ;;

(if (if true then true else true) then (\x3. x3) else (\x2. x2))
  (if (if false then false else false) then (\x1. true) else (\x0. true)) ;;

(\x5.
   (if (if x5 then x5 else x5) then (\x7. false) else (\x6. x6))
     (if (if true then false else x5) then (if x5 then x5 else true) else
      if true then false else true))
  ((if (if false then true else false) then (\x4. x4) else (\x3. x3))
     (if (if false then true else false) then (\x2. false) else (\x1. x1))
     ((\x0. if x0 then x0 else x0)
        (if (if false then true else true) then false else
         if false then false else true))) ;;

(if
 (if (if true then false else true) then (if true then false else false) else
  if true then false else false)
 then (if (if true then false else false) then (\x5. false) else (\x4. x4))
 else if false then (\x3. false) else (\x2. false))
  ((if (if false then false else true) then (\x1. false) else (\x0. true))
     (if (if false then true else true) then (if false then false else true)
      else if false then false else false)) ;;

if (if true then false else true) then (\x1. false) else (\x0. false) ;;

\x0.
  (if (if false then true else x0) then (\x2. false) else (\x1. x0))
    (if (if true then false else false) then (if true then true else false)
     else if true then true else x0) ;;

(\x2.
   if (if true then x2 else false) then (if x2 then false else x2) else
   if x2 then false else false)
  ((if (if true then false else false) then (\x1. true) else (\x0. true))
     (if (if true then false else false) then false else false)) ;;

if (if false then false else true) then false else true ;;

if (if false then false else true) then (if false then false else true) else
if false then true else false ;;

(\x0.
   if (if x0 then false else false) then (if true then x0 else true) else
   if x0 then false else false)
  (if false then false else if false then true else true) ;;

if (if false then false else true) then (if true then true else false) else
if false then false else true ;;

\x0.
  (\x1. false)
    (if (if x0 then false else false) then (if false then false else x0) else
     if true then false else false) ;;

(if
 (if (if true then false else true) then (if false then false else false)
  else if false then false else true)
 then (if (if true then true else false) then (\x5. false) else (\x4. x4))
 else if false then (\x3. x3) else (\x2. x2))
  ((if (if true then false else true) then (\x1. x1) else (\x0. false))
     (if (if true then false else true) then (if false then true else false)
      else if false then true else false)) ;;

if (if (if false then false else true) then true else true) then
(if (if true then false else false) then (if false then false else false)
 else if false then true else false)
else if (if false then true else false) then false else false ;;

(\x1.
   if true then (if x1 then false else x1) else if false then x1 else false)
  ((\x0. false)
     (if (if true then false else true) then (if false then true else false)
      else if false then true else false)) ;;

if (if false then false else false) then (if true then true else true) else
false ;;

\x0.
  if (if false then true else true) then (if x0 then true else true) else
  if false then true else false ;;

if (if false then true else true) then (if false then true else false) else
if true then false else true ;;

(if (if false then true else false) then (\x2. x2) else (\x1. x1))
  (\x0. if x0 then x0 else true) ;;

(\x1.
   if (if x1 then false else x1) then (if true then true else false) else
   if true then x1 else true)
  ((\x0. if true then x0 else false)
     (if (if true then false else true) then (if true then false else true)
      else true)) ;;

\x0.
  if (if x0 then false else false) then (if x0 then true else true) else
  if true then true else false ;;

if (if false then true else false) then false else
if false then true else false ;;

if true then (if false then false else true) else if true then true else true ;;

(if
 (if (if true then false else true) then (if false then false else false)
  else if false then false else true)
 then (if (if true then true else false) then (\x4. false) else (\x3. x3))
 else if false then (\x2. x2) else (\x1. x1))
  ((\x0. if false then x0 else x0)
     (if true then true else if false then true else true)) ;;

(if (if false then false else true) then (\x1. true) else (\x0. false))
  (if (if true then false else true) then (if false then false else false)
   else if false then true else true) ;;

(if (if false then false else true) then (\x1. false) else (\x0. true))
  (if (if true then true else false) then (if true then false else false)
   else if true then false else true) ;;

if (if true then true else false) then (if false then true else false) else
if false then false else false ;;

(\x2. (\x3. x2) (if false then false else true))
  (\x0.
     (\x1. if x0 then false else false)
       (if (if x0 then true else x0) then (if false then false else x0) else
        x0)) ;;

if
(\x11. \x12. true) ((\x10. false) (if true then true else true))
  ((\x9. if false then x9 else true)
     (if (if false then true else false) then false else
      if true then false else false))
then
(if
 (if (if true then true else false) then (if false then false else true) else
  false)
 then (if (if true then false else true) then (\x8. x8) else (\x7. true))
 else if (if true then false else true) then (\x6. true) else (\x5. true))
  ((if false then (\x4. false) else (\x3. true))
     (if true then (if false then true else true) else
      if false then true else false))
else
(if true then (\x2. x2) else (\x1. false))
  ((\x0. if false then false else true)
     (if false then (if true then true else false) else
      if false then false else true)) ;;

\x0. \x1. (\x2. true) (if x1 then false else false) ;;

(\x0. \x1. x1)
  (if (if false then false else true) then (if false then false else false)
   else if false then false else true) ;;

if (if true then true else true) then (if false then true else true) else
false ;;

\x0.
  (\x3. (\x4. true) (if true then x3 else true))
    ((if (if true then true else true) then (\x2. false) else (\x1. true))
       (if (if false then false else false) then
        (if false then false else false) else if true then true else x0)) ;;

\x0.
  (\x1. \x2. x2)
    (if (if true then x0 else true) then (if false then true else x0) else
     if true then false else false) ;;

(if (if false then true else false) then (\x1. x1) else (\x0. x0))
  (if (if false then true else true) then (if false then true else false)
   else if false then true else true) ;;

\x0. (\x1. if x1 then false else true) x0 ;;

(if
 (if (if true then true else true) then true else
  if true then false else true)
 then (if (if false then true else true) then (\x5. x5) else (\x4. true))
 else if false then (\x3. false) else (\x2. false))
  ((if (if true then false else false) then (\x1. true) else (\x0. true))
     (if (if true then false else false) then false else false)) ;;

(\x0. if true then false else x0)
  (if (if false then false else false) then true else
   if false then true else false) ;;

if (if true then true else false) then true else
if false then false else false ;;

\x0. if false then false else x0 ;;

if (if true then true else true) then (\x1. false) else (\x0. false) ;;

(if (if false then false else false) then (\x1. x1) else (\x0. false))
  (if (if false then true else false) then false else
   if true then true else true) ;;

(\x5. \x6. if false then x5 else false)
  ((if (if false then true else true) then (\x4. false) else (\x3. true))
     (if (if false then true else false) then (if true then false else false)
      else if false then true else false))
  ((\x2.
      if (if x2 then true else true) then (if x2 then x2 else x2) else
      if x2 then false else true)
     ((if (if true then false else true) then (\x1. x1) else (\x0. false))
        (if (if true then false else false) then true else
         if true then true else false))) ;;

(\x5. (\x6. x6) (if x5 then true else x5))
  ((if (if false then true else false) then (\x4. x4) else (\x3. x3))
     (if (if false then true else false) then (\x2. false) else (\x1. x1))
     ((\x0. if false then true else true)
        (if (if true then true else false) then false else
         if false then false else true))) ;;

(\x0. true) (if false then false else false) ;;

(if (if true then false else false) then (\x1. false) else (\x0. false))
  (if (if false then false else false) then true else
   if true then true else true) ;;

if
(if (if false then true else true) then (if true then true else false) else
 if true then true else true)
then
(if (if true then true else false) then (if false then false else false) else
 if false then true else true)
else
if false then (if false then false else false) else
if false then true else false ;;

(if (if true then false else true) then (\x1. false) else (\x0. false))
  (if true then true else true) ;;

(if (if false then true else false) then (\x3. false) else (\x2. false))
  ((if (if true then true else false) then (\x1. false) else (\x0. false))
     (if false then (if true then true else false) else
      if true then true else true)) ;;

(if
 (if false then (\x11. x11) else (\x10. x10))
   (if (if false then true else false) then (if true then true else true)
    else if true then false else false)
 then
 (if
  (if (if true then true else true) then (if true then true else false) else
   if true then false else true)
  then
  (if (if false then false else false) then (\x9. true) else (\x8. true))
  else if (if false then false else false) then (\x7. true) else (\x6. false))
 else
 (\x5.
    if (if true then true else true) then (if true then false else true) else
    if true then x5 else true))
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then
    (if (if true then true else true) then (\x4. false) else (\x3. true))
    else if (if true then true else true) then (\x2. true) else (\x1. false))
     (if
      (if (if true then true else false) then false else
       if false then true else true)
      then (\x0. true) (if true then true else true) else
      if (if false then true else true) then false else
      if true then false else true)) ;;

if (if true then false else false) then true else
if false then false else true ;;

(if
 (if (if false then false else true) then (if false then true else false)
  else if true then false else true)
 then (if (if true then false else false) then (\x11. x11) else (\x10. x10))
 else if (if false then true else false) then (\x9. x9) else (\x8. x8))
  ((\x6. \x7. x7)
     (if (if false then false else true) then
      (if false then false else false) else if true then false else false))
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. x2))
     ((if (if false then false else true) then (\x1. true) else (\x0. false))
        (if (if false then false else false) then
         (if true then false else false) else false))) ;;

(\x0. if true then true else false)
  (if (if false then false else true) then (if false then true else false)
   else if false then true else true) ;;

\x0. (\x1. true) (if x0 then x0 else false) ;;

if (if false then false else false) then (if false then true else false) else
if false then true else false ;;

if (if false then false else false) then (if false then true else true) else
if false then false else true ;;

(if false then (\x5. x5) else (\x4. x4))
  (if (if true then false else true) then (\x3. false) else (\x2. false))
  ((if (if true then true else false) then (\x1. x1) else (\x0. x0))
     (if (if true then false else true) then (if false then true else true)
      else true)) ;;

(\x2. \x3. true)
  ((if (if true then false else false) then (\x1. false) else (\x0. x0))
     (if true then (if false then false else true) else
      if false then true else true)) ;;

if
(if
 (if (if true then true else true) then true else
  if false then true else true)
 then
 (if true then (if false then false else true) else
  if true then false else false)
 else
 if (if true then false else true) then (if true then false else true) else
 if true then false else true)
then
(if (if false then false else true) then (\x3. false) else (\x2. true))
  (if true then (if true then true else false) else
   if true then false else false)
else
(if (if false then true else false) then (\x1. true) else (\x0. false))
  (if (if true then true else true) then (if true then true else false) else
   true) ;;

(if (if false then false else true) then (\x1. false) else (\x0. true))
  (if false then (if false then true else false) else
   if true then false else true) ;;

(\x2. if false then false else true)
  ((if (if true then true else false) then (\x1. x1) else (\x0. false))
     (if (if false then true else false) then true else
      if false then true else false)) ;;

\x0. if true then true else x0 ;;

(if true then (\x1. x1) else (\x0. x0))
  (if (if true then true else false) then false else
   if true then true else true) ;;

(\x2.
   if false then (if false then false else false) else
   if true then x2 else true)
  ((if (if false then false else true) then (\x1. false) else (\x0. true))
     (if (if true then true else true) then (if true then true else false)
      else if true then true else false)) ;;

(\x0. if x0 then x0 else x0)
  (if (if false then false else false) then true else
   if true then true else true) ;;

(if (if true then false else false) then (\x1. true) else (\x0. false))
  (if true then (if false then true else true) else true) ;;

(\x2.
   if (if x2 then false else false) then (if true then x2 else true) else
   if x2 then false else false)
  ((if (if false then false else false) then (\x1. x1) else (\x0. true))
     (if true then (if false then false else false) else true)) ;;

(\x5.
   (if (if x5 then x5 else x5) then (\x7. x5) else (\x6. true))
     (if (if false then false else true) then (if true then x5 else x5) else
      if x5 then false else false))
  ((if
    (if (if true then true else true) then (if false then true else false)
     else if false then false else false)
    then
    (if (if true then true else true) then (\x4. true) else (\x3. false))
    else if false then (\x2. false) else (\x1. true))
     ((\x0. false)
        (if (if true then true else true) then true else
         if false then true else true))) ;;

if (if true then true else true) then (if false then false else true) else
true ;;

(\x2. \x3. false)
  (if (if true then true else true) then true else
   if false then false else true)
  ((if (if true then false else true) then (\x1. false) else (\x0. true))
     (if (if false then true else true) then (if true then false else true)
      else if false then true else false)) ;;

(\x1.
   if false then (if false then false else false) else
   if false then x1 else true)
  ((\x0. if false then true else x0)
     (if false then (if true then false else true) else
      if false then true else false)) ;;

(if (if true then true else true) then (\x1. true) else (\x0. x0))
  (if false then (if false then true else true) else
   if false then false else false) ;;

(if
 (if (if true then false else true) then (if true then true else false) else
  if false then false else false)
 then (if (if true then false else false) then (\x3. true) else (\x2. true))
 else (\x1. if x1 then true else x1))
  ((\x0. if x0 then true else false)
     (if (if false then true else false) then (if false then true else false)
      else if true then true else false)) ;;

(if (if false then true else false) then (\x1. x1) else (\x0. x0))
  (if (if true then false else true) then (if false then false else false)
   else if true then true else true) ;;

if (if true then true else true) then (if true then false else true) else
if true then true else true ;;

if (if true then true else false) then (if false then false else false) else
if false then true else true ;;

\x0.
  (\x2. \x3. x0)
    (if (if x0 then false else x0) then (if x0 then false else true) else
     if true then x0 else x0)
    ((\x1. x1) (if true then x0 else true)) ;;

(if
 (if (if false then true else true) then (if false then false else false)
  else if true then true else false)
 then (if true then (\x9. true) else (\x8. x8)) else
 if (if false then true else false) then (\x7. true) else (\x6. true))
  (if
   (if (if true then false else false) then (\x5. false) else (\x4. false))
     (if true then (if false then false else false) else
      if false then false else false)
   then
   (if (if false then false else true) then (\x3. true) else (\x2. x2))
     (if (if false then false else true) then (if true then false else false)
      else false)
   else
   (if true then (\x1. true) else (\x0. true))
     (if false then (if true then true else false) else false)) ;;

(\x0. if true then false else x0)
  (if false then (if false then false else false) else
   if true then false else true) ;;

(\x0. false) (if true then false else true) ;;

(if
 (\x7. if true then true else x7)
   (if false then (if true then true else true) else
    if true then false else true)
 then
 (\x6.
    if false then (if x6 then x6 else false) else
    if false then false else false)
 else
 (\x5.
    if (if true then true else true) then (if true then false else true) else
    if true then x5 else true))
  ((\x4. x4)
     (if (if true then false else true) then (\x3. true) else (\x2. true))
     ((if false then (\x1. false) else (\x0. false))
        (if (if true then true else true) then
         (if false then false else true) else if false then true else true))) ;;

(if
 (if (if false then true else true) then (if false then true else false) else
  if false then true else true)
 then (if (if false then true else true) then (\x4. x4) else (\x3. true))
 else if (if false then true else false) then (\x2. true) else (\x1. x1))
  ((\x0. if x0 then x0 else true)
     (if true then (if false then false else false) else
      if false then false else false)) ;;

(\x4. (\x5. x5) (if x4 then true else x4))
  (if
   (if (if false then true else true) then (\x3. true) else (\x2. true))
     (if (if true then false else false) then (if false then false else true)
      else if true then false else true)
   then
   (if (if true then true else false) then (\x1. false) else (\x0. true))
     (if (if false then false else true) then (if true then false else false)
      else if true then false else true)
   else
   if (if (if true then true else false) then false else true) then
   (if (if false then false else false) then (if true then false else false)
    else if true then true else false)
   else
   if (if true then true else false) then (if false then true else false)
   else false) ;;

(if (if true then false else true) then (\x3. true) else (\x2. false))
  (if false then (\x1. x1) else (\x0. true)) ;;

(\x6.
   (if (if true then false else false) then (\x8. x8) else (\x7. true))
     (if (if true then true else true) then (if x6 then true else false) else
      if true then x6 else false))
  ((if (if false then (if true then true else false) else true) then
    (if (if false then true else true) then (\x5. false) else (\x4. x4)) else
    if false then (\x3. false) else (\x2. true))
     ((if false then (\x1. x1) else (\x0. x0))
        (if (if true then true else true) then
         (if true then false else false) else if true then true else false))) ;;

(\x0. if x0 then x0 else false)
  (if (if true then false else true) then (if false then false else false)
   else if false then true else true) ;;

(\x3.
   if true then (if x3 then false else x3) else if false then x3 else false)
  ((\x2. false)
     (if (if true then false else true) then (\x1. false) else (\x0. x0))) ;;

(\x5. \x6. if x6 then x6 else false)
  ((if (if false then true else true) then (\x4. true) else (\x3. x3))
     (if (if false then true else false) then (if false then false else true)
      else if false then true else true))
  ((\x2.
      if (if true then false else x2) then (if x2 then false else false) else
      if x2 then true else x2)
     ((if (if false then false else false) then (\x1. x1) else (\x0. true))
        (if false then (if false then false else true) else
         if true then false else false))) ;;

\x0.
  \x1.
    (if (if x0 then x0 else x1) then (\x3. x3) else (\x2. x2))
      (if (if x0 then true else x1) then (if x1 then x1 else x1) else
       if false then x0 else x0) ;;

(if (if false then true else false) then (\x1. true) else (\x0. false))
  (if (if true then true else true) then false else
   if false then false else false) ;;

if (if false then (if false then true else false) else false) then
(if (if true then false else false) then (if false then false else false)
 else if false then true else false)
else
if (if false then false else false) then (if false then true else false) else
if false then false else false ;;

\x0.
  if (\x8. x8) (\x7. true) ((\x6. false) (if true then false else false))
  then
  (if (if x0 then false else false) then (\x5. true) else (\x4. true))
    ((\x3. x3) (if true then true else true))
  else
  (if (if false then false else x0) then (\x2. true) else (\x1. true))
    (if (if true then true else x0) then (if x0 then x0 else false) else
     if true then false else false) ;;

(if
 (if (if false then true else false) then false else
  if false then false else true)
 then (\x7. if true then false else false) else
 if (if false then true else false) then (\x6. true) else (\x5. true))
  ((if (if false then true else false) then (\x4. x4) else (\x3. x3))
     (if (if false then true else false) then (\x2. false) else (\x1. x1))
     ((\x0. if false then true else true)
        (if (if true then true else false) then false else
         if false then false else true))) ;;

(if
 (if true then (if true then false else true) else
  if true then false else true)
 then (if (if true then true else false) then (\x4. true) else (\x3. true))
 else if false then (\x2. x2) else (\x1. true))
  ((\x0. if x0 then x0 else true)
     (if false then true else if true then false else false)) ;;

(if
 (if (if true then false else true) then (if false then false else false)
  else if false then false else true)
 then (if false then (\x3. x3) else (\x2. false)) else
 (\x1. if x1 then true else x1))
  ((\x0. if false then x0 else x0)
     (if true then (if false then false else true) else
      if false then true else true)) ;;

(if
 (if (if false then true else false) then false else
  if false then true else true)
 then (\x10. if false then x10 else x10) else (\x9. if false then x9 else x9))
  ((\x7. \x8. x8) ((\x6. x6) (if false then true else false)))
  (if
   (if (if true then false else false) then (\x5. false) else (\x4. false))
     (if true then (if false then false else false) else
      if false then false else false)
   then
   (if (if false then false else true) then (\x3. true) else (\x2. x2))
     (if (if false then false else true) then (if true then false else false)
      else false)
   else
   (if true then (\x1. true) else (\x0. true))
     (if false then (if true then true else false) else false)) ;;

(if false then (\x1. x1) else (\x0. true))
  (if (if false then false else false) then (if true then false else false)
   else if true then true else true) ;;

if false then (if true then true else false) else
if false then false else false ;;

\x0.
  (if (if x0 then true else false) then (\x4. x4) else (\x3. false))
    ((if (if true then true else x0) then (\x2. true) else (\x1. x1))
       (if (if false then true else x0) then (if true then x0 else x0) else
        if false then false else true)) ;;

(\x3. (\x4. x3) (if false then false else true))
  ((if (if false then true else false) then (\x2. true) else (\x1. x1))
     (if
      (if (if true then true else false) then false else
       if false then true else true)
      then (\x0. true) (if true then true else true) else
      if (if false then true else true) then false else
      if true then false else true)) ;;

if (if false then true else true) then (if true then false else false) else
if true then true else true ;;

(\x2. \x3. false)
  (if (if true then true else true) then true else
   if false then false else true)
  ((if (if true then false else true) then (\x1. true) else (\x0. true))
     (if (if true then true else true) then (if false then false else true)
      else false)) ;;

if (if true then true else false) then (if true then true else false) else
if true then false else true ;;

(\x1.
   if (if true then x1 else false) then (if x1 then false else x1) else
   if x1 then true else true)
  ((\x0. x0)
     (if (if false then false else true) then (if true then true else false)
      else if false then true else true)) ;;

(if
 (if (if false then false else false) then (\x8. true) else (\x7. false))
   (\x6. if false then true else x6)
 then
 (\x5.
    if false then (if true then false else false) else
    if x5 then true else x5)
 else
 (if false then (\x4. x4) else (\x3. x3))
   (if (if true then true else true) then (\x2. x2) else (\x1. true)))
  ((\x0. if false then true else false)
     (if (if false then true else true) then (if false then true else true)
      else true)) ;;

(if (\x10. x10) (if true then false else true) then
 (if (if false then false else false) then (\x9. x9) else (\x8. x8)) else
 if (if true then true else true) then (\x7. x7) else (\x6. x6))
  ((\x4. \x5. x5) ((\x3. x3) (if false then true else false)))
  ((\x2.
      if (if true then x2 else x2) then (if x2 then x2 else x2) else
      if false then false else true)
     ((if (if true then true else true) then (\x1. false) else (\x0. true))
        (if (if true then true else false) then
         (if false then false else true) else if false then false else true))) ;;

(if (if true then true else false) then (\x2. x2) else (\x1. x1))
  ((\x0. x0) (if true then true else false)) ;;

(\x0. \x1. true)
  (if (if false then false else false) then (if true then false else false)
   else if false then false else false)
  (if false then false else if false then true else true) ;;

if (if false then false else false) then (\x1. false) else (\x0. false) ;;

(if (if true then false else false) then (\x5. x5) else (\x4. x4))
  (if (if true then false else false) then (\x3. true) else (\x2. x2))
  ((if (if false then false else false) then (\x1. x1) else (\x0. true))
     (if false then (if true then false else true) else
      if false then true else false)) ;;

(if (if false then true else true) then (\x1. x1) else (\x0. x0))
  (if (if true then false else true) then (if false then true else false)
   else if true then true else true) ;;

if true then false else if false then false else true ;;

\x0.
  if (if true then x0 else true) then (if false then false else true) else
  if false then true else false ;;

(if
 (if (if true then true else false) then (\x8. true) else (\x7. true))
   (if (if false then true else false) then false else
    if true then true else false)
 then (\x5. (\x6. false) (if true then x5 else true)) else
 if true then (\x4. x4) else (\x3. true))
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if true then (\x1. true) else (\x0. false))
        (if (if true then false else true) then
         (if false then false else false) else if true then false else true))) ;;

if (if false then false else false) then true else
if false then false else true ;;

if (if false then true else false) then (if true then false else false) else
true ;;

(if false then (\x3. false) else (\x2. x2))
  ((if (if false then true else true) then (\x1. false) else (\x0. x0))
     (if (if false then false else false) then (if true then false else true)
      else true)) ;;

(if
 (if (if false then true else false) then (if true then false else false)
  else if false then false else true)
 then (\x10. \x11. true) else if true then (\x9. x9) else (\x8. x8))
  ((\x6. \x7. true)
     (if (if true then false else false) then true else
      if true then true else false))
  ((if
    (if (if true then true else true) then true else
     if false then true else true)
    then (if (if false then true else true) then (\x5. false) else (\x4. x4))
    else if true then (\x3. x3) else (\x2. x2))
     ((if (if false then false else true) then (\x1. true) else (\x0. false))
        (if (if false then false else false) then
         (if true then false else false) else false))) ;;

(if (if true then true else true) then (\x1. true) else (\x0. true))
  (if (if true then true else true) then (if false then false else false)
   else if false then false else false) ;;

(if (if true then false else false) then (\x1. true) else (\x0. false))
  (if (if false then true else true) then (if false then true else true) else
   if false then false else true) ;;

(\x2.
   if (if x2 then false else x2) then (if x2 then false else true) else
   if false then x2 else true)
  ((if true then (\x1. x1) else (\x0. true))
     (if (if false then false else false) then (if true then true else false)
      else false)) ;;

if (if false then false else true) then (if false then false else false) else
false ;;

(\x4.
   (if (if true then false else false) then (\x6. x6) else (\x5. true))
     (if (if true then true else true) then (if x4 then true else false) else
      if true then x4 else false))
  ((if (if (if true then false else false) then false else false) then
    (if (if true then false else true) then (\x3. true) else (\x2. true))
    else (\x1. if x1 then true else x1))
     ((\x0. false)
        (if (if true then true else false) then false else
         if false then false else true))) ;;

if (if false then false else true) then (if false then false else true) else
if false then false else false ;;

(if
 (if true then (if true then false else true) else
  if true then false else true)
 then (if (if true then true else false) then (\x3. true) else (\x2. true))
 else if false then (\x1. x1) else (\x0. true))
  (if (if true then true else false) then (if true then true else true) else
   if false then true else true) ;;

(if
 (if
  (if (if false then false else false) then (if true then false else false)
   else if true then false else true)
  then
  (if (if true then true else true) then (if false then false else false)
   else if false then true else true)
  else
  if (if true then true else false) then true else
  if false then false else false)
 then
 (\x7.
    if false then (if x7 then x7 else false) else
    if false then false else false)
 else
 if
 (if (if true then true else true) then false else
  if false then true else false)
 then (if (if true then true else true) then (\x6. true) else (\x5. x5)) else
 if (if false then false else false) then (\x4. true) else (\x3. x3))
  (if
   (\x2. if x2 then true else x2)
     (if (if false then true else false) then (if true then false else false)
      else if false then true else false)
   then
   (if true then (\x1. false) else (\x0. true))
     (if false then (if false then false else true) else true)
   else
   if (if (if true then true else false) then false else true) then
   (if (if false then false else false) then (if true then false else false)
    else if true then true else false)
   else
   if (if true then true else false) then (if false then true else false)
   else false) ;;

(if false then (\x1. true) else (\x0. false))
  (if (if false then false else false) then (if false then true else false)
   else if false then false else false) ;;

(if
 (if (if true then false else true) then (if true then true else false) else
  if false then false else false)
 then (if (if false then false else true) then (\x5. x5) else (\x4. true))
 else if (if false then true else true) then (\x3. false) else (\x2. true))
  ((if (if true then true else false) then (\x1. false) else (\x0. x0))
     (if true then false else if true then false else false)) ;;

(if (if true then false else false) then (\x5. x5) else (\x4. x4))
  (if (if true then false else false) then (\x3. true) else (\x2. x2))
  ((if (if false then false else true) then (\x1. false) else (\x0. x0))
     (if (if true then false else false) then (if false then true else true)
      else if false then false else false)) ;;

(\x2. \x3. x3)
  (if (if true then true else true) then false else
   if false then false else false)
  ((if true then (\x1. x1) else (\x0. true))
     (if (if false then false else false) then (if true then true else false)
      else false)) ;;

(if (if false then true else true) then (\x6. x6) else (\x5. x5))
  (if true then (\x4. x4) else (\x3. false))
  ((if (if false then true else false) then (\x2. false) else (\x1. false))
     (\x0. if x0 then true else false)) ;;

(\x5.
   (\x6. if false then x6 else x6)
     (if (if false then false else true) then true else
      if false then x5 else true))
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then
    (if (if true then true else true) then (\x4. false) else (\x3. true))
    else if (if true then true else true) then (\x2. true) else (\x1. false))
     (if
      (if (if true then true else false) then false else
       if false then true else true)
      then (\x0. true) (if true then true else true) else
      if (if false then true else true) then false else
      if true then false else true)) ;;

\x0.
  (\x1. if false then x1 else false)
    (if
     (if (if x0 then x0 else x0) then (if true then true else true) else
      if false then x0 else x0)
     then (if false then true else x0) else
     if x0 then (if true then true else false) else
     if x0 then true else false) ;;

(\x5. \x6. (\x7. x7) (if x6 then true else false))
  ((if (if false then (if true then true else false) else true) then
    (if false then (\x4. true) else (\x3. true)) else
    if (if true then true else true) then (\x2. true) else (\x1. false))
     ((\x0. if true then true else x0)
        (if (if true then true else false) then
         (if true then false else false) else if true then true else false))) ;;

(if
 (if (if false then true else true) then (if false then true else false) else
  if false then true else true)
 then (if (if false then true else true) then (\x5. x5) else (\x4. true))
 else if (if false then true else false) then (\x3. true) else (\x2. x2))
  ((if (if true then true else true) then (\x1. false) else (\x0. x0))
     (if (if true then false else true) then (if true then true else false)
      else if false then false else false)) ;;

(if (if true then true else true) then (\x1. x1) else (\x0. x0))
  (if true then true else true) ;;

\x0.
  (\x1. if false then x0 else x0)
    (if (if false then true else x0) then (if x0 then x0 else false) else
     if true then true else true) ;;

(\x7.
   (if (if true then x7 else true) then (\x9. true) else (\x8. true))
     (if (if true then true else false) then (if x7 then false else x7) else
      x7))
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then
    (if (if true then true else true) then (\x6. false) else (\x5. true))
    else if (if true then true else true) then (\x4. true) else (\x3. false))
     ((if true then (\x2. x2) else (\x1. true))
        ((\x0. true) (if false then true else false)))) ;;

\x0.
  (\x3.
     if (if x3 then x3 else x3) then (if true then x3 else x3) else
     if x0 then false else false)
    ((if (if false then x0 else false) then (\x2. true) else (\x1. x1))
       (if (if x0 then false else false) then (if x0 then false else x0) else
        if true then x0 else false)) ;;

(\x2. \x3. if true then true else x3)
  ((if (if false then false else false) then (\x1. true) else (\x0. false))
     (if true then (if true then true else false) else
      if false then true else true)) ;;

\x0. (\x1. true) (if x0 then true else true) ;;

\x0.
  \x1.
    if (if false then false else true) then (if x1 then false else true) else
    if x0 then x0 else true ;;

(if (if true then false else true) then (\x3. x3) else (\x2. x2))
  (if (if false then true else false) then (\x1. true) else (\x0. x0)) ;;

(\x2.
   if (if false then true else x2) then (if false then false else false) else
   if x2 then x2 else true)
  ((if false then (\x1. false) else (\x0. false))
     (if (if true then false else true) then (if false then false else true)
      else if false then false else false)) ;;

\x0. \x1. if false then x1 else false ;;

\x0.
  (if (if true then false else true) then (\x2. false) else (\x1. true))
    (if true then x0 else false) ;;

if (if false then false else false) then false else
if true then false else true ;;

if (if true then false else false) then (if true then false else true) else
if false then false else false ;;

(if (if true then false else true) then (\x1. false) else (\x0. x0))
  (if (if true then false else true) then (if false then true else false)
   else if true then true else true) ;;

(if (if true then true else false) then (\x1. false) else (\x0. false))
  (if false then false else false) ;;

if false then false else true ;;

(if
 (if (if false then false else true) then (if false then true else true) else
  true)
 then (if (if false then false else false) then (\x6. false) else (\x5. x5))
 else if true then (\x4. true) else (\x3. false))
  ((\x2.
      if (if true then false else x2) then (if x2 then false else false) else
      if x2 then true else x2)
     ((if (if true then false else true) then (\x1. true) else (\x0. false))
        (if (if true then true else false) then
         (if true then false else true) else if true then false else true))) ;;

(\x2. \x3. true)
  (if (if false then false else false) then (if true then false else false)
   else if false then false else false)
  ((if (if true then true else false) then (\x1. false) else (\x0. true))
     (if (if false then false else false) then (if true then true else false)
      else false)) ;;

(\x2. \x3. if true then true else x3)
  ((if (if true then true else false) then (\x1. false) else (\x0. false))
     (if false then (if true then true else false) else
      if true then true else true)) ;;

(\x2.
   if (if false then true else x2) then (if true then x2 else true) else
   if x2 then false else true)
  ((\x0. (\x1. x0) true)
     (if true then false else if false then true else true)) ;;

if (if true then true else true) then (if false then true else false) else
if true then false else false ;;

(if (if false then false else false) then (\x1. x1) else (\x0. false))
  (if (if true then true else false) then (if false then true else false)
   else true) ;;

if false then false else if false then false else true ;;

(\x0. \x1. x1)
  (if (if true then true else false) then false else
   if true then true else false)
  (if (if true then true else false) then (if true then true else true) else
   if false then true else true) ;;

if false then (if true then true else false) else true ;;

\x0.
  (if (if true then true else true) then (\x2. true) else (\x1. x0))
    (if (if true then x0 else x0) then (if false then false else x0) else
     if x0 then true else x0) ;;

\x0.
  if (\x1. x0) (if x0 then x0 else false) then
  (if (if x0 then true else x0) then (if true then x0 else false) else
   if false then true else true)
  else
  if (if false then x0 else true) then x0 else if x0 then false else true ;;

\x0.
  (\x2. if x2 then x0 else x0)
    ((if (if true then true else true) then x0 else x0)
       ((\x1. false) (if true then x0 else x0))) ;;

\x0.
  if (if false then true else false) then (if x0 then true else x0) else
  if true then true else x0 ;;

\x0.
  (\x1. if false then true else x0)
    (if (if true then x0 else x0) then (if false then true else x0) else
     if false then false else x0) ;;

if true then (if false then true else false) else
if false then false else false ;;

(if (if false then true else true) then (\x5. x5) else (\x4. x4))
  (if true then (\x3. x3) else (\x2. false))
  ((if (if true then false else true) then (\x1. x1) else (\x0. x0))
     (if (if true then false else true) then (if false then true else false)
      else if true then false else false)) ;;

\x0.
  \x1.
    (\x3. if true then x0 else true)
      ((\x2. x1) (if false then x0 else false)) ;;

if (if true then true else true) then true else if true then true else false ;;

(\x0. if x0 then true else false)
  (if (if false then false else true) then (if true then false else false)
   else if false then true else false) ;;

(\x3.
   (if (if x3 then false else false) then (\x5. true) else (\x4. true))
     (if (if true then true else true) then (if x3 then true else false) else
      if true then x3 else false))
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if false then (\x1. true) else (\x0. x0))
        (if (if true then true else true) then false else
         if false then false else true))) ;;

if (if false then true else false) then (if false then true else true) else
if true then true else true ;;

if true then (if false then true else false) else
if true then true else false ;;

(\x0. if true then false else x0)
  (if false then (if false then true else false) else
   if false then false else true) ;;

(if
 (if (if true then true else false) then (\x10. true) else (\x9. true))
   (if (if false then true else false) then false else
    if true then true else false)
 then (\x7. (\x8. false) (if true then x7 else true)) else
 if true then (\x6. x6) else (\x5. true))
  ((if
    (if (if true then true else true) then (if false then true else false)
     else if false then false else false)
    then
    (if (if true then true else true) then (\x4. true) else (\x3. false))
    else if false then (\x2. false) else (\x1. true))
     ((\x0. false)
        (if (if true then true else true) then true else
         if false then true else true))) ;;

if (if false then true else true) then (if true then false else false) else
if false then false else true ;;

\x0.
  (\x3.
     if (if x3 then false else x3) then (if x0 then false else true) else
     if false then true else false)
    ((if x0 then (\x2. false) else (\x1. x1))
       (if (if x0 then false else false) then (if false then true else false)
        else if x0 then false else x0)) ;;

if (if false then false else true) then (if true then true else true) else
if true then true else false ;;

if (if true then false else false) then (if true then true else true) else
if false then true else false ;;

(if (if false then true else true) then (\x1. x1) else (\x0. true))
  (if (if true then true else false) then (if false then true else false)
   else if false then false else false) ;;

(if
 (if (if false then true else true) then (if false then false else true) else
  if false then false else false)
 then (if (if true then false else false) then (\x8. x8) else (\x7. x7)) else
 if false then (\x6. x6) else (\x5. x5))
  ((\x3. \x4. x4)
     (if (if false then false else true) then
      (if false then false else false) else if true then false else false))
  (if
   (if
    (if (if false then true else false) then (if false then true else false)
     else if true then false else false)
    then
    (if true then (if false then false else false) else
     if false then false else true)
    else
    if (if true then true else true) then (if false then true else true) else
    if false then false else false)
   then
   (\x2. if x2 then false else false)
     (if (if false then false else true) then (if true then false else false)
      else if true then false else true)
   else
   (if true then (\x1. true) else (\x0. true))
     (if false then (if true then true else false) else false)) ;;

\x0.
  if (if true then x0 else true) then (if x0 then x0 else false) else
  if true then x0 else x0 ;;

if false then (if false then true else true) else
if false then false else true ;;

if (if true then true else false) then (if true then false else true) else
if false then false else true ;;

\x0.
  if (if false then true else true) then (if x0 then false else true) else
  if false then true else false ;;

(if
 (if (if true then false else true) then (if true then true else false) else
  if false then false else false)
 then (if (if true then true else false) then (\x4. true) else (\x3. true))
 else (\x2. if true then false else x2))
  ((if (if false then false else true) then (\x1. false) else (\x0. false))
     (if (if true then true else false) then (if false then true else false)
      else if true then false else false)) ;;

(if
 (if (if false then true else false) then false else
  if false then true else true)
 then (\x10. if false then x10 else x10) else (\x9. if false then x9 else x9))
  ((\x7. \x8. x8) ((\x6. x6) (if false then true else false)))
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. x2))
     ((if (if true then true else true) then (\x1. false) else (\x0. x0))
        (if true then false else false))) ;;

if
(\x1. if false then false else x1)
  (if (if true then true else false) then (if false then true else false)
   else if true then false else false)
then
(if (if true then false else false) then (if true then false else false) else
 if false then true else false)
else
(\x0. if x0 then true else false)
  (if (if false then false else false) then true else true) ;;

(\x4. if true then x4 else x4)
  (if (if false then false else false) then (\x3. x3) else (\x2. false))
  ((if (if false then false else false) then (\x1. x1) else (\x0. true))
     (if false then (if true then false else true) else
      if false then true else false)) ;;

\x0. (\x1. true) (if x0 then true else false) ;;

(\x2. if false then x2 else x2)
  (if (if false then false else false) then (\x1. true) else (\x0. true)) ;;

if true then (if true then false else false) else true ;;

if true then (if false then false else true) else
if true then false else true ;;

(\x0. \x1. x1)
  (if (if true then true else true) then false else
   if false then false else false)
  (if
   (if (if true then false else true) then (if false then true else false)
    else if true then true else true)
   then (if (if false then true else true) then true else true) else
   if (if false then false else false) then (if false then true else false)
   else if true then true else true) ;;

if (if false then false else true) then (if true then true else false) else
true ;;

if (if false then true else false) then (if true then true else true) else
if true then true else true ;;

(if (if false then false else false) then (\x1. x1) else (\x0. true))
  (if (if false then true else false) then (if false then false else false)
   else if true then true else true) ;;

\x0.
  if (if false then true else true) then (if true then true else x0) else
  if true then true else false ;;

(\x1. (\x2. x1) x1)
  ((\x0. if true then x0 else x0)
     (if (if false then false else true) then (if true then false else true)
      else if true then true else false)) ;;

if (if true then true else true) then (\x1. false) else (\x0. true) ;;

if (if false then false else true) then (if false then false else false) else
if false then false else false ;;

(\x0. \x1. x1)
  (if (if false then false else false) then (if false then true else true)
   else if false then true else false) ;;

if (if true then true else true) then (if true then false else true) else
if true then false else false ;;

(if true then (\x1. true) else (\x0. x0))
  (if true then (if false then true else false) else
   if true then true else true) ;;

(\x4. \x5. if true then false else x4)
  ((if (if false then true else true) then (\x3. x3) else (\x2. true))
     (if (if false then false else true) then (if true then true else true)
      else if true then false else false))
  ((if false then (\x1. true) else (\x0. false))
     (if (if false then true else false) then true else
      if false then true else false)) ;;

if (if false then true else false) then (if false then true else true) else
false ;;

\x0.
  (\x1. if false then x0 else x1)
    (if (if false then true else false) then (if true then true else false)
     else if x0 then true else x0) ;;

if (if false then false else true) then false else
if false then false else true ;;

\x0. \x1. if true then true else x0 ;;

(\x6. \x7. if x7 then x7 else x7)
  ((if
    (if (if true then true else true) then true else
     if false then true else true)
    then (if (if false then true else true) then (\x5. false) else (\x4. x4))
    else if true then (\x3. x3) else (\x2. x2))
     ((if (if false then false else true) then (\x1. true) else (\x0. false))
        (if (if false then false else false) then
         (if true then false else false) else false))) ;;

(if
 (if false then (\x6. true) else (\x5. x5))
   (if (if true then true else true) then (if false then true else true) else
    if false then false else true)
 then
 (\x4.
    if false then (if true then false else false) else
    if x4 then true else x4)
 else if true then (\x3. x3) else (\x2. true))
  ((\x0. (\x1. x0) true)
     (if true then false else if false then true else true)) ;;

(if (if true then false else true) then (\x2. x2) else (\x1. x1))
  (\x0. if x0 then x0 else true) ;;

\x0.
  (if (if false then x0 else true) then (\x2. x2) else (\x1. x0))
    (if (if true then x0 else x0) then (if x0 then x0 else x0) else
     if true then true else x0) ;;

(\x1. \x2. x1) (if true then false else if false then false else false)
  ((\x0. if x0 then true else false)
     (if (if false then true else false) then (if false then true else false)
      else if true then true else false)) ;;

if (if false then true else true) then (if true then true else true) else
if false then false else true ;;

\x0.
  if (if true then false else false) then (if x0 then x0 else false) else
  if false then false else false ;;

(if
 (if (if false then false else false) then (if false then true else true)
  else if false then true else true)
 then (if (if true then true else true) then (\x9. x9) else (\x8. true)) else
 if true then (\x7. false) else (\x6. true))
  ((if (if false then (if true then true else false) else true) then
    (if (if false then true else true) then (\x5. false) else (\x4. x4)) else
    if false then (\x3. false) else (\x2. true))
     ((if true then (\x1. x1) else (\x0. false))
        (if true then false else true))) ;;

if false then false else if false then true else false ;;

(\x5.
   (if (if x5 then x5 else x5) then (\x8. x5) else (\x7. false))
     (\x6. if false then true else x5))
  ((\x4. x4)
     (if (if true then false else true) then (\x3. true) else (\x2. true))
     ((if false then (\x1. false) else (\x0. false))
        (if (if true then true else true) then
         (if false then false else true) else if false then true else true))) ;;

(if true then (\x1. x1) else (\x0. x0))
  (if (if false then true else true) then (if true then false else false)
   else if false then true else true) ;;

(\x5. if true then x5 else x5)
  (if (if false then false else false) then (\x4. x4) else (\x3. false))
  ((if (if false then false else false) then (\x2. true) else (\x1. true))
     (\x0. if x0 then true else x0)) ;;

\x0.
  (if (if x0 then false else x0) then (\x2. false) else (\x1. x0))
    (if (if false then true else false) then (if false then true else x0)
     else if true then false else true) ;;

(if (if false then true else true) then (\x1. x1) else (\x0. true))
  (if (if false then false else false) then (if false then true else true)
   else if false then true else false) ;;

if (if true then false else false) then false else
if true then true else false ;;

(if
 (if (if true then false else true) then (if true then true else false) else
  if false then false else false)
 then (if (if true then true else false) then (\x2. true) else (\x1. true))
 else (\x0. if true then false else x0))
  (if (if true then true else false) then (if false then true else false)
   else if true then false else false) ;;

(if
 (if (if false then true else false) then (if true then false else false)
  else if false then true else true)
 then (if (if true then true else false) then (\x3. false) else (\x2. x2))
 else if (if true then false else true) then (\x1. x1) else (\x0. true))
  (if
   (if (if true then true else false) then (if true then true else true) else
    true)
   then (if false then true else true) else
   if (if true then false else false) then (if true then true else true) else
   if true then true else false) ;;

(if
 (if (if true then true else true) then (if true then false else true) else
  true)
 then (if true then (\x6. true) else (\x5. x5)) else
 if (if false then true else false) then (\x4. true) else (\x3. true))
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if false then (\x1. true) else (\x0. x0))
        (if (if true then true else true) then false else
         if false then false else true))) ;;

(if
 (if (if false then true else false) then (if false then true else false)
  else if false then false else true)
 then (if (if true then true else false) then (\x5. false) else (\x4. x4))
 else if false then (\x3. false) else (\x2. false))
  ((if (if true then false else true) then (\x1. true) else (\x0. false))
     (if (if false then true else true) then (if false then true else false)
      else true)) ;;

\x0. \x1. if true then x1 else x0 ;;

(if
 (if false then (\x11. true) else (\x10. x10))
   (if (if true then true else true) then (if false then true else true) else
    if false then false else true)
 then
 (if
  (if (if false then true else false) then (if true then false else false)
   else if false then false else false)
  then (if (if false then true else true) then (\x9. true) else (\x8. x8))
  else if (if false then false else true) then (\x7. false) else (\x6. x6))
 else
 (\x5.
    if (if false then x5 else true) then (if true then false else true) else
    if false then false else false))
  ((if false then (\x4. x4) else (\x3. x3))
     (if (if false then true else false) then (\x2. false) else (\x1. x1))
     (if
      (if (if true then true else false) then false else
       if false then true else true)
      then (\x0. true) (if true then true else true) else
      if (if false then true else true) then false else
      if true then false else true)) ;;

(\x2.
   if (if false then true else x2) then (if true then true else false) else
   if x2 then true else x2)
  ((if (if false then true else true) then (\x1. true) else (\x0. true))
     (if (if true then false else true) then (if true then false else true)
      else true)) ;;

if (if false then true else false) then (if false then false else true) else
if false then true else true ;;

(\x2. \x3. x3)
  (if (if false then false else false) then (if true then false else false)
   else if false then false else false)
  ((if (if true then true else false) then (\x1. false) else (\x0. false))
     (if false then (if true then true else false) else
      if true then true else true)) ;;

(\x0. if x0 then x0 else false)
  (if (if false then false else false) then true else
   if false then false else true) ;;

(\x0. if false then x0 else x0)
  (if (if false then false else false) then (if true then false else false)
   else true) ;;

(if (if true then false else true) then (\x1. true) else (\x0. x0))
  (if (if true then true else true) then (if true then false else true) else
   true) ;;

(if (if false then false else true) then (\x1. x1) else (\x0. false))
  (if (if false then false else false) then (if true then false else false)
   else if true then true else true) ;;

if
(if
 (if (if false then false else true) then (if true then true else true) else
  if true then false else true)
 then (if false then (\x12. false) else (\x11. true)) else
 if (if false then false else false) then (\x10. true) else (\x9. true))
  ((if (if false then false else false) then (\x8. true) else (\x7. true))
     (if (if true then true else false) then (if false then false else true)
      else if true then false else false))
then
(\x5. \x6. true)
  (if true then (if true then true else true) else
   if false then false else false)
  ((if (if true then false else false) then (\x4. false) else (\x3. false))
     (if (if true then false else true) then (if false then true else true)
      else if false then false else true))
else
(\x2.
   if (if true then true else true) then (if false then false else false)
   else if true then x2 else true)
  ((if (if false then true else false) then (\x1. x1) else (\x0. x0))
     (if (if false then true else true) then (if false then false else true)
      else if false then false else false)) ;;

if
(if (if true then true else true) then (\x4. false) else (\x3. x3))
  (if false then false else false)
then
(if (if false then false else false) then (\x2. true) else (\x1. false))
  (if (if true then false else false) then (if false then false else false)
   else if false then true else true)
else
(\x0. if true then true else x0)
  (if (if true then false else true) then (if true then false else true) else
   if false then true else true) ;;

\x0.
  (\x1. if x1 then x0 else false)
    (if (if false then x0 else x0) then (if true then true else true) else
     if true then false else false) ;;

\x0.
  if (if true then x0 else true) then (if x0 then true else true) else
  if false then x0 else true ;;

\x0. \x1. if x0 then x1 else true ;;

(if (if true then false else false) then (\x2. x2) else (\x1. true))
  ((\x0. x0) (if true then true else false)) ;;

\x0.
  if (if false then true else true) then (if true then true else x0) else
  if true then true else x0 ;;

if (if true then true else true) then true else true ;;

(if
 (if (if false then false else false) then (\x15. true) else (\x14. false))
   (\x13. if false then true else x13)
 then
 (\x12.
    if false then (if true then false else false) else
    if x12 then true else x12)
 else
 (if false then (\x11. x11) else (\x10. x10))
   (if (if true then true else true) then (\x9. x9) else (\x8. true)))
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then (if (if false then true else true) then (\x7. x7) else (\x6. x6))
    else if (if false then true else false) then (\x5. true) else (\x4. x4))
     ((if (if false then false else true) then (\x3. false) else (\x2. false))
        (if true then (\x1. x1) else (\x0. true)))) ;;

if (if false then true else true) then (if true then false else false) else
false ;;

(\x2.
   (if (if x2 then x2 else x2) then (\x5. x2) else (\x4. false))
     (\x3. if false then true else x2))
  ((\x1.
      if (if true then x1 else false) then (if x1 then false else x1) else
      if x1 then true else true)
     ((\x0. if true then true else x0)
        (if (if true then true else false) then
         (if true then false else false) else if true then true else false))) ;;

(if
 (if (if true then true else true) then true else
  if true then false else true)
 then (if (if true then false else false) then (\x5. false) else (\x4. x4))
 else if (if false then false else true) then (\x3. true) else (\x2. x2))
  ((if (if false then false else true) then (\x1. false) else (\x0. false))
     (if (if true then true else false) then (if false then true else false)
      else if true then false else false)) ;;

(\x0. if x0 then true else true)
  (if (if false then true else true) then (if true then false else false)
   else if false then true else false) ;;

\x0.
  (\x3. \x4. x0)
    (if (if false then x0 else x0) then (if x0 then false else false) else
     if false then x0 else false)
    ((if (if true then true else true) then (\x2. false) else (\x1. true))
       (if (if false then false else false) then
        (if false then false else false) else if true then true else x0)) ;;

(if
 (if (if false then true else true) then (if false then true else false) else
  if false then true else true)
 then (if (if true then false else false) then (\x4. false) else (\x3. x3))
 else if false then (\x2. x2) else (\x1. x1))
  ((\x0. if x0 then x0 else true)
     (if false then true else if true then false else false)) ;;

if (if false then true else false) then (if false then false else false) else
if true then true else true ;;

if (if true then true else true) then (if true then true else true) else
if true then true else false ;;

(\x3. \x4. (\x5. x5) (if x4 then true else false))
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if false then (\x1. true) else (\x0. x0))
        (if (if true then true else true) then false else
         if false then false else true))) ;;

\x0.
  (\x3. \x4. x0)
    (if (if x0 then false else x0) then (if x0 then false else true) else
     if true then x0 else x0)
    ((if (if true then true else x0) then (\x2. false) else (\x1. x1))
       (if (if false then true else x0) then (if true then x0 else x0) else
        false)) ;;

\x0.
  (\x2. if true then x2 else x0) (\x1. x1)
    ((if (if false then false else false) then (if false then x0 else x0)
      else if true then x0 else x0) (if x0 true then x0 true else false)) ;;

(\x6.
   (if (if false then true else x6) then (\x9. true) else (\x8. x8))
     ((\x7. x6) (if false then true else true)))
  ((if
    (if (if false then false else true) then (if true then false else false)
     else if false then false else true)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. true))
     (\x0. (\x1. x1) x0)) ;;

(if (if false then true else true) then (\x1. false) else (\x0. false))
  (if false then false else true) ;;

(\x1. \x2. x2)
  (if (if true then false else false) then false else
   if true then true else false)
  ((\x0. false) (if (if false then true else true) then false else true)) ;;

\x0.
  (\x3. \x4. x0) ((\x2. x0) (if false then false else false))
    (if
     (if (if false then true else false) then (if false then x0 else true)
      else if x0 then x0 else false)
     then
     (if (if x0 then x0 else true) then x0 else if true then true else true)
     else (\x1. false) (if x0 then false else x0)) ;;

\x0.
  (if (if true then false else x0) then (\x3. false) else (\x2. true))
    ((\x1. if false then x1 else false)
       (if (if x0 then false else false) then (if true then x0 else x0) else
        if true then false else true)) ;;

(if (if false then false else true) then (\x1. x1) else (\x0. true))
  (if false then (if false then false else true) else
   if true then false else true) ;;

(if (if false then true else true) then (\x5. x5) else (\x4. x4))
  (if true then (\x3. x3) else (\x2. false))
  ((if (if false then true else true) then (\x1. false) else (\x0. x0))
     (if (if false then false else false) then (if true then false else true)
      else true)) ;;

(if
 (\x11. if true then true else x11)
   (if false then (if true then true else true) else
    if true then false else true)
 then
 (if
  (if (if false then false else false) then true else
   if false then false else true)
  then
  (if (if false then true else true) then (\x10. true) else (\x9. false))
  else if (if false then false else false) then (\x8. false) else (\x7. true))
 else (\x6. if x6 then false else false))
  ((if false then (\x5. x5) else (\x4. x4))
     (if (if false then false else false) then (\x3. true) else (\x2. false))
     ((if (if false then false else true) then (\x1. true) else (\x0. true))
        (if (if true then true else true) then true else
         if false then false else false))) ;;

if (if false then false else false) then (if true then false else true) else
true ;;

(if (if false then true else true) then (\x1. x1) else (\x0. true))
  (if (if false then false else true) then (if true then false else false)
   else if false then false else true) ;;

(\x6.
   (if (if false then true else x6) then (\x8. false) else (\x7. false))
     (if (if false then true else true) then (if true then x6 else x6) else
      if true then x6 else false))
  (if
   (if (if true then false else false) then (\x5. false) else (\x4. false))
     (if true then (if false then false else false) else
      if false then false else false)
   then
   (if (if false then false else true) then (\x3. true) else (\x2. x2))
     (if (if false then false else true) then (if true then false else false)
      else false)
   else
   (if true then (\x1. true) else (\x0. true))
     (if false then (if true then true else false) else false)) ;;

if (if false then true else true) then (if true then true else true) else
if false then true else true ;;

(if
 (if (if false then true else false) then (if true then false else false)
  else if false then false else true)
 then (\x7. \x8. true) else if true then (\x6. x6) else (\x5. x5))
  ((\x3. \x4. true)
     (if (if true then false else false) then true else
      if true then true else false))
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if false then (\x1. true) else (\x0. x0))
        (if (if true then true else true) then false else
         if false then false else true))) ;;

(if
 (if (if false then false else false) then (if false then false else false)
  else if true then false else true)
 then
 (if (if false then true else false) then (\x7. false) else (\x6. false))
 else (\x5. if true then true else x5))
  ((\x4.
      if (if x4 then false else true) then (if x4 then false else false) else
      if x4 then false else true)
     ((if (if false then false else true) then (\x3. false) else (\x2. false))
        (if true then (\x1. x1) else (\x0. true)))) ;;

\x0.
  if (if false then x0 else x0) then (if x0 then true else x0) else
  if false then false else false ;;

(if (if false then true else false) then (\x1. false) else (\x0. x0))
  (if (if true then false else true) then (if false then true else false)
   else if true then true else true) ;;

(if
 (if (if false then true else true) then (if false then true else false) else
  if false then true else true)
 then (if (if true then false else false) then (\x4. false) else (\x3. x3))
 else if false then (\x2. x2) else (\x1. x1))
  ((\x0. false) (if (if false then true else true) then false else true)) ;;

(if (if false then true else false) then (\x1. true) else (\x0. true))
  (if false then (if false then true else true) else
   if true then false else true) ;;

(if false then (\x1. false) else (\x0. false)) (if true then false else true) ;;

(\x2.
   if (if x2 then true else true) then (if false then x2 else x2) else
   if x2 then true else true)
  ((if (if true then false else true) then (\x1. true) else (\x0. true))
     (if (if true then true else true) then (if false then false else true)
      else false)) ;;

(if (if false then false else false) then (\x1. true) else (\x0. x0))
  (if (if true then false else true) then (if false then true else true) else
   true) ;;

if (if false then true else true) then (if false then true else false) else
false ;;

(\x1. \x2. if true then true else x2)
  ((\x0. if x0 then true else false)
     (if (if false then true else false) then (if false then true else false)
      else if true then true else false)) ;;

(\x2. \x3. x2) (if true then false else if false then false else false)
  ((\x1. x1) (\x0. true)
     (if (if true then true else true) then (if false then true else false)
      else if false then true else false)) ;;

(if (if true then false else true) then (\x5. x5) else (\x4. x4))
  (\x3. if x3 then true else false)
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if true then (\x1. true) else (\x0. false))
        (if (if true then false else true) then
         (if false then false else false) else if true then false else true))) ;;

if (if true then false else false) then (if true then true else true) else
if true then false else true ;;

(if true then (\x1. x1) else (\x0. x0))
  (if (if true then true else true) then (if false then false else true) else
   true) ;;

(if
 (if (if true then false else true) then (if true then true else false) else
  if false then false else false)
 then (if false then (\x3. true) else (\x2. true)) else
 (\x1. if true then false else x1))
  ((\x0. if true then true else true)
     (if (if false then false else true) then
      (if false then false else false) else if false then false else false)) ;;

(\x2.
   if (if false then true else x2) then (if false then false else false) else
   if x2 then x2 else true)
  ((if (if true then true else false) then (\x1. x1) else (\x0. true))
     (if (if false then true else true) then false else true)) ;;

(if (if true then false else false) then (\x1. x1) else (\x0. false))
  (if (if false then true else true) then (if false then true else false)
   else if false then true else false) ;;

(if (if true then true else false) then (\x1. true) else (\x0. x0))
  (if false then (if false then false else true) else
   if true then true else true) ;;

(\x2. \x3. true)
  ((if true then (\x1. x1) else (\x0. true))
     (if (if false then false else false) then (if true then true else false)
      else false)) ;;

if
(\x9.
   if (if true then false else false) then x9 else if false then true else x9)
  ((\x8. if false then x8 else x8)
     (if (if true then false else true) then (if true then true else true)
      else if true then true else true))
then
(if
 (if (if false then false else false) then (if false then true else false)
  else if true then false else false)
 then (if (if true then true else true) then (\x7. true) else (\x6. x6)) else
 if (if true then true else false) then (\x5. true) else (\x4. false))
  ((if (if true then false else false) then (\x3. x3) else (\x2. x2))
     (if (if true then true else true) then (if true then false else false)
      else if false then true else true))
else
(if (if false then true else true) then (\x1. true) else (\x0. x0))
  (if (if false then false else false) then (if true then false else true)
   else if false then true else false) ;;

\x0.
  if (if false then true else true) then (if true then true else x0) else
  if true then x0 else x0 ;;

(if
 (if (if false then false else false) then (\x11. true) else (\x10. true))
   (if (if true then true else true) then (if false then true else true) else
    if false then false else true)
 then
 (if
  (if (if false then true else false) then (if true then false else false)
   else if false then false else false)
  then (if (if false then true else true) then (\x9. true) else (\x8. x8))
  else if (if false then false else true) then (\x7. false) else (\x6. x6))
 else
 if
 (if (if true then true else true) then false else
  if false then true else false)
 then (if (if true then true else true) then (\x5. true) else (\x4. x4)) else
 if (if false then false else false) then (\x3. true) else (\x2. x2))
  ((\x0. (\x1. x0) true)
     (if true then false else if false then true else true)) ;;

\x0. (\x1. x0) x0 ;;

(\x0. if false then true else true) (if true then true else true) ;;

(if false then (\x1. x1) else (\x0. x0))
  (if (if true then false else true) then (if true then false else true) else
   if false then true else false) ;;

(if (if true then false else false) then (\x1. true) else (\x0. x0))
  (if (if false then false else true) then (if false then false else false)
   else if false then true else false) ;;

(if
 (if (if false then false else false) then (if false then true else true)
  else if false then true else true)
 then (if (if true then true else true) then (\x7. x7) else (\x6. true)) else
 if true then (\x5. false) else (\x4. true))
  ((\x3.
      if (if true then x3 else false) then (if x3 then false else x3) else
      if x3 then true else true)
     ((if (if true then false else false) then (\x2. x2) else (\x1. x1))
        ((\x0. false) (if false then true else false)))) ;;

if
(if (if true then false else false) then (\x3. true) else (\x2. false))
  (if (if true then false else true) then (if false then true else true) else
   if false then true else false)
then (\x1. if true then x1 else true) else
(\x0.
   if (if false then x0 else true) then (if false then x0 else true) else
   if x0 then false else x0) ;;

if (if false then false else true) then (if true then true else false) else
if true then false else false ;;

(if (if true then false else false) then (\x1. false) else (\x0. false))
  (if (if false then false else false) then (if true then false else true)
   else if true then true else true) ;;

\x0. x0 true ;;

(if
 (if (if false then false else false) then (\x16. true) else (\x15. true))
   (if (if true then true else true) then (if false then true else true) else
    if false then false else true)
 then
 (if (\x14. false) (if false then true else false) then
  (if (if false then false else false) then (\x13. true) else (\x12. true))
  else
  if (if false then false else false) then (\x11. true) else (\x10. false))
 else
 (if false then (\x9. x9) else (\x8. x8))
   (if (if true then true else true) then (\x7. x7) else (\x6. true)))
  ((if
    (if (if false then true else false) then (if false then false else true)
     else if false then true else true)
    then (if false then (\x5. true) else (\x4. true)) else
    if (if false then true else false) then (\x3. x3) else (\x2. false))
     ((if true then (\x1. false) else (\x0. true))
        (if (if true then false else false) then
         (if false then false else true) else if false then false else false))) ;;

(\x1. \x2. true)
  ((\x0. if x0 then true else true)
     (if (if false then true else true) then (if false then false else true)
      else if false then false else false)) ;;

if (if true then false else false) then (if true then false else false) else
if true then true else false ;;

(\x1. \x2. x2) (if false then (if true then true else true) else true)
  ((\x0. if false then x0 else x0)
     (if true then (if false then false else true) else
      if false then true else true)) ;;

(if (if false then true else false) then (\x1. x1) else (\x0. true))
  (if false then (if false then true else false) else
   if false then false else false) ;;

(\x0. if x0 then true else true)
  (if (if true then false else false) then (if false then false else true)
   else if false then true else true) ;;

(\x1. \x2. if true then true else x2)
  ((\x0. if true then x0 else false)
     (if (if true then false else true) then (if true then false else true)
      else true)) ;;

if (if false then false else true) then (if false then true else true) else
false ;;

(\x0. if false then x0 else x0)
  (if false then (if false then true else false) else
   if false then false else false) ;;

(\x0. \x1. x0)
  (if (if false then true else false) then (if false then true else true)
   else if false then false else true) ;;

(if
 (if (if false then false else true) then (if false then true else false)
  else if true then false else true)
 then (\x9. if true then x9 else x9) else
 if (if false then true else false) then (\x8. x8) else (\x7. x7))
  ((\x5. \x6. x6) ((\x4. x4) (if false then true else false)))
  ((\x3.
      if (if true then x3 else false) then (if x3 then false else x3) else
      if x3 then true else true)
     ((if (if true then false else false) then (\x2. x2) else (\x1. x1))
        ((\x0. false) (if false then true else false)))) ;;

(\x0. if true then x0 else x0)
  (if (if false then false else false) then (if true then false else false)
   else if true then false else true) ;;

(\x7. \x8. x8)
  (if false then (if true then true else false) else
   if false then true else false)
  ((if true then (\x6. x6) else (\x5. x5))
     (if true then (\x4. false) else (\x3. true))
     ((if (if false then false else true) then (\x2. true) else (\x1. false))
        (\x0. true))) ;;

\x0. if false then x0 else false ;;

(\x4. \x5. x5) ((\x3. x3) true)
  ((\x2.
      if (if x2 then false else true) then (if x2 then false else x2) else x2)
     ((if (if false then true else true) then (\x1. true) else (\x0. false))
        (if (if false then true else true) then true else
         if false then false else true))) ;;

(\x1.
   (if (if true then false else false) then (\x3. x3) else (\x2. true))
     (if (if true then true else true) then (if x1 then true else false) else
      if true then x1 else false))
  ((\x0. if true then true else x0)
     (if (if false then true else false) then (if false then true else true)
      else if false then true else false)) ;;

if (if false then (if false then true else false) else false) then
(if (if true then false else false) then (if false then false else false)
 else if false then true else false)
else
if (if false then false else true) then (if false then true else true) else
if true then true else false ;;

(if (if true then true else true) then (\x1. x1) else (\x0. false))
  (if (if false then true else false) then (if false then false else true)
   else true) ;;

\x0.
  (\x3. if (if false then x0 else x3) then false else if x3 then x3 else x3)
    ((if (if true then true else false) then (\x2. x0) else (\x1. false))
       (if (if false then x0 else false) then (if true then x0 else x0) else
        if x0 then false else x0)) ;;

(\x0. if false then x0 else true)
  (if (if true then true else true) then false else true) ;;

(\x0. \x1. x1) (if true then (if false then true else false) else true) ;;

(\x2. if true then x2 else x2)
  (if (if false then false else false) then (\x1. x1) else (\x0. false))
  (if false then false else if false then true else true) ;;

(\x6. if true then x6 else if x6 then x6 else x6)
  ((if (if (if true then false else false) then false else false) then
    (if (if false then true else true) then (\x5. true) else (\x4. false))
    else if (if true then false else false) then (\x3. x3) else (\x2. false))
     ((if (if false then true else true) then (\x1. x1) else (\x0. x0))
        (if (if false then true else false) then
         (if false then false else false) else if true then true else true))) ;;

\x0.
  if (if x0 then false else x0) then (if x0 then true else x0) else
  if true then true else false ;;

if (if true then false else true) then false else true ;;

(\x6.
   (\x7. if x7 then true else x7)
     (if (if false then true else true) then (if false then true else true)
      else false))
  ((if (if (if true then false else false) then false else false) then
    (if (if true then true else true) then (\x5. true) else (\x4. false))
    else if false then (\x3. false) else (\x2. false))
     ((if (if true then true else true) then (\x1. true) else (\x0. x0))
        (if (if true then true else false) then false else
         if false then false else true))) ;;

if
(if (if true then true else true) then (\x4. false) else (\x3. x3))
  (if false then false else false)
then (\x1. (\x2. false) (if true then x1 else x1)) else
(\x0.
   if (if false then x0 else true) then (if false then x0 else true) else
   if x0 then false else x0) ;;

if (if false then true else false) then true else false ;;

if
(if
 (if (if false then false else true) then (if true then true else true) else
  if true then false else true)
 then (if false then (\x14. false) else (\x13. true)) else
 if (if false then false else false) then (\x12. true) else (\x11. true))
  ((if (if false then false else false) then (\x10. true) else (\x9. true))
     (if (if true then true else false) then (if false then false else true)
      else if true then false else false))
then
(if
 (if (if true then true else true) then (if false then false else false) else
  if false then true else false)
 then (if (if true then false else true) then (\x8. x8) else (\x7. true))
 else if (if true then false else false) then (\x6. false) else (\x5. false))
  ((if (if false then true else true) then (\x4. true) else (\x3. x3))
     (if (if true then false else true) then (if false then true else true)
      else if true then false else true))
else
(if true then (\x2. x2) else (\x1. false))
  ((\x0. if false then false else true)
     (if false then (if true then true else false) else
      if false then false else true)) ;;

(if
 (if (if false then false else false) then (\x8. true) else (\x7. false))
   (\x6. if false then true else x6)
 then
 (\x5.
    if false then (if x5 then x5 else false) else
    if false then false else false)
 else
 if
 (if (if false then false else true) then (if true then true else true) else
  if true then true else false)
 then (\x4. if false then x4 else true) else (\x3. if true then x3 else true))
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if false then (\x1. true) else (\x0. x0))
        (if (if true then true else true) then false else
         if false then false else true))) ;;

(if (if false then true else true) then (\x1. x1) else (\x0. true))
  (if (if false then false else true) then (if true then false else true)
   else true) ;;

(\x0. if true then true else false)
  (if true then (if false then false else false) else
   if true then true else true) ;;

(if (if false then (if true then true else true) else true) then
 (if (if false then false else true) then (\x5. false) else (\x4. false))
 else if (if true then false else true) then (\x3. x3) else (\x2. true))
  ((if true then (\x1. true) else (\x0. x0))
     (if false then (if true then false else true) else
      if false then true else false)) ;;

(if (if false then true else false) then (\x1. x1) else (\x0. true))
  (if (if false then true else true) then (if true then false else false)
   else if false then true else false) ;;

(if
 (\x5. if x5 then true else true)
   (if (if false then false else false) then (if true then true else true)
    else if true then false else false)
 then
 (\x4.
    if false then (if x4 then x4 else false) else
    if false then false else false)
 else (\x3. if x3 then false else false))
  (if
   (if
    (if (if false then true else false) then (if false then true else false)
     else if true then false else false)
    then
    (if true then (if false then false else false) else
     if false then false else true)
    else
    if (if true then true else true) then (if false then true else true) else
    if false then false else false)
   then
   (\x2. if x2 then false else false)
     (if (if false then false else true) then (if true then false else false)
      else if true then false else true)
   else
   (if true then (\x1. true) else (\x0. true))
     (if false then (if true then true else false) else false)) ;;

if (if false then false else true) then (\x1. false) else (\x0. x0) ;;

if (if true then false else false) then (if false then false else true) else
if false then true else false ;;

if (if true then true else true) then true else if true then false else true ;;

(if
 (if (if false then true else true) then (if false then false else true) else
  if false then false else false)
 then (if (if true then false else false) then (\x8. x8) else (\x7. x7)) else
 if false then (\x6. x6) else (\x5. x5))
  ((\x3. \x4. x4)
     (if (if false then false else true) then
      (if false then false else false) else if true then false else false))
  ((\x2.
      if true then (if x2 then false else false) else
      if false then false else true)
     ((if false then (\x1. true) else (\x0. x0))
        (if (if true then true else true) then false else
         if false then false else true))) ;;

(\x2. \x3. true)
  ((if (if false then false else true) then (\x1. false) else (\x0. true))
     (if (if false then true else true) then (if false then false else true)
      else if false then false else false)) ;;

(if false then (\x1. x1) else (\x0. true))
  (if true then (if false then false else false) else
   if true then true else true) ;;

\x0.
  if (if x0 then x0 else true) then (if x0 then x0 else false) else
  if true then false else false ;;

(if false then (\x2. false) else (\x1. x1))
  ((\x0. if false then x0 else x0)
     (if true then (if false then false else true) else
      if false then true else true)) ;;

if (if (if true then true else true) then false else true) then
(if (if true then true else false) then (if false then false else false) else
 if true then false else true)
else
if (if false then false else true) then (if true then false else true) else
if false then false else false ;;

(if true then (\x1. true) else (\x0. x0))
  (if (if true then true else true) then (if false then true else false) else
   if true then true else true) ;;

(\x4.
   (if (if false then false else false) then (\x6. true) else (\x5. x5))
     (if (if false then false else true) then (if x4 then false else x4) else
      if x4 then x4 else true))
  ((if (if (if true then false else false) then false else false) then
    (if (if true then false else true) then (\x3. true) else (\x2. true))
    else (\x1. if x1 then true else x1))
     ((\x0. false)
        (if (if true then true else false) then false else
         if false then false else true))) ;;

(\x0. \x1. x1)
  (if (if false then false else true) then (if true then false else false)
   else if false then false else true) ;;

(if
 (if (if false then true else true) then (if false then false else true) else
  if false then false else false)
 then (if (if true then false else false) then (\x10. x10) else (\x9. x9))
 else if false then (\x8. x8) else (\x7. x7))
  ((\x5. \x6. x6)
     (if (if false then false else true) then
      (if false then false else false) else if true then false else false))
  ((if
    (if (if true then true else true) then (if false then true else false)
     else if false then false else false)
    then
    (if (if true then true else true) then (\x4. true) else (\x3. false))
    else if false then (\x2. false) else (\x1. true))
     ((\x0. false)
        (if (if true then true else true) then true else
         if false then true else true))) ;;

(\x3. \x4. if true then true else x4)
  ((if (if false then false else false) then (\x2. true) else (\x1. true))
     (\x0. if x0 then true else x0)) ;;

(\x1.
   if (if true then x1 else false) then (if x1 then false else x1) else
   if x1 then false else false)
  ((\x0. x0) (if true then false else if true then false else false)) ;;

if (if true then false else true) then (\x1. x1) else (\x0. false) ;;

(\x5. \x6. (\x7. x7) (if x6 then true else false))
  ((\x4. x4)
     (if (if true then false else false) then (\x3. true) else (\x2. true))
     ((if (if false then false else false) then (\x1. x1) else (\x0. false))
        (if (if true then true else true) then true else
         if false then true else true))) ;;

(\x0. \x1. x0)
  (if (if false then false else false) then (if true then false else false)
   else if true then true else true) ;;

if (if true then true else true) then true else
if false then false else false ;;

(\x3. \x4. true)
  (if (if false then false else false) then (if true then false else false)
   else if false then false else false)
  ((if true then (\x2. false) else (\x1. false))
     (\x0. if x0 then false else false)) ;;

\x0.
  if
  (if (if false then true else true) then (if false then x0 else true) else
   if false then false else x0)
  then
  (if (if x0 then x0 else true) then (if false then false else false) else x0)
  else
  if (if false then true else true) then (if true then x0 else x0) else
  if false then x0 else true ;;

(\x4. \x5. x5) (if false then (\x3. x3) else (\x2. x2))
  ((if (if false then false else true) then (\x1. false) else (\x0. x0))
     (if (if true then false else false) then (if false then true else true)
      else if false then false else false)) ;;

(\x2. \x3. true)
  (if (if true then false else true) then (\x1. false) else (\x0. false))
  (if
   (if (if false then true else true) then (if false then false else true)
    else if true then true else false)
   then
   (if true then (if false then true else true) else
    if true then false else false)
   else
   if (if true then false else false) then (if true then true else true) else
   if true then true else false) ;;

(if
 (if (if true then true else true) then false else
  if true then true else true)
 then (if (if true then true else false) then (\x10. x10) else (\x9. x9))
 else if true then (\x8. x8) else (\x7. x7))
  (\x5. (\x6. true) (if false then true else x5))
  ((if (if (if true then false else false) then false else false) then
    (if (if true then false else true) then (\x4. true) else (\x3. true))
    else (\x2. if x2 then true else x2))
     ((if true then (\x1. true) else (\x0. false))
        (if (if true then false else true) then
         (if false then false else false) else if true then false else true))) ;;

(if
 (if (if true then true else true) then (if true then false else true) else
  true)
 then (if true then (\x8. true) else (\x7. x7)) else
 if (if false then true else false) then (\x6. true) else (\x5. true))
  ((\x4. if false then x4 else x4)
     (if (if true then true else false) then (\x3. x3) else (\x2. false))
     ((if (if true then true else true) then (\x1. true) else (\x0. x0))
        (if (if true then true else false) then false else
         if false then false else true))) ;;

if (if false then false else true) then (if true then true else false) else
if false then true else true ;;

(if (if true then false else false) then (\x3. false) else (\x2. false))
  (if (if false then false else true) then (\x1. true) else (\x0. true)) ;;

\x0. \x1. x0 ;;

(if
 (if (if false then false else true) then (if true then true else false) else
  if true then true else false)
 then (if (if true then false else false) then (\x5. true) else (\x4. true))
 else (\x3. if x3 then true else x3))
  ((if true then (\x2. false) else (\x1. true))
     (\x0. if x0 then false else false)) ;;

(if (if false then (if true then true else true) else true) then
 (if (if false then false else true) then (\x5. false) else (\x4. false))
 else if (if true then false else true) then (\x3. x3) else (\x2. true))
  ((if (if true then false else false) then (\x1. true) else (\x0. false))
     (if (if true then true else false) then (if false then false else true)
      else true)) ;;

(if (if false then true else true) then (\x1. x1) else (\x0. true))
  (if (if false then true else false) then false else
   if true then true else true) ;;

(\x1. \x2. false)
  (if (if true then true else true) then true else
   if false then false else true)
  ((\x0. x0)
     (if (if false then false else true) then (if true then true else false)
      else if false then true else true)) ;;

if true then (if true then true else true) else if true then false else true ;;

(\x0. \x1. true)
  (if (if false then false else false) then (if true then false else false)
   else if false then false else false)
  (if
   (if true then (if false then true else true) else
    if true then true else true)
   then
   (if true then (if true then false else false) else
    if true then true else true)
   else
   if (if true then false else false) then (if true then false else true)
   else if true then false else true) ;;

if (if false then true else false) then (if true then true else false) else
if false then true else true ;;

if (if true then false else true) then (if false then false else false) else
if true then true else false ;;

if
(if (if true then false else false) then (\x4. true) else (\x3. true))
  ((\x2. x2) true)
then
(\x1.
   if (if x1 then true else x1) then false else if false then true else true)
else
(\x0.
   if (if false then x0 else true) then (if false then x0 else true) else
   if x0 then false else x0) ;;

(\x1. \x2. (\x3. x3) (if x2 then true else false))
  (\x0.
     if (if false then true else x0) then (if x0 then true else x0) else
     if x0 then true else false) ;;

(\x1. x1) (\x0. x0) ;;

(\x0. if false then false else true)
  (if
   (if (if false then true else true) then (if false then false else true)
    else if true then true else false)
   then (if (if false then false else true) then false else true) else
   if (if true then true else false) then (if false then false else false)
   else if false then false else true) ;;

(\x6. \x7. x7)
  (if false then (if true then true else false) else
   if false then true else false)
  ((if
    (if (if false then false else true) then (if true then false else false)
     else if false then false else true)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. true))
     ((if false then (\x1. x1) else (\x0. x0))
        (if (if true then true else true) then
         (if true then false else false) else if true then true else false))) ;;

(\x0. if true then true else x0)
  (if (if false then false else true) then (if false then true else false)
   else if false then true else true) ;;

(if
 (if (if false then false else true) then (if true then true else false) else
  if true then true else false)
 then (if (if true then false else false) then (\x3. true) else (\x2. true))
 else (\x1. if x1 then true else x1))
  ((\x0. x0) (if true then false else if true then false else false)) ;;

(if
 (if (if false then true else true) then (if false then true else false) else
  if false then true else true)
 then (if (if true then false else false) then (\x5. false) else (\x4. x4))
 else if false then (\x3. x3) else (\x2. x2))
  ((if (if true then true else false) then (\x1. x1) else (\x0. false))
     (if true then (if true then false else true) else
      if true then true else false)) ;;

(if (if true then false else false) then (\x1. x1) else (\x0. false))
  (if false then (if false then false else false) else
   if true then false else true) ;;

if true then (if false then false else true) else
if false then false else true ;;

\x0. (\x1. if false then true else x0) (if true then x0 else false) ;;

(if
 (if (if false then true else false) then (if false then true else false)
  else if false then false else true)
 then (if false then (\x5. x5) else (\x4. false)) else
 if (if false then true else true) then (\x3. false) else (\x2. true))
  ((if (if false then true else true) then (\x1. false) else (\x0. x0))
     (if (if false then false else false) then (if true then false else true)
      else true)) ;;

(\x2.
   (if (if x2 then x2 else x2) then (\x4. false) else (\x3. x3))
     (if (if true then false else x2) then (if x2 then x2 else true) else
      if true then false else true))
  ((\x0. (\x1. x0) true)
     (if true then false else if false then true else true)) ;;

(if (if true then false else true) then (\x8. x8) else (\x7. x7))
  (\x6. if x6 then true else false)
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. x2))
     ((if (if false then false else true) then (\x1. true) else (\x0. false))
        (if (if false then false else false) then
         (if true then false else false) else false))) ;;

(\x8. if true then x8 else if x8 then x8 else x8)
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then (if (if false then true else true) then (\x7. x7) else (\x6. x6))
    else if (if false then true else false) then (\x5. true) else (\x4. x4))
     ((if (if false then false else true) then (\x3. false) else (\x2. false))
        (if true then (\x1. x1) else (\x0. true)))) ;;

(\x3. \x4. false) ((\x2. false) (if false then false else false))
  ((if (if true then true else false) then (\x1. x1) else (\x0. false))
     (if true then (if true then false else true) else
      if true then true else false)) ;;

if (if true then false else true) then (if true then false else true) else
if false then true else false ;;

if (if (if false then false else true) then true else true) then
(if (if true then false else true) then (if true then true else true) else
 if false then false else true)
else
if (if false then true else false) then (if false then false else true) else
if true then false else true ;;

(\x0. if true then false else false)
  (if (if false then true else true) then (if true then false else false)
   else if true then false else true) ;;

(if (if true then false else false) then (\x1. x1) else (\x0. false))
  (if (if true then false else true) then (if false then false else false)
   else if true then true else true) ;;

(if (if false then false else true) then (\x1. true) else (\x0. true))
  (if (if false then false else true) then (if false then false else false)
   else if false then false else true) ;;

(\x0. if x0 then false else false)
  (if (if true then false else true) then (if false then false else false)
   else if false then true else true) ;;

(if (if false then true else false) then (\x1. true) else (\x0. false))
  (if (if false then true else true) then (if false then true else true) else
   if false then false else true) ;;

if (if true then true else true) then (if true then false else true) else
if false then false else true ;;

(if
 (if (if false then true else false) then (if true then false else false)
  else if false then true else true)
 then (if false then (\x5. true) else (\x4. true)) else
 if (if false then true else false) then (\x3. true) else (\x2. x2))
  ((if (if true then false else true) then (\x1. false) else (\x0. true))
     (if (if false then true else true) then (if true then false else true)
      else if false then true else false)) ;;

(\x5. (\x6. x5) (if false then false else true))
  ((if false then (\x4. x4) else (\x3. x3))
     (if (if false then true else false) then (\x2. false) else (\x1. x1))
     ((\x0. if true then true else x0)
        (if true then false else if true then true else false))) ;;

if (if false then false else false) then (if false then true else false) else
if true then false else false ;;

(\x2. \x3. false)
  (if (if true then true else true) then true else
   if false then false else true)
  ((if (if false then false else false) then (\x1. x1) else (\x0. x0))
     (if (if false then false else false) then (if false then true else true)
      else if false then true else true)) ;;

(if (if false then true else true) then (\x1. true) else (\x0. false))
  (if (if false then false else false) then (if false then false else true)
   else if false then true else true) ;;

(if
 (\x11. x11)
   (if (if false then true else true) then true else
    if false then false else true)
 then
 (if
  (if (if true then true else true) then (if true then true else false) else
   if true then false else true)
  then
  (if (if false then false else false) then (\x10. true) else (\x9. true))
  else if (if false then false else false) then (\x8. true) else (\x7. false))
 else
 (\x6.
    if (if false then x6 else true) then (if true then false else true) else
    if false then false else false))
  ((if
    (if (if false then false else true) then (if true then false else false)
     else if false then false else true)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. true))
     ((if false then (\x1. x1) else (\x0. x0))
        (if (if true then true else true) then
         (if true then false else false) else if true then true else false))) ;;

\x0.
  if (if x0 then false else x0) then (if x0 then true else x0) else
  if true then false else false ;;

(if (if false then true else false) then (\x1. true) else (\x0. true))
  (if true then (if false then true else true) else true) ;;

\x0.
  (\x2. if x2 then x0 else x0)
    ((\x1. if true then x0 else false)
       (if (if false then false else false) then
        (if false then false else false) else if true then true else x0)) ;;

(if (if false then false else true) then (\x1. x1) else (\x0. false))
  (if (if false then true else true) then false else
   if false then false else false) ;;

(if
 (if
  (if (if false then false else false) then (if true then false else false)
   else if true then false else true)
  then
  (if (if true then true else true) then (if false then false else false)
   else if false then true else true)
  else
  if (if true then true else false) then true else
  if false then false else false)
 then
 (if
  (if (if false then true else false) then (if true then false else false)
   else if false then false else false)
  then (if (if false then true else true) then (\x11. true) else (\x10. x10))
  else if (if false then false else true) then (\x9. false) else (\x8. x8))
 else
 if
 (if (if false then false else true) then (if true then true else true) else
  if true then true else false)
 then (\x7. if true then false else false) else
 if (if false then false else false) then (\x6. x6) else (\x5. x5))
  ((\x4. x4)
     (if (if true then false else true) then (\x3. true) else (\x2. true))
     ((if false then (\x1. false) else (\x0. false))
        (if (if true then true else true) then
         (if false then false else true) else if false then true else true))) ;;

(if
 (if (if false then true else true) then (if false then false else true) else
  if false then false else false)
 then (if (if true then false else false) then (\x6. x6) else (\x5. x5)) else
 if false then (\x4. x4) else (\x3. x3))
  ((\x1. \x2. x2)
     (if (if false then false else true) then
      (if false then false else false) else if true then false else false))
  ((\x0. if true then true else x0)
     (if (if false then true else false) then (if false then true else true)
      else if false then true else false)) ;;

\x0.
  if (if false then true else false) then (if x0 then x0 else false) else
  if true then true else true ;;

(if
 (if (if false then false else false) then (if false then false else false)
  else if true then false else true)
 then
 (if (if false then true else false) then (\x8. false) else (\x7. false))
 else (\x6. if true then true else x6))
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. x2))
     ((if (if true then true else true) then (\x1. false) else (\x0. x0))
        (if true then false else false))) ;;

if (if false then true else false) then true else
if true then false else true ;;

(if
 (if (if false then false else true) then (if false then true else true) else
  true)
 then (if (if false then false else false) then (\x7. false) else (\x6. x6))
 else if true then (\x5. true) else (\x4. false))
  ((\x2. (\x3. true) (if x2 then x2 else false))
     ((if (if false then true else true) then (\x1. true) else (\x0. false))
        (if (if false then false else false) then
         (if true then false else false) else false))) ;;

\x0.
  if (if x0 then false else x0) then (if true then true else x0) else
  if false then false else false ;;

if (if false then false else false) then (if true then false else false) else
if false then true else true ;;

\x0. (\x1. x0) (if true then false else x0) ;;

(if (if true then false else true) then (\x8. x8) else (\x7. x7))
  (\x6. if x6 then true else false)
  ((if
    (if (if false then true else false) then (if false then false else true)
     else if false then true else true)
    then (if false then (\x5. true) else (\x4. true)) else
    if (if false then true else false) then (\x3. x3) else (\x2. false))
     ((if true then (\x1. false) else (\x0. true))
        (if (if true then false else false) then
         (if false then false else true) else if false then false else false))) ;;

(if
 (if false then (\x10. x10) else (\x9. x9))
   (if (if false then true else false) then (if true then true else true)
    else if true then false else false)
 then
 (if
  (if (if true then true else true) then (if true then true else false) else
   if true then false else true)
  then
  (if (if false then false else false) then (\x8. true) else (\x7. true))
  else if (if false then false else false) then (\x6. true) else (\x5. false))
 else
 (\x4.
    if (if true then true else true) then (if true then false else true) else
    if true then x4 else true))
  (if
   (if (if false then true else true) then (\x3. true) else (\x2. true))
     (if (if true then false else false) then (if false then false else true)
      else if true then false else true)
   then
   (if (if true then true else false) then (\x1. false) else (\x0. true))
     (if (if false then false else true) then (if true then false else false)
      else if true then false else true)
   else
   if (if (if true then true else false) then false else true) then
   (if (if false then false else false) then (if true then false else false)
    else if true then true else false)
   else
   if (if true then true else false) then (if false then true else false)
   else false) ;;

(\x6. \x7. false)
  (if (if false then true else true) then (if true then false else true) else
   if false then true else true)
  ((if (if (if true then false else false) then false else false) then
    (if (if true then false else true) then (\x5. false) else (\x4. false))
    else if (if true then true else true) then (\x3. true) else (\x2. false))
     ((if (if false then true else false) then (\x1. false) else (\x0. false))
        (if false then (if false then false else false) else true))) ;;

(if
 (if (if false then true else true) then (if false then false else false)
  else if true then true else false)
 then (if true then (\x9. true) else (\x8. x8)) else
 if (if false then true else false) then (\x7. true) else (\x6. true))
  ((if (if false then (if true then true else false) else true) then
    (if (if false then true else true) then (\x5. false) else (\x4. x4)) else
    if false then (\x3. false) else (\x2. true))
     ((if true then (\x1. x1) else (\x0. false))
        (if true then false else true))) ;;

(if (if false then false else true) then (\x1. true) else (\x0. false))
  (if (if false then false else false) then (if true then false else true)
   else if false then false else false) ;;

(\x2.
   if (if x2 then true else true) then (if false then false else false) else
   if x2 then false else false)
  ((if (if true then false else true) then (\x1. true) else (\x0. false))
     (if (if true then false else false) then (if true then false else true)
      else false)) ;;

if false then false else if false then false else false ;;

(if (if false then true else true) then (\x1. true) else (\x0. x0))
  (if (if false then false else false) then true else
   if true then true else true) ;;

(if (if false then true else false) then (\x1. false) else (\x0. false))
  (if false then (if false then false else true) else
   if true then false else true) ;;

(if (if false then false else false) then (\x1. false) else (\x0. x0))
  (if (if true then true else false) then (if true then false else true) else
   if false then true else false) ;;

(if (if false then false else false) then (\x1. false) else (\x0. x0))
  (if (if false then false else false) then (if false then false else true)
   else if false then true else true) ;;

(if (if false then true else true) then (\x1. true) else (\x0. false))
  (if (if true then true else true) then false else
   if false then false else false) ;;

if (if true then false else true) then (if false then true else true) else
if false then true else false ;;

(if (if false then true else true) then (\x1. x1) else (\x0. true))
  (if (if false then false else false) then (if false then false else true)
   else if false then true else true) ;;

(if (if false then true else false) then (\x5. x5) else (\x4. x4))
  (if (if true then false else true) then (\x3. x3) else (\x2. x2))
  ((if (if true then true else false) then (\x1. x1) else (\x0. x0))
     (if (if true then false else true) then (if false then true else true)
      else true)) ;;

(\x0. \x1. x1)
  (if false then (if true then false else true) else
   if false then true else false) ;;

(\x6. \x7. x6) (if false then false else false)
  ((if
    (if (if false then false else true) then (if true then false else false)
     else if false then false else true)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. true))
     ((if false then (\x1. x1) else (\x0. x0))
        (if (if true then true else true) then
         (if true then false else false) else if true then true else false))) ;;

\x0. \x1. if x1 then x0 else x0 ;;

(if (if true then false else true) then (\x1. x1) else (\x0. x0))
  (if (if false then true else true) then (if false then true else false)
   else if false then true else false) ;;

(\x0.
   if (if false then true else x0) then (if true then true else false) else
   if x0 then true else x0)
  (if (if false then false else false) then (if true then true else true)
   else if false then false else false) ;;

if (if true then false else true) then (if false then false else false) else
if true then true else true ;;

if
(\x3. if false then false else x3)
  (if (if true then true else false) then (if false then true else false)
   else if true then false else false)
then
(if (if true then true else false) then (\x2. false) else (\x1. true))
  (if (if true then false else true) then (if false then false else false)
   else if true then false else true)
else
(\x0. if true then true else x0)
  (if (if true then false else true) then (if true then false else true) else
   if false then true else true) ;;

(\x0. if true then x0 else false)
  (if (if false then false else false) then true else
   if false then false else true) ;;

(if (if false then true else true) then (\x5. x5) else (\x4. x4))
  (if true then (\x3. x3) else (\x2. false))
  ((if (if true then false else false) then (\x1. true) else (\x0. false))
     (if (if true then true else false) then (if false then false else true)
      else true)) ;;

(\x1. \x2. false) ((\x0. false) (if false then false else false))
  (if
   (if true then (if false then true else true) else
    if true then true else true)
   then
   (if true then (if true then false else false) else
    if true then true else true)
   else
   if (if true then false else false) then (if true then false else true)
   else if true then false else true) ;;

\x0.
  (if (if x0 then x0 else x0) then (\x2. false) else (\x1. true))
    (if (if x0 then false else false) then (if x0 then x0 else x0) else
     if true then false else true) ;;

if
(\x8. if (if x8 then true else false) then x8 else if x8 then true else true)
  ((if (if true then true else false) then (\x7. true) else (\x6. x6))
     (if (if false then true else false) then (if false then true else false)
      else if true then false else false))
then
(\x4. \x5. true)
  (if true then (if true then true else true) else
   if false then false else false)
  ((\x3. if x3 then false else true)
     (if (if true then false else false) then (if true then false else false)
      else if true then true else true))
else
(\x2.
   if (if true then true else true) then (if false then false else false)
   else if true then x2 else true)
  ((if (if false then true else false) then (\x1. x1) else (\x0. x0))
     (if (if false then true else true) then (if false then false else true)
      else if false then false else false)) ;;

(\x0. if false then true else true)
  (if (if false then false else true) then (if true then false else false)
   else if false then false else true) ;;

if (if true then false else true) then (if false then true else true) else
if true then true else false ;;

(if true then (\x1. x1) else (\x0. x0))
  (if false then (if false then false else false) else
   if true then false else true) ;;

if (if false then false else false) then (if true then false else true) else
if false then true else false ;;

\x0.
  if (if x0 then false else x0) then (if x0 then false else true) else
  if true then true else false ;;

if (if true then false else true) then (if false then false else false) else
if true then false else false ;;

if (if true then true else false) then (if false then false else true) else
if false then false else false ;;

(\x5.
   (if (if true then x5 else true) then (\x7. true) else (\x6. true))
     (if (if true then true else false) then (if x5 then false else x5) else
      x5))
  ((if false then (\x4. x4) else (\x3. x3))
     (if (if false then true else false) then (\x2. false) else (\x1. x1))
     ((\x0. if true then true else x0)
        (if true then false else if true then true else false))) ;;

if
(if (if false then true else true) then (if true then true else false) else
 if true then true else true)
then
(if (if false then true else true) then false else
 if true then false else true)
else
if (if false then true else false) then true else
if true then false else false ;;

if
(\x4. if x4 then false else x4)
  (if (if false then true else true) then true else
   if false then false else true)
then
(if (if false then false else false) then (\x3. x3) else (\x2. false))
  (if false then true else if false then false else false)
else
(if (if false then true else false) then (\x1. true) else (\x0. false))
  (if (if true then true else true) then (if true then true else false) else
   true) ;;

if (if true then false else true) then false else
if true then true else false ;;

(\x2. \x3. true)
  (if true then (if true then true else false) else
   if true then false else true)
  ((if (if false then false else true) then (\x1. false) else (\x0. true))
     (if (if false then true else true) then (if false then false else true)
      else if false then false else false)) ;;

(\x5. \x6. (\x7. x7) (if x6 then true else false))
  ((if false then (\x4. x4) else (\x3. x3))
     (if (if false then true else false) then (\x2. false) else (\x1. x1))
     (if
      (if (if true then true else false) then false else
       if false then true else true)
      then (\x0. true) (if true then true else true) else
      if (if false then true else true) then false else
      if true then false else true)) ;;

(\x1.
   (if (if true then false else false) then (\x3. x3) else (\x2. true))
     (if (if true then true else false) then (if x1 then x1 else true) else
      if x1 then x1 else x1))
  ((\x0. if true then true else x0)
     (if (if false then true else false) then (if false then true else true)
      else if false then true else false)) ;;

(if (if false then false else false) then (\x1. false) else (\x0. false))
  (if true then (if false then false else false) else
   if true then true else true) ;;

if (if false then true else false) then (if true then true else true) else
false ;;

if (if true then false else true) then (\x1. x1) else (\x0. true) ;;

(if
 (if (if false then false else true) then (if false then true else true) else
  true)
 then (if (if false then false else false) then (\x9. false) else (\x8. x8))
 else if true then (\x7. true) else (\x6. false))
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. x2))
     ((if (if false then false else true) then (\x1. true) else (\x0. false))
        (if (if false then false else false) then
         (if true then false else false) else false))) ;;

if (if (if true then true else true) then false else true) then
(if (if false then true else false) then (if false then false else true) else
 if false then true else false)
else if false then (if true then true else true) else true ;;

if
(\x10.
   if (if true then false else false) then x10 else
   if false then true else x10)
  ((\x9. if false then x9 else x9)
     (if (if true then false else true) then (if true then true else true)
      else if true then true else true))
then
(if
 (\x8. x8) (\x7. x7)
   (if (if false then true else true) then (if true then false else false)
    else true)
 then
 (if (if false then false else false) then (\x6. false) else (\x5. x5))
   (if (if false then false else true) then (if false then true else true)
    else true)
 else
 (if (if true then false else true) then (\x4. x4) else (\x3. true))
   (if (if false then true else false) then (if false then false else false)
    else if true then true else true))
else
(\x2.
   if (if true then true else true) then (if false then false else false)
   else if true then x2 else true)
  ((if (if false then true else false) then (\x1. x1) else (\x0. x0))
     (if (if false then true else true) then (if false then false else true)
      else if false then false else false)) ;;

if false then true else if false then true else true ;;

(\x2. \x3. true)
  ((if (if false then false else false) then (\x1. x1) else (\x0. true))
     (if (if true then false else true) then (if true then true else false)
      else if true then false else false)) ;;

(if
 (\x8. x8)
   (if (if false then true else true) then true else
    if false then false else true)
 then
 (if
  (if (if true then true else true) then (if true then true else false) else
   if true then false else true)
  then
  (if (if false then false else false) then (\x7. true) else (\x6. true))
  else if (if false then false else false) then (\x5. true) else (\x4. false))
 else
 (\x3.
    if (if false then x3 else true) then (if true then false else true) else
    if false then false else false))
  ((\x2.
      if (if true then false else x2) then (if x2 then false else false) else
      if x2 then true else x2)
     ((if (if false then false else false) then (\x1. x1) else (\x0. true))
        (if false then (if false then false else true) else
         if true then false else false))) ;;

(\x0. \x1. x1)
  (if (if true then true else true) then (if false then false else false)
   else if false then false else false) ;;

\x0.
  \x1.
    if (if false then true else true) then (if x1 then false else true) else
    if x0 then false else x1 ;;

if true then (\x1. true) else (\x0. x0) ;;

(\x0. \x1. if true then true else x1)
  (if
   (if (if true then true else false) then (if true then true else true) else
    true)
   then (if (if false then true else true) then true else true) else
   if (if true then false else false) then (if true then false else true)
   else if true then false else true) ;;

(\x7. \x8. if true then false else x7)
  ((if (if false then true else true) then (\x6. x6) else (\x5. true))
     (if (if false then false else true) then (if true then true else true)
      else if true then false else false))
  ((if (if false then true else false) then (\x4. x4) else (\x3. x3))
     (if (if false then true else false) then (\x2. false) else (\x1. x1))
     ((\x0. if x0 then x0 else x0)
        (if (if false then true else true) then false else
         if false then false else true))) ;;

if (if false then false else false) then (if false then false else false)
else if true then true else false ;;

(if (if false then true else true) then (\x3. x3) else (\x2. x2))
  (if (if false then false else false) then (\x1. true) else (\x0. true)) ;;

(\x2. \x3. true)
  ((if (if true then false else false) then (\x1. true) else (\x0. false))
     (if (if true then true else false) then (if false then false else true)
      else true)) ;;

(\x0. if true then x0 else false) (if true then true else true) ;;

(\x6. \x7. if x7 then x7 else false)
  (if (if true then false else false) then false else
   if true then true else true)
  ((if
    (if (if false then true else false) then (if false then true else false)
     else if true then true else true)
    then (if (if false then true else true) then (\x5. x5) else (\x4. x4))
    else if false then (\x3. false) else (\x2. false))
     ((if (if false then false else false) then (\x1. x1) else (\x0. true))
        (if false then (if false then false else true) else
         if true then false else false))) ;;

(\x5.
   (if (if x5 then false else false) then (\x7. true) else (\x6. true))
     (if (if true then true else true) then (if x5 then true else false) else
      if true then x5 else false))
  ((if false then (\x4. x4) else (\x3. x3))
     (if (if false then true else false) then (\x2. false) else (\x1. x1))
     ((\x0. false)
        (if (if true then true else false) then false else
         if false then false else true))) ;;

if false then (if false then false else false) else
if true then true else true ;;

(\x5. \x6. if x6 then x6 else x6)
  ((if
    (if true then (if true then true else false) else
     if false then false else false)
    then
    (if (if true then true else true) then (\x4. false) else (\x3. true))
    else if (if true then true else true) then (\x2. true) else (\x1. false))
     (if
      (if (if true then true else false) then false else
       if false then true else true)
      then (\x0. true) (if true then true else true) else
      if (if false then true else true) then false else
      if true then false else true)) ;;

(\x0. \x1. true)
  (if true then (if false then false else false) else
   if true then true else true) ;;

(\x5. \x6. false)
  (if (if true then false else true) then (\x4. true) else (\x3. x3))
  ((\x2. x2)
     (if (if false then true else false) then (\x1. false) else (\x0. false))
     (if (if true then false else false) then (if false then true else false)
      else true)) ;;

\x0.
  (\x1. if false then x0 else x0)
    (if (if false then true else false) then (if false then true else x0)
     else if x0 then x0 else false) ;;

(\x1.
   if true then (if x1 then false else x1) else if false then x1 else false)
  ((\x0. false)
     (if (if false then true else false) then (if false then true else false)
      else if true then true else false)) ;;

(\x8. \x9. if true then false else x8)
  ((if (if true then false else false) then (\x7. false) else (\x6. x6))
     (if false then (if false then true else true) else
      if false then true else true))
  ((if
    (if (if false then false else true) then (if true then false else false)
     else if false then false else true)
    then
    (if (if true then false else true) then (\x5. true) else (\x4. true))
    else if (if false then true else false) then (\x3. true) else (\x2. true))
     ((if false then (\x1. x1) else (\x0. x0))
        (if (if true then true else true) then
         (if true then false else false) else if true then true else false))) ;;

(if (if false then true else true) then (\x1. false) else (\x0. false))
  (if (if true then false else true) then true else
   if false then false else true) ;;

\x0.
  (if (if false then true else x0) then (\x2. x2) else (\x1. true))
    (if false then false else x0) ;;

if false then (\x1. false) else (\x0. x0) ;;

(if (if true then false else false) then (\x1. x1) else (\x0. false))
  (if (if true then false else true) then (if false then true else false)
   else if true then true else true) ;;

(if
 (if (if true then true else true) then false else
  if true then true else true)
 then (if (if true then true else false) then (\x10. x10) else (\x9. x9))
 else if true then (\x8. x8) else (\x7. x7))
  (\x5. (\x6. true) (if false then true else x5))
  ((if (if false then true else true) then (\x4. x4) else (\x3. x3))
     (if (if false then false else false) then (\x2. false) else (\x1. x1))
     (if
      (if (if true then false else true) then false else
       if false then true else true)
      then (\x0. true) (if true then true else true) else
      if (if true then true else true) then (if true then false else false)
      else if true then true else true)) ;;

(if true then (\x1. x1) else (\x0. x0))
  (if false then (if false then true else true) else
   if false then true else true) ;;

(if (if true then false else true) then (\x7. x7) else (\x6. x6))
  (\x5. if x5 then true else false)
  ((\x3. (\x4. true) (if x3 then x3 else false))
     ((if (if false then false else false) then (\x2. true) else (\x1. true))
        (\x0. if false then true else true))) ;;

\x0.
  (if (if true then true else true) then (\x2. true) else (\x1. x0))
    (if (if x0 then x0 else x0) then (if true then true else false) else
     if true then false else true) ;;

if
(\x4. if true then true else true)
  (if false then (if false then true else true) else
   if true then true else false)
then
(if (if false then false else false) then (\x3. true) else (\x2. false))
  (if (if true then false else false) then (if false then false else false)
   else if false then true else true)
else
(if (if false then false else true) then (\x1. false) else (\x0. true))
  (if (if false then true else true) then (if false then true else true) else
   false) ;;

(if (if true then false else true) then (\x1. true) else (\x0. x0))
  (if (if false then false else false) then false else true) ;;

if
(if
 (if (if false then false else true) then (if true then true else true) else
  if true then false else true)
 then (if false then (\x14. false) else (\x13. true)) else
 if (if false then false else false) then (\x12. true) else (\x11. true))
  ((if (if false then false else false) then (\x10. true) else (\x9. true))
     (if (if true then true else false) then (if false then false else true)
      else if true then false else false))
then
(if
 (\x8. x8) (\x7. x7)
   (if (if false then true else true) then (if true then false else false)
    else true)
 then
 (if (if false then false else false) then (\x6. false) else (\x5. x5))
   (if (if false then false else true) then (if false then true else true)
    else true)
 else
 (if (if true then false else true) then (\x4. x4) else (\x3. true))
   (if (if false then true else false) then (if false then false else false)
    else if true then true else true))
else
(\x2.
   if (if true then true else true) then (if false then false else false)
   else if true then x2 else true)
  ((if (if true then true else true) then (\x1. false) else (\x0. false))
     (if (if false then false else false) then
      (if false then false else false) else if true then false else false)) ;;