Solving Logic Puzzles with the Laws of Form Notation

We can use the following functions to build up forms that represent electronic circuits and logical statements:

In [1]:
nor = lambda *bits: bits
or_ = lambda *bits: nor(bits)
and_ = lambda *bits: tuple(nor(bit) for bit in bits)
nand = lambda *bits: nor(and_(*bits))
eqiv = lambda *bits: (bits, and_(*bits))
xor = lambda *bits: nor(eqiv(*bits))

An expression composed of tuples and strings, which serve as logical symbols or variables, can be transformed into a standard form.

In [2]:
def reify(meaning, form):
  if isinstance(form, basestring):
    return meaning.get(form, form)
  return tuple(reify(meaning, inner) for inner in form)
In [3]:
def standard_form(x, form):
  Ex = reify({x: ((),)}, form)
  E_x_ = reify({x: ()}, form)
  return (x, Ex), ((x,), E_x_)

It is also helpful to be able to simply forms. We can use functions like these to reduce forms according to the Bricken basis.

In [4]:
def unwrap(form):
  '''
  Remove all (()) and let ((*)) -> * in a form. Generator.
  '''
  for term in form:
    if term == ((),):
      continue
    if isinstance(term, tuple) and len(term) == 1 and isinstance(term[0], tuple):
      # Flatten out one "layer" of "wrapping".
      for item in term[0]:
        yield item
      continue
    yield term
In [5]:
_A = lambda form: form if isinstance(form, basestring) else tuple(unwrap(form))
_B = lambda form: form if isinstance(form, basestring) else ((),) if () in form else form
In [6]:
def Reduce(form):
  if isinstance(form, basestring):
    return form
  if len(form) == 1 and isinstance(form[0], tuple) and len(form[0]) == 1:
    return Reduce(form[0][0])
  return tuple(_A(_B(tuple(map(Reduce, form)))))

This is a helper function to find all the symbols in a form.

In [7]:
def collect_names(form, names=None):
  if names is None:
    names = set()
  if isinstance(form, basestring):
    names.add(form)
  else:
    for inner in form:
      collect_names(inner, names)
  return names

This is a helper function to generate a nice string representation of a form.

In [8]:
to_string = lambda term: (str(term)
                  .replace(' ', '')
                  .replace("','", ' ')
                  .replace("'", '')
                  .replace(',', '')
                  .replace('(())', '◎')
                  .replace('()', '○')
                  )

This function applies the standard_form() function to a form for each of the names in the form. It also prints out the result at each stage for our edification.

In [9]:
def fstan(form):
  for name in sorted(collect_names(form)):
    form = Reduce(standard_form(name, form))
    print name, to_string(form) ; print
  return form

Now we can solve a logic puzzle. The following is based on George Burnett-Stuart's Exposition on Lewis Carroll's Five Liar Problem, which in turn is based on William Bricken's article. In this case the process of mechanically computing the full standard form of the puzzle is sufficient to discover the two solutions of the puzzle. I do not know under what circumstances this will always be true.

In [10]:
a, b, c, d, e, f, g, h, i, j = 'abcdefghij'
In [11]:
tale = {
  a: eqiv(xor(b, g), eqiv(d, i)),  # same as xor(xor(b, g), xor(d, i)) etc...
  f: xor(nand(c, h), nand(e, j)),

  b: eqiv(xor(a, f), eqiv(c, h)),
  g: xor(nand(d, i), or_(e, j)),

  c: xor(or_(a, f), or_(d, i)),
  h: xor(xor(b, g), nand(e, j)),

  d: xor(nand(a, f), nand(e, j)),
  i: xor(nand(b, g), or_(c, h)),

  e: xor(or_(a, f), or_(b, g)),
  j: eqiv(xor(c, h), eqiv(d, i)),
  }
In [12]:
E = or_(*(eqiv(name, expr) for name, expr in tale.iteritems()))
print to_string(E)
((((a(((((b g)((b)(g))))((d i)((d)(i))))(((((b g)((b)(g)))))(((d i)((d)(i)))))))((a)((((((b g)((b)(g))))((d i)((d)(i))))(((((b g)((b)(g)))))(((d i)((d)(i)))))))))((c(((((a f))((d i)))((((a f)))(((d i)))))))((c)((((((a f))((d i)))((((a f)))(((d i)))))))))((b(((((a f)((a)(f))))((c h)((c)(h))))(((((a f)((a)(f)))))(((c h)((c)(h)))))))((b)((((((a f)((a)(f))))((c h)((c)(h))))(((((a f)((a)(f)))))(((c h)((c)(h)))))))))((e(((((a f))((b g)))((((a f)))(((b g)))))))((e)((((((a f))((b g)))((((a f)))(((b g)))))))))((d((((((a)(f)))(((e)(j))))(((((a)(f))))((((e)(j))))))))((d)(((((((a)(f)))(((e)(j))))(((((a)(f))))((((e)(j))))))))))((g((((((d)(i)))((e j)))(((((d)(i))))(((e j)))))))((g)(((((((d)(i)))((e j)))(((((d)(i))))(((e j)))))))))((f((((((c)(h)))(((e)(j))))(((((c)(h))))((((e)(j))))))))((f)(((((((c)(h)))(((e)(j))))(((((c)(h))))((((e)(j))))))))))((i((((((b)(g)))((c h)))(((((b)(g))))(((c h)))))))((i)(((((((b)(g)))((c h)))(((((b)(g))))(((c h)))))))))((h((((((b g)((b)(g))))(((e)(j))))(((((b g)((b)(g)))))((((e)(j))))))))((h)(((((((b g)((b)(g))))(((e)(j))))(((((b g)((b)(g)))))((((e)(j))))))))))((j(((((c h)((c)(h))))((d i)((d)(i))))(((((c h)((c)(h)))))(((d i)((d)(i)))))))((j)((((((c h)((c)(h))))((d i)((d)(i))))(((((c h)((c)(h)))))(((d i)((d)(i)))))))))))
In [13]:
print to_string(Reduce(E))
((((a(((b g)((b)(g))((d i)((d)(i))))(((b g)((b)(g)))(d i)((d)(i)))))((a)((b g)((b)(g))((d i)((d)(i))))(((b g)((b)(g)))(d i)((d)(i)))))((c(a f d i)((a f)(d i)))((c)((a f d i)((a f)(d i)))))((b(((a f)((a)(f))((c h)((c)(h))))(((a f)((a)(f)))(c h)((c)(h)))))((b)((a f)((a)(f))((c h)((c)(h))))(((a f)((a)(f)))(c h)((c)(h)))))((e(a f b g)((a f)(b g)))((e)((a f b g)((a f)(b g)))))((d((a)(f)(e)(j))(((a)(f))((e)(j))))((d)(((a)(f)(e)(j))(((a)(f))((e)(j))))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f((c)(h)(e)(j))(((c)(h))((e)(j))))((f)(((c)(h)(e)(j))(((c)(h))((e)(j))))))((i((b)(g)c h)(((b)(g))(c h)))((i)(((b)(g)c h)(((b)(g))(c h)))))((h((b g)((b)(g))(e)(j))(((b g)((b)(g)))((e)(j))))((h)(((b g)((b)(g))(e)(j))(((b g)((b)(g)))((e)(j))))))((j(((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i)))))((j)((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i)))))))
In [14]:
Z = fstan(E)
a ((a(((b g)((b)(g))((d i)((d)(i))))(((b g)((b)(g)))(d i)((d)(i))))((c(f d i)((f)(d i)))((c)((f d i)((f)(d i)))))((b(((f)((c h)((c)(h))))(f(c h)((c)(h)))))((b)((f)((c h)((c)(h))))(f(c h)((c)(h)))))((e(f b g)((f)(b g)))((e)((f b g)((f)(b g)))))((d(e)(j))((d)((e)(j))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f((c)(h)(e)(j))(((c)(h))((e)(j))))((f)(((c)(h)(e)(j))(((c)(h))((e)(j))))))((i((b)(g)c h)(((b)(g))(c h)))((i)(((b)(g)c h)(((b)(g))(c h)))))((h((b g)((b)(g))(e)(j))(((b g)((b)(g)))((e)(j))))((h)(((b g)((b)(g))(e)(j))(((b g)((b)(g)))((e)(j))))))((j(((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i)))))((j)((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i))))))((a)((b g)((b)(g))((d i)((d)(i))))(((b g)((b)(g)))(d i)((d)(i)))((c d i)((c)(d i)))((b((f((c h)((c)(h))))((f)(c h)((c)(h)))))((b)(f((c h)((c)(h))))((f)(c h)((c)(h)))))((e b g)((e)(b g)))((d((f)(e)(j))(f((e)(j))))((d)(((f)(e)(j))(f((e)(j))))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f((c)(h)(e)(j))(((c)(h))((e)(j))))((f)(((c)(h)(e)(j))(((c)(h))((e)(j))))))((i((b)(g)c h)(((b)(g))(c h)))((i)(((b)(g)c h)(((b)(g))(c h)))))((h((b g)((b)(g))(e)(j))(((b g)((b)(g)))((e)(j))))((h)(((b g)((b)(g))(e)(j))(((b g)((b)(g)))((e)(j))))))((j(((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i)))))((j)((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i)))))))

b ((b((a(((g)((d i)((d)(i))))(g(d i)((d)(i))))((c(f d i)((f)(d i)))((c)((f d i)((f)(d i)))))(((f)((c h)((c)(h))))(f(c h)((c)(h))))((e(f g)((f)(g)))((e)((f g)((f)(g)))))((d(e)(j))((d)((e)(j))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f((c)(h)(e)(j))(((c)(h))((e)(j))))((f)(((c)(h)(e)(j))(((c)(h))((e)(j))))))((i c h)((i)(c h)))((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j(((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i)))))((j)((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i))))))((a)((g)((d i)((d)(i))))(g(d i)((d)(i)))((c d i)((c)(d i)))((f((c h)((c)(h))))((f)(c h)((c)(h))))((e g)((e)(g)))((d((f)(e)(j))(f((e)(j))))((d)(((f)(e)(j))(f((e)(j))))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f((c)(h)(e)(j))(((c)(h))((e)(j))))((f)(((c)(h)(e)(j))(((c)(h))((e)(j))))))((i c h)((i)(c h)))((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j(((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i)))))((j)((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i))))))))((b)((a((g((d i)((d)(i))))((g)(d i)((d)(i))))((c(f d i)((f)(d i)))((c)((f d i)((f)(d i)))))((f)((c h)((c)(h))))(f(c h)((c)(h)))((e f)((e)(f)))((d(e)(j))((d)((e)(j))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f((c)(h)(e)(j))(((c)(h))((e)(j))))((f)(((c)(h)(e)(j))(((c)(h))((e)(j))))))((i((g)c h)(g(c h)))((i)(((g)c h)(g(c h)))))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j(((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i)))))((j)((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i))))))((a)(g((d i)((d)(i))))((g)(d i)((d)(i)))((c d i)((c)(d i)))(f((c h)((c)(h))))((f)(c h)((c)(h)))(e)((d((f)(e)(j))(f((e)(j))))((d)(((f)(e)(j))(f((e)(j))))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f((c)(h)(e)(j))(((c)(h))((e)(j))))((f)(((c)(h)(e)(j))(((c)(h))((e)(j))))))((i((g)c h)(g(c h)))((i)(((g)c h)(g(c h)))))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j(((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i)))))((j)((c h)((c)(h))((d i)((d)(i))))(((c h)((c)(h)))(d i)((d)(i)))))))))

c ((c((b((a(((g)((d i)((d)(i))))(g(d i)((d)(i))))(f d i)((f)(d i))(((f)h)(f(h)))((e(f g)((f)(g)))((e)((f g)((f)(g)))))((d(e)(j))((d)((e)(j))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f(e)(j))((f)((e)(j))))((i h)((i)(h)))((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j(((h)((d i)((d)(i))))(h(d i)((d)(i)))))((j)((h)((d i)((d)(i))))(h(d i)((d)(i))))))((a)((g)((d i)((d)(i))))(g(d i)((d)(i)))d i((f h)((f)(h)))((e g)((e)(g)))((d((f)(e)(j))(f((e)(j))))((d)(((f)(e)(j))(f((e)(j))))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f(e)(j))((f)((e)(j))))((i h)((i)(h)))((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j(((h)((d i)((d)(i))))(h(d i)((d)(i)))))((j)((h)((d i)((d)(i))))(h(d i)((d)(i))))))))((b)((a((g((d i)((d)(i))))((g)(d i)((d)(i))))(f d i)((f)(d i))((f)h)(f(h))((e f)((e)(f)))((d(e)(j))((d)((e)(j))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f(e)(j))((f)((e)(j))))((i((g)h)(g(h)))((i)(((g)h)(g(h)))))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j(((h)((d i)((d)(i))))(h(d i)((d)(i)))))((j)((h)((d i)((d)(i))))(h(d i)((d)(i))))))((a)(g((d i)((d)(i))))((g)(d i)((d)(i)))d i(f h)((f)(h))(e)((d((f)(e)(j))(f((e)(j))))((d)(((f)(e)(j))(f((e)(j))))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f(e)(j))((f)((e)(j))))((i((g)h)(g(h)))((i)(((g)h)(g(h)))))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j(((h)((d i)((d)(i))))(h(d i)((d)(i)))))((j)((h)((d i)((d)(i))))(h(d i)((d)(i))))))))))((c)((b((a(((g)((d i)((d)(i))))(g(d i)((d)(i))))((f d i)((f)(d i)))(((f)(h))(f h))((e(f g)((f)(g)))((e)((f g)((f)(g)))))((d(e)(j))((d)((e)(j))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f((h)(e)(j))(h((e)(j))))((f)(((h)(e)(j))(h((e)(j))))))(i)((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j((h((d i)((d)(i))))((h)(d i)((d)(i)))))((j)(h((d i)((d)(i))))((h)(d i)((d)(i))))))((a)((g)((d i)((d)(i))))(g(d i)((d)(i)))(d i)((f(h))((f)h))((e g)((e)(g)))((d((f)(e)(j))(f((e)(j))))((d)(((f)(e)(j))(f((e)(j))))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f((h)(e)(j))(h((e)(j))))((f)(((h)(e)(j))(h((e)(j))))))(i)((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j((h((d i)((d)(i))))((h)(d i)((d)(i)))))((j)(h((d i)((d)(i))))((h)(d i)((d)(i))))))))((b)((a((g((d i)((d)(i))))((g)(d i)((d)(i))))((f d i)((f)(d i)))((f)(h))(f h)((e f)((e)(f)))((d(e)(j))((d)((e)(j))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f((h)(e)(j))(h((e)(j))))((f)(((h)(e)(j))(h((e)(j))))))((i(g))((i)g))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j((h((d i)((d)(i))))((h)(d i)((d)(i)))))((j)(h((d i)((d)(i))))((h)(d i)((d)(i))))))((a)(g((d i)((d)(i))))((g)(d i)((d)(i)))(d i)(f(h))((f)h)(e)((d((f)(e)(j))(f((e)(j))))((d)(((f)(e)(j))(f((e)(j))))))((g((d)(i)e j)(((d)(i))(e j)))((g)(((d)(i)e j)(((d)(i))(e j)))))((f((h)(e)(j))(h((e)(j))))((f)(((h)(e)(j))(h((e)(j))))))((i(g))((i)g))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j((h((d i)((d)(i))))((h)(d i)((d)(i)))))((j)(h((d i)((d)(i))))((h)(d i)((d)(i)))))))))))

d ((d((c((b((a(((g)i)(g(i)))(f i)((f)(i))(((f)h)(f(h)))((e(f g)((f)(g)))((e)((f g)((f)(g)))))(e)(j)((g e j)((g)(e j)))((f(e)(j))((f)((e)(j))))((i h)((i)(h)))((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((a)((g)i)(g(i))i((f h)((f)(h)))((e g)((e)(g)))((f)(e)(j))(f((e)(j)))((g e j)((g)(e j)))((f(e)(j))((f)((e)(j))))((i h)((i)(h)))((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))))((b)((a((g i)((g)(i)))(f i)((f)(i))((f)h)(f(h))((e f)((e)(f)))(e)(j)((g e j)((g)(e j)))((f(e)(j))((f)((e)(j))))((i((g)h)(g(h)))((i)(((g)h)(g(h)))))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((a)(g i)((g)(i))i(f h)((f)(h))(e)((f)(e)(j))(f((e)(j)))((g e j)((g)(e j)))((f(e)(j))((f)((e)(j))))((i((g)h)(g(h)))((i)(((g)h)(g(h)))))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))))))((c)((b((a(((g)i)(g(i)))((f i)((f)(i)))(((f)(h))(f h))((e(f g)((f)(g)))((e)((f g)((f)(g)))))(e)(j)((g e j)((g)(e j)))((f((h)(e)(j))(h((e)(j))))((f)(((h)(e)(j))(h((e)(j))))))(i)((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))((a)((g)i)(g(i))(i)((f(h))((f)h))((e g)((e)(g)))((f)(e)(j))(f((e)(j)))((g e j)((g)(e j)))((f((h)(e)(j))(h((e)(j))))((f)(((h)(e)(j))(h((e)(j))))))(i)((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))((b)((a((g i)((g)(i)))((f i)((f)(i)))((f)(h))(f h)((e f)((e)(f)))(e)(j)((g e j)((g)(e j)))((f((h)(e)(j))(h((e)(j))))((f)(((h)(e)(j))(h((e)(j))))))((i(g))((i)g))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))((a)(g i)((g)(i))(i)(f(h))((f)h)(e)((f)(e)(j))(f((e)(j)))((g e j)((g)(e j)))((f((h)(e)(j))(h((e)(j))))((f)(((h)(e)(j))(h((e)(j))))))((i(g))((i)g))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))))))((d)((c((b a(((g)(i))(g i))f(((f)h)(f(h)))((e(f g)((f)(g)))((e)((f g)((f)(g)))))((e)(j))((g((i)e j)(i(e j)))((g)(((i)e j)(i(e j)))))((f(e)(j))((f)((e)(j))))((i h)((i)(h)))((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j(((h)(i))(h i)))((j)((h)(i))(h i))))((b)a((g(i))((g)i))f((f)h)(f(h))((e f)((e)(f)))((e)(j))((g((i)e j)(i(e j)))((g)(((i)e j)(i(e j)))))((f(e)(j))((f)((e)(j))))((i((g)h)(g(h)))((i)(((g)h)(g(h)))))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j(((h)(i))(h i)))((j)((h)(i))(h i))))))((c)((b((a(((g)(i))(g i))(f)(((f)(h))(f h))((e(f g)((f)(g)))((e)((f g)((f)(g)))))((e)(j))((g((i)e j)(i(e j)))((g)(((i)e j)(i(e j)))))((f((h)(e)(j))(h((e)(j))))((f)(((h)(e)(j))(h((e)(j))))))(i)((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j((h(i))((h)i)))((j)(h(i))((h)i))))((a)((g)(i))(g i)((f(h))((f)h))((e g)((e)(g)))(((f)(e)(j))(f((e)(j))))((g((i)e j)(i(e j)))((g)(((i)e j)(i(e j)))))((f((h)(e)(j))(h((e)(j))))((f)(((h)(e)(j))(h((e)(j))))))(i)((h((g)(e)(j))(g((e)(j))))((h)(((g)(e)(j))(g((e)(j))))))((j((h(i))((h)i)))((j)(h(i))((h)i))))))((b)((a((g(i))((g)i))(f)((f)(h))(f h)((e f)((e)(f)))((e)(j))((g((i)e j)(i(e j)))((g)(((i)e j)(i(e j)))))((f((h)(e)(j))(h((e)(j))))((f)(((h)(e)(j))(h((e)(j))))))((i(g))((i)g))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j((h(i))((h)i)))((j)(h(i))((h)i))))((a)(g(i))((g)i)(f(h))((f)h)(e)(((f)(e)(j))(f((e)(j))))((g((i)e j)(i(e j)))((g)(((i)e j)(i(e j)))))((f((h)(e)(j))(h((e)(j))))((f)(((h)(e)(j))(h((e)(j))))))((i(g))((i)g))((h(g(e)(j))((g)((e)(j))))((h)((g(e)(j))((g)((e)(j))))))((j((h(i))((h)i)))((j)(h(i))((h)i)))))))))))

e ((e((d((c b(a)((g)i)(g(i))i((f h)((f)(h)))g(f)((g j)((g)(j)))(f)((i h)((i)(h)))((h(g))((h)g))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((c)b(a)((g)i)(g(i))(i)((f(h))((f)h))g(f)((g j)((g)(j)))((f(h))((f)h))(i)((h(g))((h)g))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))((d)((c((b a(((g)(i))(g i))f(((f)h)(f(h)))(f g)((f)(g))((g((i)j)(i(j)))((g)(((i)j)(i(j)))))(f)((i h)((i)(h)))((h(g))((h)g))((j(((h)(i))(h i)))((j)((h)(i))(h i))))((b)a((g(i))((g)i))f((f)h)(f(h))f((g((i)j)(i(j)))((g)(((i)j)(i(j)))))(f)((i((g)h)(g(h)))((i)(((g)h)(g(h)))))((h g)((h)(g)))((j(((h)(i))(h i)))((j)((h)(i))(h i))))))((c)((b((a(((g)(i))(g i))(f)(((f)(h))(f h))(f g)((f)(g))((g((i)j)(i(j)))((g)(((i)j)(i(j)))))((f(h))((f)h))(i)((h(g))((h)g))((j((h(i))((h)i)))((j)(h(i))((h)i))))((a)((g)(i))(g i)((f(h))((f)h))g f((g((i)j)(i(j)))((g)(((i)j)(i(j)))))((f(h))((f)h))(i)((h(g))((h)g))((j((h(i))((h)i)))((j)(h(i))((h)i))))))((b)a((g(i))((g)i))(f)((f)(h))(f h)f((g((i)j)(i(j)))((g)(((i)j)(i(j)))))((f(h))((f)h))((i(g))((i)g))((h g)((h)(g)))((j((h(i))((h)i)))((j)(h(i))((h)i))))))))))((e)((d((c((b((a(((g)i)(g(i)))(f i)((f)(i))(((f)h)(f(h)))((f g)((f)(g)))(j)(g)((f(j))((f)j))((i h)((i)(h)))((h((g)(j))(g j))((h)(((g)(j))(g j))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((a)((g)i)(g(i))i((f h)((f)(h)))(g)((f)(j))(f j)(g)((f(j))((f)j))((i h)((i)(h)))((h((g)(j))(g j))((h)(((g)(j))(g j))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))))((b)((a((g i)((g)(i)))(f i)((f)(i))((f)h)(f(h))(f)(j)(g)((f(j))((f)j))((i((g)h)(g(h)))((i)(((g)h)(g(h)))))((h(g(j))((g)j))((h)((g(j))((g)j))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((a)(g i)((g)(i))i(f h)((f)(h))((f)(j))(f j)(g)((f(j))((f)j))((i((g)h)(g(h)))((i)(((g)h)(g(h)))))((h(g(j))((g)j))((h)((g(j))((g)j))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))))))((c)((b((a(((g)i)(g(i)))((f i)((f)(i)))(((f)(h))(f h))((f g)((f)(g)))(j)(g)((f((h)(j))(h j))((f)(((h)(j))(h j))))(i)((h((g)(j))(g j))((h)(((g)(j))(g j))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))((a)((g)i)(g(i))(i)((f(h))((f)h))(g)((f)(j))(f j)(g)((f((h)(j))(h j))((f)(((h)(j))(h j))))(i)((h((g)(j))(g j))((h)(((g)(j))(g j))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))((b)((a((g i)((g)(i)))((f i)((f)(i)))((f)(h))(f h)(f)(j)(g)((f((h)(j))(h j))((f)(((h)(j))(h j))))((i(g))((i)g))((h(g(j))((g)j))((h)((g(j))((g)j))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))((a)(g i)((g)(i))(i)(f(h))((f)h)((f)(j))(f j)(g)((f((h)(j))(h j))((f)(((h)(j))(h j))))((i(g))((i)g))((h(g(j))((g)j))((h)((g(j))((g)j))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))))))((d)((c((b a(((g)(i))(g i))f(((f)h)(f(h)))((f g)((f)(g)))j((g(i))((g)i))((f(j))((f)j))((i h)((i)(h)))((h((g)(j))(g j))((h)(((g)(j))(g j))))((j(((h)(i))(h i)))((j)((h)(i))(h i))))((b)a((g(i))((g)i))f((f)h)(f(h))(f)j((g(i))((g)i))((f(j))((f)j))((i((g)h)(g(h)))((i)(((g)h)(g(h)))))((h(g(j))((g)j))((h)((g(j))((g)j))))((j(((h)(i))(h i)))((j)((h)(i))(h i))))))((c)((b((a(((g)(i))(g i))(f)(((f)(h))(f h))((f g)((f)(g)))j((g(i))((g)i))((f((h)(j))(h j))((f)(((h)(j))(h j))))(i)((h((g)(j))(g j))((h)(((g)(j))(g j))))((j((h(i))((h)i)))((j)(h(i))((h)i))))((a)((g)(i))(g i)((f(h))((f)h))(g)(((f)(j))(f j))((g(i))((g)i))((f((h)(j))(h j))((f)(((h)(j))(h j))))(i)((h((g)(j))(g j))((h)(((g)(j))(g j))))((j((h(i))((h)i)))((j)(h(i))((h)i))))))((b)((a((g(i))((g)i))(f)((f)(h))(f h)(f)j((g(i))((g)i))((f((h)(j))(h j))((f)(((h)(j))(h j))))((i(g))((i)g))((h(g(j))((g)j))((h)((g(j))((g)j))))((j((h(i))((h)i)))((j)(h(i))((h)i))))((a)(g(i))((g)i)(f(h))((f)h)(((f)(j))(f j))((g(i))((g)i))((f((h)(j))(h j))((f)(((h)(j))(h j))))((i(g))((i)g))((h(g(j))((g)j))((h)((g(j))((g)j))))((j((h(i))((h)i)))((j)(h(i))((h)i)))))))))))))

f ((f((e(d)(c)b(a)((g)(i))(g i)(h)g((g((i)j)(i(j)))((g)(((i)j)(i(j)))))(h)(i)((h(g))((h)g))((j((h(i))((h)i)))((j)(h(i))((h)i))))((e)((d((c((b((a(((g)i)(g(i)))(i)(h)g(j)(g)(j)((i h)((i)(h)))((h((g)(j))(g j))((h)(((g)(j))(g j))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((a)((g)i)(g(i))i h(g)(j)(g)(j)((i h)((i)(h)))((h((g)(j))(g j))((h)(((g)(j))(g j))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))))((b)(a)(g i)((g)(i))i(h)(j)(g)(j)((i((g)h)(g(h)))((i)(((g)h)(g(h)))))((h(g(j))((g)j))((h)((g(j))((g)j))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))))((c)((b((a(((g)i)(g(i)))i h g(j)(g)((h)(j))(h j)(i)((h((g)(j))(g j))((h)(((g)(j))(g j))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))((a)((g)i)(g(i))(i)(h)(g)(j)(g)((h)(j))(h j)(i)((h((g)(j))(g j))((h)(((g)(j))(g j))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))((b)(a)(g i)((g)(i))(i)h(j)(g)((h)(j))(h j)((i(g))((i)g))((h(g(j))((g)j))((h)((g(j))((g)j))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))))((d)((c b a(((g)(i))(g i))(h)g j((g(i))((g)i))(j)((i h)((i)(h)))((h((g)(j))(g j))((h)(((g)(j))(g j))))((j(((h)(i))(h i)))((j)((h)(i))(h i))))((c)((b(a)((g)(i))(g i)(h)(g)j((g(i))((g)i))((h)(j))(h j)(i)((h((g)(j))(g j))((h)(((g)(j))(g j))))((j((h(i))((h)i)))((j)(h(i))((h)i))))((b)(a)(g(i))((g)i)h j((g(i))((g)i))((h)(j))(h j)((i(g))((i)g))((h(g(j))((g)j))((h)((g(j))((g)j))))((j((h(i))((h)i)))((j)(h(i))((h)i))))))))))))((f)((e((d((c b(a)((g)i)(g(i))i(h)g((g j)((g)(j)))((i h)((i)(h)))((h(g))((h)g))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((c)b(a)((g)i)(g(i))(i)h g((g j)((g)(j)))h(i)((h(g))((h)g))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))((d)(c)b a(((g)(i))(g i))(h)g((g((i)j)(i(j)))((g)(((i)j)(i(j)))))h(i)((h(g))((h)g))((j((h(i))((h)i)))((j)(h(i))((h)i))))))((e)((d((c((b((a(((g)i)(g(i)))i h(g)(j)(g)j((i h)((i)(h)))((h((g)(j))(g j))((h)(((g)(j))(g j))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((a)((g)i)(g(i))i(h)(g)j(g)j((i h)((i)(h)))((h((g)(j))(g j))((h)(((g)(j))(g j))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))))((b)((a((g i)((g)(i)))i(h)(j)(g)j((i((g)h)(g(h)))((i)(((g)h)(g(h)))))((h(g(j))((g)j))((h)((g(j))((g)j))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((a)(g i)((g)(i))i h j(g)j((i((g)h)(g(h)))((i)(((g)h)(g(h)))))((h(g(j))((g)j))((h)((g(j))((g)j))))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))))))((c)((b((a(((g)i)(g(i)))(i)(h)(g)(j)(g)(((h)(j))(h j))(i)((h((g)(j))(g j))((h)(((g)(j))(g j))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))((a)((g)i)(g(i))(i)h(g)j(g)(((h)(j))(h j))(i)((h((g)(j))(g j))((h)(((g)(j))(g j))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))((b)((a((g i)((g)(i)))(i)h(j)(g)(((h)(j))(h j))((i(g))((i)g))((h(g(j))((g)j))((h)((g(j))((g)j))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))((a)(g i)((g)(i))(i)(h)j(g)(((h)(j))(h j))((i(g))((i)g))((h(g(j))((g)j))((h)((g(j))((g)j))))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))))))((d)(c)((b((a(((g)(i))(g i))(h)(g)j((g(i))((g)i))(((h)(j))(h j))(i)((h((g)(j))(g j))((h)(((g)(j))(g j))))((j((h(i))((h)i)))((j)(h(i))((h)i))))((a)((g)(i))(g i)h(g)(j)((g(i))((g)i))(((h)(j))(h j))(i)((h((g)(j))(g j))((h)(((g)(j))(g j))))((j((h(i))((h)i)))((j)(h(i))((h)i))))))((b)((a((g(i))((g)i))h j((g(i))((g)i))(((h)(j))(h j))((i(g))((i)g))((h(g(j))((g)j))((h)((g(j))((g)j))))((j((h(i))((h)i)))((j)(h(i))((h)i))))((a)(g(i))((g)i)(h)(j)((g(i))((g)i))(((h)(j))(h j))((i(g))((i)g))((h(g(j))((g)j))((h)((g(j))((g)j))))((j((h(i))((h)i)))((j)(h(i))((h)i)))))))))))))

g ((g((f((e(d)(c)b(a)(i)(h)((i)j)(i(j))(h)(i)(h)((j((h(i))((h)i)))((j)(h(i))((h)i))))((e)(d)((c b a i(h)j(i)(j)((i h)((i)(h)))((h(j))((h)j))((j(((h)(i))(h i)))((j)((h)(i))(h i))))((c)(b)(a)i h j(i)((h)(j))(h j)(i)((h j)((h)(j)))((j((h(i))((h)i)))((j)(h(i))((h)i))))))))((f)((e((d((c b(a)i i(h)j((i h)((i)(h)))(h)((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((c)b(a)i(i)h j h(i)(h)((j((h i)((h)(i))))((j)(h i)((h)(i)))))))((d)(c)b a i(h)((i)j)(i(j))h(i)(h)((j((h(i))((h)i)))((j)(h(i))((h)i))))))((e)(d)(c)(b)((a(i)h j(i)(((h)(j))(h j))(i)((h j)((h)(j)))((j((h(i))((h)i)))((j)(h(i))((h)i))))((a)i(h)(j)(i)(((h)(j))(h j))(i)((h j)((h)(j)))((j((h(i))((h)i)))((j)(h(i))((h)i))))))))))((g)((f(e)((d((c((b(a)(i)i h(j)(j)((i h)((i)(h)))((h j)((h)(j)))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((b)(a)i i(h)(j)(j)((i(h))((i)h))((h(j))((h)j))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))))((c)((b(a)(i)(i)(h)(j)((h)(j))(h j)(i)((h j)((h)(j)))((j((h i)((h)(i))))((j)(h i)((h)(i)))))((b)(a)i(i)h(j)((h)(j))(h j)i((h(j))((h)j))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))))((d)(c)((b(a)i(h)j i((h)(j))(h j)(i)((h j)((h)(j)))((j((h(i))((h)i)))((j)(h(i))((h)i))))((b)(a)(i)h j i((h)(j))(h j)i((h(j))((h)j))((j((h(i))((h)i)))((j)(h(i))((h)i))))))))((f)(e)((d((c((b((a i i h(j)j((i h)((i)(h)))((h j)((h)(j)))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((a)(i)i(h)j j((i h)((i)(h)))((h j)((h)(j)))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))))((b)((a(i)i(h)(j)j((i(h))((i)h))((h(j))((h)j))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))((a)i i h j j((i(h))((i)h))((h(j))((h)j))((j(((h)i)(h(i))))((j)((h)i)(h(i)))))))))((c)((b((a i(i)(h)(j)(((h)(j))(h j))(i)((h j)((h)(j)))((j((h i)((h)(i))))((j)(h i)((h)(i)))))((a)(i)(i)h j(((h)(j))(h j))(i)((h j)((h)(j)))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))((b)((a(i)(i)h(j)(((h)(j))(h j))i((h(j))((h)j))((j((h i)((h)(i))))((j)(h i)((h)(i)))))((a)i(i)(h)j(((h)(j))(h j))i((h(j))((h)j))((j((h i)((h)(i))))((j)(h i)((h)(i)))))))))))((d)(c)((b((a(i)(h)j i(((h)(j))(h j))(i)((h j)((h)(j)))((j((h(i))((h)i)))((j)(h(i))((h)i))))((a)i h(j)i(((h)(j))(h j))(i)((h j)((h)(j)))((j((h(i))((h)i)))((j)(h(i))((h)i))))))((b)((a i h j i(((h)(j))(h j))i((h(j))((h)j))((j((h(i))((h)i)))((j)(h(i))((h)i))))((a)(i)(h)(j)i(((h)(j))(h j))i((h(j))((h)j))((j((h(i))((h)i)))((j)(h(i))((h)i)))))))))))))

h ((h((g((f(e)(d)(c)(b)(a)i j(i)(j)(i)j((j(i))((j)i)))((f)(e)(d)(c)(b)a(i)j(i)j(i)j((j(i))((j)i)))))((g)((f(e)((d((c b(a)(i)i(j)(j)i j((j(i))((j)i)))((c)(b)(a)i(i)(j)(j)i(j)((j i)((j)(i))))))((d)(c)(b)(a)(i)j i(j)i(j)((j(i))((j)i)))))((f)(e)((d((c((b a i i(j)j i j((j(i))((j)i)))((b)(a)i i j j(i)(j)((j(i))((j)i)))))((c)((b(a)(i)(i)j j(i)j((j i)((j)(i))))((b)a(i)(i)(j)j i(j)((j i)((j)(i))))))))((d)(c)((b(a)i(j)i j(i)j((j(i))((j)i)))((b)a i j i j i(j)((j(i))((j)i)))))))))))((h)((g((f((e(d)(c)b(a)(i)((i)j)(i(j))(i)((j i)((j)(i))))((e)(d)c b a i j(i)(j)(i)j((j(i))((j)i)))))((f)((e d c b(a)i i j(i)((j i)((j)(i))))((e)(d)(c)(b)(a)i(j)(i)(j)(i)(j)((j i)((j)(i))))))))((g)((f(e)((d((c(b)(a)i i(j)(j)i j((j i)((j)(i))))((c)b(a)(i)(i)(j)j(i)(j)((j(i))((j)i)))))((d)(c)b(a)i j i j(i)(j)((j i)((j)(i))))))((f)(e)((d((c((b(a)(i)i j j(i)(j)((j i)((j)(i))))((b)a(i)i(j)j i j((j i)((j)(i))))))((c)((b a i(i)(j)(j)(i)(j)((j(i))((j)i)))((b)(a)i(i)j(j)i j((j(i))((j)i)))))))((d)(c)((b a(i)j i(j)(i)(j)((j i)((j)(i))))((b)(a)(i)(j)i(j)i j((j i)((j)(i)))))))))))))

i ((i((h(g)(f)(e)((d c b a(j)j j(j))((d)(c)(b)a j j(j)(j))))((h)(g)f(e)d c(b)(a)(j)(j)j j)))((i)((h((g(f)(e)(d)(c)(b)a j j j j)((g)(f)(e)d(c)b(a)j j j(j))))((h)((g f e(d)(c)b(a)(j)(j))((g)f(e)d(c)b(a)(j)j(j)j))))))

j ((j(i)h g(f)(e)(d)(c)(b)a)((j)(i)(h)g f e(d)(c)b(a)))
In [15]:
print to_string(Z)
((j(i)h g(f)(e)(d)(c)(b)a)((j)(i)(h)g f e(d)(c)b(a)))