<*>
+ <*>
| + pure (\u1 -> (\u2 -> u1))
| ` <*>
|   + <*>
|   | + <*>
|   | | + pure (\u1 -> (\u2 -> u1))
|   | | ` pure (\u1 -> u1)
|   | ` def name_11
|   |   ` <*>
|   |     + <*>
|   |     | + <*>
|   |     | | + pure (\u1 -> (\u2 -> u1))
|   |     | | ` pure (\u1 -> u1)
|   |     | ` <*>
|   |     |   + <*>
|   |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|   |     |   | ` def name_27
|   |     |   |   ` pure Term
|   |     |   ` def name_28
|   |     |     ` <|>
|   |     |       + <*>
|   |     |       | + <*>
|   |     |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   |     |       | | ` <*>
|   |     |       | |   + <*>
|   |     |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|   |     |       | |   | ` pure (\u1 -> (\u2 -> u1))
|   |     |       | |   ` <|>
|   |     |       | |     + <*>
|   |     |       | |     | + <*>
|   |     |       | |     | | + <*>
|   |     |       | |     | | | + pure (\u1 -> (\u2 -> u1))
|   |     |       | |     | | | ` pure (\u1 -> u1)
|   |     |       | |     | | ` def name_26
|   |     |       | |     | |   ` <*>
|   |     |       | |     | |     + <*>
|   |     |       | |     | |     | + <*>
|   |     |       | |     | |     | | + pure (\u1 -> (\u2 -> u1))
|   |     |       | |     | |     | | ` pure (\u1 -> u1)
|   |     |       | |     | |     | ` def name_2
|   |     |       | |     | |     |   ` satisfy
|   |     |       | |     | |     ` ref name_27
|   |     |       | |     | ` <*>
|   |     |       | |     |   + <*>
|   |     |       | |     |   | + <*>
|   |     |       | |     |   | | + pure (\u1 -> (\u2 -> u1))
|   |     |       | |     |   | | ` pure (\u1 -> u1)
|   |     |       | |     |   | ` <*>
|   |     |       | |     |   |   + <*>
|   |     |       | |     |   |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|   |     |       | |     |   |   | ` pure Term
|   |     |       | |     |   |   ` def name_20
|   |     |       | |     |   |     ` <|>
|   |     |       | |     |   |       + <*>
|   |     |       | |     |   |       | + <*>
|   |     |       | |     |   |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   |     |       | |     |   |       | | ` <*>
|   |     |       | |     |   |       | |   + <*>
|   |     |       | |     |   |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|   |     |       | |     |   |       | |   | ` pure (\u1 -> (\u2 -> u1))
|   |     |       | |     |   |       | |   ` ref name_26
|   |     |       | |     |   |       | ` rec name_20
|   |     |       | |     |   |       ` pure (\u1 -> u1)
|   |     |       | |     |   ` pure Term
|   |     |       | |     ` <*>
|   |     |       | |       + <*>
|   |     |       | |       | + <*>
|   |     |       | |       | | + pure (\u1 -> (\u2 -> u1))
|   |     |       | |       | | ` pure (\u1 -> u1)
|   |     |       | |       | ` <*>
|   |     |       | |       |   + <*>
|   |     |       | |       |   | + <*>
|   |     |       | |       |   | | + pure (\u1 -> (\u2 -> u1))
|   |     |       | |       |   | | ` pure (\u1 -> u1)
|   |     |       | |       |   | ` try
|   |     |       | |       |   |   ` <*>
|   |     |       | |       |   |     + <*>
|   |     |       | |       |   |     | + pure cons
|   |     |       | |       |   |     | ` <*>
|   |     |       | |       |   |     |   + <*>
|   |     |       | |       |   |     |   | + pure (\u1 -> (\u2 -> u1))
|   |     |       | |       |   |     |   | ` pure '/'
|   |     |       | |       |   |     |   ` ref name_2
|   |     |       | |       |   |     ` <*>
|   |     |       | |       |   |       + <*>
|   |     |       | |       |   |       | + pure cons
|   |     |       | |       |   |       | ` <*>
|   |     |       | |       |   |       |   + <*>
|   |     |       | |       |   |       |   | + pure (\u1 -> (\u2 -> u1))
|   |     |       | |       |   |       |   | ` pure '/'
|   |     |       | |       |   |       |   ` ref name_2
|   |     |       | |       |   |       ` pure Term
|   |     |       | |       |   ` <*>
|   |     |       | |       |     + <*>
|   |     |       | |       |     | + <*>
|   |     |       | |       |     | | + pure (\u1 -> (\u2 -> u1))
|   |     |       | |       |     | | ` pure (\u1 -> u1)
|   |     |       | |       |     | ` <*>
|   |     |       | |       |     |   + <*>
|   |     |       | |       |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|   |     |       | |       |     |   | ` ref name_27
|   |     |       | |       |     |   ` def name_12
|   |     |       | |       |     |     ` <|>
|   |     |       | |       |     |       + <*>
|   |     |       | |       |     |       | + <*>
|   |     |       | |       |     |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|   |     |       | |       |     |       | | ` <*>
|   |     |       | |       |     |       | |   + <*>
|   |     |       | |       |     |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|   |     |       | |       |     |       | |   | ` pure (\u1 -> (\u2 -> u1))
|   |     |       | |       |     |       | |   ` ref name_2
|   |     |       | |       |     |       | ` rec name_12
|   |     |       | |       |     |       ` pure (\u1 -> u1)
|   |     |       | |       |     ` ref name_27
|   |     |       | |       ` ref name_27
|   |     |       | ` rec name_28
|   |     |       ` pure (\u1 -> u1)
|   |     ` ref name_27
|   ` <*>
|     + <*>
|     | + <*>
|     | | + pure (\u1 -> (\u2 -> u1))
|     | | ` pure (\u1 -> u1)
|     | ` <*>
|     |   + <*>
|     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|     |   | ` ref name_27
|     |   ` def name_15
|     |     ` <|>
|     |       + <*>
|     |       | + <*>
|     |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|     |       | | ` <*>
|     |       | |   + <*>
|     |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|     |       | |   | ` pure (\u1 -> (\u2 -> u1))
|     |       | |   ` <*>
|     |       | |     + <*>
|     |       | |     | + <*>
|     |       | |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     | | ` pure (\u1 -> u1)
|     |       | |     | ` <*>
|     |       | |     |   + <*>
|     |       | |     |   | + <*>
|     |       | |     |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   | | ` pure (\u1 -> u1)
|     |       | |     |   | ` <*>
|     |       | |     |   |   + <*>
|     |       | |     |   |   | + <*>
|     |       | |     |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |   | | ` pure (\u1 -> u1)
|     |       | |     |   |   | ` <*>
|     |       | |     |   |   |   + <*>
|     |       | |     |   |   |   | + <*>
|     |       | |     |   |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |   |   | | ` pure (\u1 -> u1)
|     |       | |     |   |   |   | ` try
|     |       | |     |   |   |   |   ` <*>
|     |       | |     |   |   |   |     + <*>
|     |       | |     |   |   |   |     | + <*>
|     |       | |     |   |   |   |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |   |   |     | | ` pure (\u1 -> u1)
|     |       | |     |   |   |   |     | ` try
|     |       | |     |   |   |   |     |   ` <*>
|     |       | |     |   |   |   |     |     + <*>
|     |       | |     |   |   |   |     |     | + pure cons
|     |       | |     |   |   |   |     |     | ` <*>
|     |       | |     |   |   |   |     |     |   + <*>
|     |       | |     |   |   |   |     |     |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |   |   |     |     |   | ` pure 'f'
|     |       | |     |   |   |   |     |     |   ` ref name_2
|     |       | |     |   |   |   |     |     ` <*>
|     |       | |     |   |   |   |     |       + <*>
|     |       | |     |   |   |   |     |       | + pure cons
|     |       | |     |   |   |   |     |       | ` <*>
|     |       | |     |   |   |   |     |       |   + <*>
|     |       | |     |   |   |   |     |       |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |   |   |     |       |   | ` pure 'u'
|     |       | |     |   |   |   |     |       |   ` ref name_2
|     |       | |     |   |   |   |     |       ` <*>
|     |       | |     |   |   |   |     |         + <*>
|     |       | |     |   |   |   |     |         | + pure cons
|     |       | |     |   |   |   |     |         | ` <*>
|     |       | |     |   |   |   |     |         |   + <*>
|     |       | |     |   |   |   |     |         |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |   |   |     |         |   | ` pure 'n'
|     |       | |     |   |   |   |     |         |   ` ref name_2
|     |       | |     |   |   |   |     |         ` <*>
|     |       | |     |   |   |   |     |           + <*>
|     |       | |     |   |   |   |     |           | + pure cons
|     |       | |     |   |   |   |     |           | ` <*>
|     |       | |     |   |   |   |     |           |   + <*>
|     |       | |     |   |   |   |     |           |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |   |   |     |           |   | ` pure 'c'
|     |       | |     |   |   |   |     |           |   ` ref name_2
|     |       | |     |   |   |   |     |           ` <*>
|     |       | |     |   |   |   |     |             + <*>
|     |       | |     |   |   |   |     |             | + pure cons
|     |       | |     |   |   |   |     |             | ` <*>
|     |       | |     |   |   |   |     |             |   + <*>
|     |       | |     |   |   |   |     |             |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |   |   |     |             |   | ` pure 't'
|     |       | |     |   |   |   |     |             |   ` ref name_2
|     |       | |     |   |   |   |     |             ` <*>
|     |       | |     |   |   |   |     |               + <*>
|     |       | |     |   |   |   |     |               | + pure cons
|     |       | |     |   |   |   |     |               | ` <*>
|     |       | |     |   |   |   |     |               |   + <*>
|     |       | |     |   |   |   |     |               |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |   |   |     |               |   | ` pure 'i'
|     |       | |     |   |   |   |     |               |   ` ref name_2
|     |       | |     |   |   |   |     |               ` <*>
|     |       | |     |   |   |   |     |                 + <*>
|     |       | |     |   |   |   |     |                 | + pure cons
|     |       | |     |   |   |   |     |                 | ` <*>
|     |       | |     |   |   |   |     |                 |   + <*>
|     |       | |     |   |   |   |     |                 |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |   |   |     |                 |   | ` pure 'o'
|     |       | |     |   |   |   |     |                 |   ` ref name_2
|     |       | |     |   |   |   |     |                 ` <*>
|     |       | |     |   |   |   |     |                   + <*>
|     |       | |     |   |   |   |     |                   | + pure cons
|     |       | |     |   |   |   |     |                   | ` <*>
|     |       | |     |   |   |   |     |                   |   + <*>
|     |       | |     |   |   |   |     |                   |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |   |   |     |                   |   | ` pure 'n'
|     |       | |     |   |   |   |     |                   |   ` ref name_2
|     |       | |     |   |   |   |     |                   ` def name_5
|     |       | |     |   |   |   |     |                     ` pure Term
|     |       | |     |   |   |   |     ` def name_7
|     |       | |     |   |   |   |       ` negLook
|     |       | |     |   |   |   |         ` ref name_2
|     |       | |     |   |   |   ` ref name_11
|     |       | |     |   |   ` def name_9
|     |       | |     |   |     ` <*>
|     |       | |     |   |       + <*>
|     |       | |     |   |       | + <*>
|     |       | |     |   |       | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |       | | ` pure (\u1 -> u1)
|     |       | |     |   |       | ` try
|     |       | |     |   |       |   ` <*>
|     |       | |     |   |       |     + <*>
|     |       | |     |   |       |     | + <*>
|     |       | |     |   |       |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |       |     | | ` pure (\u1 -> u1)
|     |       | |     |   |       |     | ` ref name_2
|     |       | |     |   |       |     ` <*>
|     |       | |     |   |       |       + <*>
|     |       | |     |   |       |       | + <*>
|     |       | |     |   |       |       | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |       |       | | ` pure (\u1 -> u1)
|     |       | |     |   |       |       | ` <*>
|     |       | |     |   |       |       |   + <*>
|     |       | |     |   |       |       |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|     |       | |     |   |       |       |   | ` ref name_27
|     |       | |     |   |       |       |   ` def name_16
|     |       | |     |   |       |       |     ` <|>
|     |       | |     |   |       |       |       + <*>
|     |       | |     |   |       |       |       | + <*>
|     |       | |     |   |       |       |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|     |       | |     |   |       |       |       | | ` <*>
|     |       | |     |   |       |       |       | |   + <*>
|     |       | |     |   |       |       |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|     |       | |     |   |       |       |       | |   | ` pure (\u1 -> (\u2 -> u1))
|     |       | |     |   |       |       |       | |   ` ref name_2
|     |       | |     |   |       |       |       | ` rec name_16
|     |       | |     |   |       |       |       ` pure (\u1 -> u1)
|     |       | |     |   |       |       ` ref name_27
|     |       | |     |   |       ` ref name_11
|     |       | |     |   ` <*>
|     |       | |     |     + <*>
|     |       | |     |     | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     | ` <*>
|     |       | |     |     |   + <*>
|     |       | |     |     |   | + <*>
|     |       | |     |     |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |   | | ` pure (\u1 -> u1)
|     |       | |     |     |   | ` def name_18
|     |       | |     |     |   |   ` <*>
|     |       | |     |     |   |     + <*>
|     |       | |     |     |   |     | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |   |     | ` <*>
|     |       | |     |     |   |     |   + <*>
|     |       | |     |     |   |     |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |   |     |   | ` pure '('
|     |       | |     |     |   |     |   ` ref name_2
|     |       | |     |     |   |     ` ref name_11
|     |       | |     |     |   ` <*>
|     |       | |     |     |     + <*>
|     |       | |     |     |     | + <*>
|     |       | |     |     |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     | | ` pure (\u1 -> u1)
|     |       | |     |     |     | ` def name_10
|     |       | |     |     |     |   ` <|>
|     |       | |     |     |     |     + <*>
|     |       | |     |     |     |     | + <*>
|     |       | |     |     |     |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     | | ` pure Term
|     |       | |     |     |     |     | ` <*>
|     |       | |     |     |     |     |   + <*>
|     |       | |     |     |     |     |   | + <*>
|     |       | |     |     |     |     |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |   | | ` pure (\u1 -> u1)
|     |       | |     |     |     |     |   | ` def name_30
|     |       | |     |     |     |     |   |   ` <*>
|     |       | |     |     |     |     |   |     + <*>
|     |       | |     |     |     |     |   |     | + <*>
|     |       | |     |     |     |     |   |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |   |     | | ` pure (\u1 -> u1)
|     |       | |     |     |     |     |   |     | ` ref name_9
|     |       | |     |     |     |     |   |     ` <|>
|     |       | |     |     |     |     |   |       + <*>
|     |       | |     |     |     |     |   |       | + <*>
|     |       | |     |     |     |     |   |       | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |   |       | | ` pure Term
|     |       | |     |     |     |     |   |       | ` def name_19
|     |       | |     |     |     |     |   |       |   ` <*>
|     |       | |     |     |     |     |   |       |     + <*>
|     |       | |     |     |     |     |   |       |     | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |   |       |     | ` <*>
|     |       | |     |     |     |     |   |       |     |   + <*>
|     |       | |     |     |     |     |   |       |     |   | + <*>
|     |       | |     |     |     |     |   |       |     |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |   |       |     |   | | ` pure (\u1 -> u1)
|     |       | |     |     |     |     |   |       |     |   | ` <*>
|     |       | |     |     |     |     |   |       |     |   |   + <*>
|     |       | |     |     |     |     |   |       |     |   |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |   |       |     |   |   | ` <*>
|     |       | |     |     |     |     |   |       |     |   |   |   + <*>
|     |       | |     |     |     |     |   |       |     |   |   |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |   |       |     |   |   |   | ` pure '['
|     |       | |     |     |     |     |   |       |     |   |   |   ` ref name_2
|     |       | |     |     |     |     |   |       |     |   |   ` ref name_11
|     |       | |     |     |     |     |   |       |     |   ` <*>
|     |       | |     |     |     |     |   |       |     |     + <*>
|     |       | |     |     |     |     |   |       |     |     | + <*>
|     |       | |     |     |     |     |   |       |     |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |   |       |     |     | | ` pure (\u1 -> u1)
|     |       | |     |     |     |     |   |       |     |     | ` ref name_2
|     |       | |     |     |     |     |   |       |     |     ` <*>
|     |       | |     |     |     |     |   |       |     |       + <*>
|     |       | |     |     |     |     |   |       |     |       | + <*>
|     |       | |     |     |     |     |   |       |     |       | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |   |       |     |       | | ` pure (\u1 -> u1)
|     |       | |     |     |     |     |   |       |     |       | ` <*>
|     |       | |     |     |     |     |   |       |     |       |   + <*>
|     |       | |     |     |     |     |   |       |     |       |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|     |       | |     |     |     |     |   |       |     |       |   | ` pure Term
|     |       | |     |     |     |     |   |       |     |       |   ` def name_13
|     |       | |     |     |     |     |   |       |     |       |     ` <|>
|     |       | |     |     |     |     |   |       |     |       |       + <*>
|     |       | |     |     |     |     |   |       |     |       |       | + <*>
|     |       | |     |     |     |     |   |       |     |       |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|     |       | |     |     |     |     |   |       |     |       |       | | ` <*>
|     |       | |     |     |     |     |   |       |     |       |       | |   + <*>
|     |       | |     |     |     |     |   |       |     |       |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|     |       | |     |     |     |     |   |       |     |       |       | |   | ` pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |   |       |     |       |       | |   ` ref name_2
|     |       | |     |     |     |     |   |       |     |       |       | ` rec name_13
|     |       | |     |     |     |     |   |       |     |       |       ` pure (\u1 -> u1)
|     |       | |     |     |     |     |   |       |     |       ` pure Term
|     |       | |     |     |     |     |   |       |     ` <*>
|     |       | |     |     |     |     |   |       |       + <*>
|     |       | |     |     |     |     |   |       |       | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |   |       |       | ` <*>
|     |       | |     |     |     |     |   |       |       |   + <*>
|     |       | |     |     |     |     |   |       |       |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |   |       |       |   | ` pure ']'
|     |       | |     |     |     |     |   |       |       |   ` ref name_2
|     |       | |     |     |     |     |   |       |       ` ref name_11
|     |       | |     |     |     |     |   |       ` ref name_27
|     |       | |     |     |     |     |   ` <*>
|     |       | |     |     |     |     |     + <*>
|     |       | |     |     |     |     |     | + <*>
|     |       | |     |     |     |     |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |     | | ` pure (\u1 -> u1)
|     |       | |     |     |     |     |     | ` <*>
|     |       | |     |     |     |     |     |   + <*>
|     |       | |     |     |     |     |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|     |       | |     |     |     |     |     |   | ` ref name_27
|     |       | |     |     |     |     |     |   ` def name_29
|     |       | |     |     |     |     |     |     ` <|>
|     |       | |     |     |     |     |     |       + <*>
|     |       | |     |     |     |     |     |       | + <*>
|     |       | |     |     |     |     |     |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|     |       | |     |     |     |     |     |       | | ` <*>
|     |       | |     |     |     |     |     |       | |   + def name_6
|     |       | |     |     |     |     |     |       | |   | ` <*>
|     |       | |     |     |     |     |     |       | |   |   + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|     |       | |     |     |     |     |     |       | |   |   ` pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |     |       | |   ` <*>
|     |       | |     |     |     |     |     |       | |     + <*>
|     |       | |     |     |     |     |     |       | |     | + <*>
|     |       | |     |     |     |     |     |       | |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |     |       | |     | | ` pure (\u1 -> u1)
|     |       | |     |     |     |     |     |       | |     | ` def name_23
|     |       | |     |     |     |     |     |       | |     |   ` <*>
|     |       | |     |     |     |     |     |       | |     |     + <*>
|     |       | |     |     |     |     |     |       | |     |     | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |     |       | |     |     | ` <*>
|     |       | |     |     |     |     |     |       | |     |     |   + <*>
|     |       | |     |     |     |     |     |       | |     |     |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |     |     |     |       | |     |     |   | ` pure ','
|     |       | |     |     |     |     |     |       | |     |     |   ` ref name_2
|     |       | |     |     |     |     |     |       | |     |     ` ref name_11
|     |       | |     |     |     |     |     |       | |     ` ref name_30
|     |       | |     |     |     |     |     |       | ` rec name_29
|     |       | |     |     |     |     |     |       ` pure (\u1 -> u1)
|     |       | |     |     |     |     |     ` ref name_27
|     |       | |     |     |     |     ` ref name_27
|     |       | |     |     |     ` <|>
|     |       | |     |     |       + <*>
|     |       | |     |     |       | + <*>
|     |       | |     |     |       | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |       | | ` pure Term
|     |       | |     |     |       | ` <*>
|     |       | |     |     |       |   + <*>
|     |       | |     |     |       |   | + <*>
|     |       | |     |     |       |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |       |   | | ` pure (\u1 -> u1)
|     |       | |     |     |       |   | ` <*>
|     |       | |     |     |       |   |   + <*>
|     |       | |     |     |       |   |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |       |   |   | ` <*>
|     |       | |     |     |       |   |   |   + <*>
|     |       | |     |     |       |   |   |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |     |       |   |   |   | ` pure ':'
|     |       | |     |     |       |   |   |   ` ref name_2
|     |       | |     |     |       |   |   ` ref name_11
|     |       | |     |     |       |   ` ref name_10
|     |       | |     |     |       ` ref name_27
|     |       | |     |     ` def name_8
|     |       | |     |       ` <*>
|     |       | |     |         + <*>
|     |       | |     |         | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |         | ` <*>
|     |       | |     |         |   + <*>
|     |       | |     |         |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |     |         |   | ` pure ')'
|     |       | |     |         |   ` ref name_2
|     |       | |     |         ` ref name_11
|     |       | |     ` def name_24
|     |       | |       ` <*>
|     |       | |         + <*>
|     |       | |         | + pure (\u1 -> (\u2 -> u1))
|     |       | |         | ` <*>
|     |       | |         |   + <*>
|     |       | |         |   | + <*>
|     |       | |         |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |   | | ` pure (\u1 -> u1)
|     |       | |         |   | ` <*>
|     |       | |         |   |   + <*>
|     |       | |         |   |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |   |   | ` <*>
|     |       | |         |   |   |   + <*>
|     |       | |         |   |   |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |   |   |   | ` pure '{'
|     |       | |         |   |   |   ` ref name_2
|     |       | |         |   |   ` ref name_11
|     |       | |         |   ` <*>
|     |       | |         |     + <*>
|     |       | |         |     | + <*>
|     |       | |         |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     | | ` pure (\u1 -> u1)
|     |       | |         |     | ` <*>
|     |       | |         |     |   + <*>
|     |       | |         |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|     |       | |         |     |   | ` ref name_27
|     |       | |         |     |   ` def name_4
|     |       | |         |     |     ` <|>
|     |       | |         |     |       + <*>
|     |       | |         |     |       | + <*>
|     |       | |         |     |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|     |       | |         |     |       | | ` <*>
|     |       | |         |     |       | |   + <*>
|     |       | |         |     |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|     |       | |         |     |       | |   | ` pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |   ` <|>
|     |       | |         |     |       | |     + <|>
|     |       | |         |     |       | |     | + <|>
|     |       | |         |     |       | |     | | + <*>
|     |       | |         |     |       | |     | | | + <*>
|     |       | |         |     |       | |     | | | | + <*>
|     |       | |         |     |       | |     | | | | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | | ` <*>
|     |       | |         |     |       | |     | | | |   + <*>
|     |       | |         |     |       | |     | | | |   | + <*>
|     |       | |         |     |       | |     | | | |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   | ` <*>
|     |       | |         |     |       | |     | | | |   |   + <*>
|     |       | |         |     |       | |     | | | |   |   | + <*>
|     |       | |         |     |       | |     | | | |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |   | ` <*>
|     |       | |         |     |       | |     | | | |   |   |   + <*>
|     |       | |         |     |       | |     | | | |   |   |   | + <*>
|     |       | |         |     |       | |     | | | |   |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |   |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |   |   | ` try
|     |       | |         |     |       | |     | | | |   |   |   |   ` <*>
|     |       | |         |     |       | |     | | | |   |   |   |     + <*>
|     |       | |         |     |       | |     | | | |   |   |   |     | + <*>
|     |       | |         |     |       | |     | | | |   |   |   |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |   |   |     | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |   |   |     | ` try
|     |       | |         |     |       | |     | | | |   |   |   |     |   ` <*>
|     |       | |         |     |       | |     | | | |   |   |   |     |     + <*>
|     |       | |         |     |       | |     | | | |   |   |   |     |     | + pure cons
|     |       | |         |     |       | |     | | | |   |   |   |     |     | ` <*>
|     |       | |         |     |       | |     | | | |   |   |   |     |     |   + <*>
|     |       | |         |     |       | |     | | | |   |   |   |     |     |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |   |   |     |     |   | ` pure 'i'
|     |       | |         |     |       | |     | | | |   |   |   |     |     |   ` ref name_2
|     |       | |         |     |       | |     | | | |   |   |   |     |     ` <*>
|     |       | |         |     |       | |     | | | |   |   |   |     |       + <*>
|     |       | |         |     |       | |     | | | |   |   |   |     |       | + pure cons
|     |       | |         |     |       | |     | | | |   |   |   |     |       | ` <*>
|     |       | |         |     |       | |     | | | |   |   |   |     |       |   + <*>
|     |       | |         |     |       | |     | | | |   |   |   |     |       |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |   |   |     |       |   | ` pure 'f'
|     |       | |         |     |       | |     | | | |   |   |   |     |       |   ` ref name_2
|     |       | |         |     |       | |     | | | |   |   |   |     |       ` ref name_5
|     |       | |         |     |       | |     | | | |   |   |   |     ` ref name_7
|     |       | |         |     |       | |     | | | |   |   |   ` ref name_11
|     |       | |         |     |       | |     | | | |   |   ` def name_14
|     |       | |         |     |       | |     | | | |   |     ` <*>
|     |       | |         |     |       | |     | | | |   |       + <*>
|     |       | |         |     |       | |     | | | |   |       | + <*>
|     |       | |         |     |       | |     | | | |   |       | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |       | ` def name_25
|     |       | |         |     |       | |     | | | |   |       |   ` <|>
|     |       | |         |     |       | |     | | | |   |       |     + <|>
|     |       | |         |     |       | |     | | | |   |       |     | + <*>
|     |       | |         |     |       | |     | | | |   |       |     | | + <*>
|     |       | |         |     |       | |     | | | |   |       |     | | | + <*>
|     |       | |         |     |       | |     | | | |   |       |     | | | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |     | | | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |       |     | | | ` <|>
|     |       | |         |     |       | |     | | | |   |       |     | | |   + <*>
|     |       | |         |     |       | |     | | | |   |       |     | | |   | + <*>
|     |       | |         |     |       | |     | | | |   |       |     | | |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |     | | |   | | ` pure '0'
|     |       | |         |     |       | |     | | | |   |       |     | | |   | ` ref name_2
|     |       | |         |     |       | |     | | | |   |       |     | | |   ` <*>
|     |       | |         |     |       | |     | | | |   |       |     | | |     + <*>
|     |       | |         |     |       | |     | | | |   |       |     | | |     | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |     | | |     | ` pure '1'
|     |       | |         |     |       | |     | | | |   |       |     | | |     ` ref name_2
|     |       | |         |     |       | |     | | | |   |       |     | | ` ref name_11
|     |       | |         |     |       | |     | | | |   |       |     | ` <*>
|     |       | |         |     |       | |     | | | |   |       |     |   + <*>
|     |       | |         |     |       | |     | | | |   |       |     |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |     |   | ` <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |   + <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |   | + <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |     |   |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |       |     |   |   | ` <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |   |   + <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |   |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |     |   |   |   | ` pure '\''
|     |       | |         |     |       | |     | | | |   |       |     |   |   |   ` ref name_2
|     |       | |         |     |       | |     | | | |   |       |     |   |   ` <|>
|     |       | |         |     |       | |     | | | |   |       |     |   |     + <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |     | + <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |     | | + <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |     | | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |     |   |     | | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |       |     |   |     | | ` ref name_2
|     |       | |         |     |       | |     | | | |   |       |     |   |     | ` ref name_27
|     |       | |         |     |       | |     | | | |   |       |     |   |     ` <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |       + <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |       | + <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |       | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |     |   |       | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |       |     |   |       | ` <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |       |   + <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |       |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |     |   |       |   | ` pure '\\'
|     |       | |         |     |       | |     | | | |   |       |     |   |       |   ` ref name_2
|     |       | |         |     |       | |     | | | |   |       |     |   |       ` <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |         + <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |         | + <*>
|     |       | |         |     |       | |     | | | |   |       |     |   |         | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |     |   |         | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |       |     |   |         | ` ref name_2
|     |       | |         |     |       | |     | | | |   |       |     |   |         ` ref name_27
|     |       | |         |     |       | |     | | | |   |       |     |   ` <*>
|     |       | |         |     |       | |     | | | |   |       |     |     + <*>
|     |       | |         |     |       | |     | | | |   |       |     |     | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |     |     | ` <*>
|     |       | |         |     |       | |     | | | |   |       |     |     |   + <*>
|     |       | |         |     |       | |     | | | |   |       |     |     |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |     |     |   | ` pure '\''
|     |       | |         |     |       | |     | | | |   |       |     |     |   ` ref name_2
|     |       | |         |     |       | |     | | | |   |       |     |     ` ref name_11
|     |       | |         |     |       | |     | | | |   |       |     ` <*>
|     |       | |         |     |       | |     | | | |   |       |       + <*>
|     |       | |         |     |       | |     | | | |   |       |       | + <*>
|     |       | |         |     |       | |     | | | |   |       |       | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |       | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |       |       | ` ref name_9
|     |       | |         |     |       | |     | | | |   |       |       ` <|>
|     |       | |         |     |       | |     | | | |   |       |         + <*>
|     |       | |         |     |       | |     | | | |   |       |         | + <*>
|     |       | |         |     |       | |     | | | |   |       |         | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |         | | ` pure Term
|     |       | |         |     |       | |     | | | |   |       |         | ` <|>
|     |       | |         |     |       | |     | | | |   |       |         |   + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |         |   | | ` <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |   + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |   | + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |         |   | |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |       |         |   | |   | ` ref name_18
|     |       | |         |     |       | |     | | | |   |       |         |   | |   ` <|>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     | + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |         |   | |     | | ` pure Term
|     |       | |         |     |       | |     | | | |   |       |         |   | |     | ` <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |   + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |   | + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |   | ` rec name_14
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |   ` <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     | + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     | ` <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |   + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |   | ` ref name_27
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |   ` def name_17
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |     ` <|>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | | ` <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |   + ref name_6
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |   ` <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |     + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |     | + <*>
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |     | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |     | ` ref name_23
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | |     ` rec name_14
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       | ` rec name_17
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     |       ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |       |         |   | |     |     ` ref name_27
|     |       | |         |     |       | |     | | | |   |       |         |   | |     ` ref name_27
|     |       | |         |     |       | |     | | | |   |       |         |   | ` ref name_8
|     |       | |         |     |       | |     | | | |   |       |         |   ` ref name_19
|     |       | |         |     |       | |     | | | |   |       |         ` ref name_27
|     |       | |         |     |       | |     | | | |   |       ` <*>
|     |       | |         |     |       | |     | | | |   |         + <*>
|     |       | |         |     |       | |     | | | |   |         | + <*>
|     |       | |         |     |       | |     | | | |   |         | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |         | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |         | ` <*>
|     |       | |         |     |       | |     | | | |   |         |   + <*>
|     |       | |         |     |       | |     | | | |   |         |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|     |       | |         |     |       | |     | | | |   |         |   | ` ref name_27
|     |       | |         |     |       | |     | | | |   |         |   ` def name_22
|     |       | |         |     |       | |     | | | |   |         |     ` <|>
|     |       | |         |     |       | |     | | | |   |         |       + <*>
|     |       | |         |     |       | |     | | | |   |         |       | + <*>
|     |       | |         |     |       | |     | | | |   |         |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|     |       | |         |     |       | |     | | | |   |         |       | | ` <*>
|     |       | |         |     |       | |     | | | |   |         |       | |   + <*>
|     |       | |         |     |       | |     | | | |   |         |       | |   | + pure (\u1 -> (\u2 -> (\u3 -> (u1 u3) u2)))
|     |       | |         |     |       | |     | | | |   |         |       | |   | ` pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |         |       | |   ` <*>
|     |       | |         |     |       | |     | | | |   |         |       | |     + <*>
|     |       | |         |     |       | |     | | | |   |         |       | |     | + <*>
|     |       | |         |     |       | |     | | | |   |         |       | |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |         |       | |     | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |         |       | |     | ` <*>
|     |       | |         |     |       | |     | | | |   |         |       | |     |   + <*>
|     |       | |         |     |       | |     | | | |   |         |       | |     |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |         |       | |     |   | ` <*>
|     |       | |         |     |       | |     | | | |   |         |       | |     |   |   + <*>
|     |       | |         |     |       | |     | | | |   |         |       | |     |   |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | | |   |         |       | |     |   |   | ` pure '!'
|     |       | |         |     |       | |     | | | |   |         |       | |     |   |   ` ref name_2
|     |       | |         |     |       | |     | | | |   |         |       | |     |   ` ref name_11
|     |       | |         |     |       | |     | | | |   |         |       | |     ` ref name_25
|     |       | |         |     |       | |     | | | |   |         |       | ` rec name_22
|     |       | |         |     |       | |     | | | |   |         |       ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | | |   |         ` ref name_27
|     |       | |         |     |       | |     | | | |   ` rec name_24
|     |       | |         |     |       | |     | | | ` <|>
|     |       | |         |     |       | |     | | |   + <*>
|     |       | |         |     |       | |     | | |   | + <*>
|     |       | |         |     |       | |     | | |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | |   | | ` pure Term
|     |       | |         |     |       | |     | | |   | ` <*>
|     |       | |         |     |       | |     | | |   |   + <*>
|     |       | |         |     |       | |     | | |   |   | + <*>
|     |       | |         |     |       | |     | | |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | |   |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | |   |   | ` <*>
|     |       | |         |     |       | |     | | |   |   |   + <*>
|     |       | |         |     |       | |     | | |   |   |   | + <*>
|     |       | |         |     |       | |     | | |   |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | |   |   |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | |   |   |   | ` try
|     |       | |         |     |       | |     | | |   |   |   |   ` <*>
|     |       | |         |     |       | |     | | |   |   |   |     + <*>
|     |       | |         |     |       | |     | | |   |   |   |     | + <*>
|     |       | |         |     |       | |     | | |   |   |   |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | |   |   |   |     | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | | |   |   |   |     | ` try
|     |       | |         |     |       | |     | | |   |   |   |     |   ` <*>
|     |       | |         |     |       | |     | | |   |   |   |     |     + <*>
|     |       | |         |     |       | |     | | |   |   |   |     |     | + pure cons
|     |       | |         |     |       | |     | | |   |   |   |     |     | ` <*>
|     |       | |         |     |       | |     | | |   |   |   |     |     |   + <*>
|     |       | |         |     |       | |     | | |   |   |   |     |     |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | |   |   |   |     |     |   | ` pure 'e'
|     |       | |         |     |       | |     | | |   |   |   |     |     |   ` ref name_2
|     |       | |         |     |       | |     | | |   |   |   |     |     ` <*>
|     |       | |         |     |       | |     | | |   |   |   |     |       + <*>
|     |       | |         |     |       | |     | | |   |   |   |     |       | + pure cons
|     |       | |         |     |       | |     | | |   |   |   |     |       | ` <*>
|     |       | |         |     |       | |     | | |   |   |   |     |       |   + <*>
|     |       | |         |     |       | |     | | |   |   |   |     |       |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | |   |   |   |     |       |   | ` pure 'l'
|     |       | |         |     |       | |     | | |   |   |   |     |       |   ` ref name_2
|     |       | |         |     |       | |     | | |   |   |   |     |       ` <*>
|     |       | |         |     |       | |     | | |   |   |   |     |         + <*>
|     |       | |         |     |       | |     | | |   |   |   |     |         | + pure cons
|     |       | |         |     |       | |     | | |   |   |   |     |         | ` <*>
|     |       | |         |     |       | |     | | |   |   |   |     |         |   + <*>
|     |       | |         |     |       | |     | | |   |   |   |     |         |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | |   |   |   |     |         |   | ` pure 's'
|     |       | |         |     |       | |     | | |   |   |   |     |         |   ` ref name_2
|     |       | |         |     |       | |     | | |   |   |   |     |         ` <*>
|     |       | |         |     |       | |     | | |   |   |   |     |           + <*>
|     |       | |         |     |       | |     | | |   |   |   |     |           | + pure cons
|     |       | |         |     |       | |     | | |   |   |   |     |           | ` <*>
|     |       | |         |     |       | |     | | |   |   |   |     |           |   + <*>
|     |       | |         |     |       | |     | | |   |   |   |     |           |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | | |   |   |   |     |           |   | ` pure 'e'
|     |       | |         |     |       | |     | | |   |   |   |     |           |   ` ref name_2
|     |       | |         |     |       | |     | | |   |   |   |     |           ` ref name_5
|     |       | |         |     |       | |     | | |   |   |   |     ` ref name_7
|     |       | |         |     |       | |     | | |   |   |   ` ref name_11
|     |       | |         |     |       | |     | | |   |   ` rec name_24
|     |       | |         |     |       | |     | | |   ` ref name_27
|     |       | |         |     |       | |     | | ` <*>
|     |       | |         |     |       | |     | |   + <*>
|     |       | |         |     |       | |     | |   | + <*>
|     |       | |         |     |       | |     | |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | |   | ` <*>
|     |       | |         |     |       | |     | |   |   + <*>
|     |       | |         |     |       | |     | |   |   | + <*>
|     |       | |         |     |       | |     | |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | |   |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | |   |   | ` <*>
|     |       | |         |     |       | |     | |   |   |   + <*>
|     |       | |         |     |       | |     | |   |   |   | + <*>
|     |       | |         |     |       | |     | |   |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | |   |   |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | |   |   |   | ` try
|     |       | |         |     |       | |     | |   |   |   |   ` <*>
|     |       | |         |     |       | |     | |   |   |   |     + <*>
|     |       | |         |     |       | |     | |   |   |   |     | + <*>
|     |       | |         |     |       | |     | |   |   |   |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | |   |   |   |     | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     | |   |   |   |     | ` try
|     |       | |         |     |       | |     | |   |   |   |     |   ` <*>
|     |       | |         |     |       | |     | |   |   |   |     |     + <*>
|     |       | |         |     |       | |     | |   |   |   |     |     | + pure cons
|     |       | |         |     |       | |     | |   |   |   |     |     | ` <*>
|     |       | |         |     |       | |     | |   |   |   |     |     |   + <*>
|     |       | |         |     |       | |     | |   |   |   |     |     |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | |   |   |   |     |     |   | ` pure 'w'
|     |       | |         |     |       | |     | |   |   |   |     |     |   ` ref name_2
|     |       | |         |     |       | |     | |   |   |   |     |     ` <*>
|     |       | |         |     |       | |     | |   |   |   |     |       + <*>
|     |       | |         |     |       | |     | |   |   |   |     |       | + pure cons
|     |       | |         |     |       | |     | |   |   |   |     |       | ` <*>
|     |       | |         |     |       | |     | |   |   |   |     |       |   + <*>
|     |       | |         |     |       | |     | |   |   |   |     |       |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | |   |   |   |     |       |   | ` pure 'h'
|     |       | |         |     |       | |     | |   |   |   |     |       |   ` ref name_2
|     |       | |         |     |       | |     | |   |   |   |     |       ` <*>
|     |       | |         |     |       | |     | |   |   |   |     |         + <*>
|     |       | |         |     |       | |     | |   |   |   |     |         | + pure cons
|     |       | |         |     |       | |     | |   |   |   |     |         | ` <*>
|     |       | |         |     |       | |     | |   |   |   |     |         |   + <*>
|     |       | |         |     |       | |     | |   |   |   |     |         |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | |   |   |   |     |         |   | ` pure 'i'
|     |       | |         |     |       | |     | |   |   |   |     |         |   ` ref name_2
|     |       | |         |     |       | |     | |   |   |   |     |         ` <*>
|     |       | |         |     |       | |     | |   |   |   |     |           + <*>
|     |       | |         |     |       | |     | |   |   |   |     |           | + pure cons
|     |       | |         |     |       | |     | |   |   |   |     |           | ` <*>
|     |       | |         |     |       | |     | |   |   |   |     |           |   + <*>
|     |       | |         |     |       | |     | |   |   |   |     |           |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | |   |   |   |     |           |   | ` pure 'l'
|     |       | |         |     |       | |     | |   |   |   |     |           |   ` ref name_2
|     |       | |         |     |       | |     | |   |   |   |     |           ` <*>
|     |       | |         |     |       | |     | |   |   |   |     |             + <*>
|     |       | |         |     |       | |     | |   |   |   |     |             | + pure cons
|     |       | |         |     |       | |     | |   |   |   |     |             | ` <*>
|     |       | |         |     |       | |     | |   |   |   |     |             |   + <*>
|     |       | |         |     |       | |     | |   |   |   |     |             |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     | |   |   |   |     |             |   | ` pure 'e'
|     |       | |         |     |       | |     | |   |   |   |     |             |   ` ref name_2
|     |       | |         |     |       | |     | |   |   |   |     |             ` ref name_5
|     |       | |         |     |       | |     | |   |   |   |     ` ref name_7
|     |       | |         |     |       | |     | |   |   |   ` ref name_11
|     |       | |         |     |       | |     | |   |   ` ref name_14
|     |       | |         |     |       | |     | |   ` rec name_24
|     |       | |         |     |       | |     | ` try
|     |       | |         |     |       | |     |   ` <*>
|     |       | |         |     |       | |     |     + <*>
|     |       | |         |     |       | |     |     | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     | ` <*>
|     |       | |         |     |       | |     |     |   + <*>
|     |       | |         |     |       | |     |     |   | + <*>
|     |       | |         |     |       | |     |     |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |   | ` <*>
|     |       | |         |     |       | |     |     |   |   + <*>
|     |       | |         |     |       | |     |     |   |   | + <*>
|     |       | |         |     |       | |     |     |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |   |   | ` <*>
|     |       | |         |     |       | |     |     |   |   |   + <*>
|     |       | |         |     |       | |     |     |   |   |   | + <*>
|     |       | |         |     |       | |     |     |   |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |   |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |   |   |   | ` <|>
|     |       | |         |     |       | |     |     |   |   |   |   + <*>
|     |       | |         |     |       | |     |     |   |   |   |   | + <*>
|     |       | |         |     |       | |     |     |   |   |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |   |   |   | | ` pure Term
|     |       | |         |     |       | |     |     |   |   |   |   | ` <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   + <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   | + <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |   |   |   |   | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |   |   |   |   |   | ` try
|     |       | |         |     |       | |     |     |   |   |   |   |   |   ` <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     + <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     | + <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |   |   |   |   |     | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |   |   |   |   |   |     | ` try
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |   ` <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |     + <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |     | + pure cons
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |     | ` <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |     |   + <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |     |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |     |   | ` pure 'v'
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |     |   ` ref name_2
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |     ` <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |       + <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |       | + pure cons
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |       | ` <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |       |   + <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |       |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |       |   | ` pure 'a'
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |       |   ` ref name_2
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |       ` <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |         + <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |         | + pure cons
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |         | ` <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |         |   + <*>
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |         |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |         |   | ` pure 'r'
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |         |   ` ref name_2
|     |       | |         |     |       | |     |     |   |   |   |   |   |     |         ` ref name_5
|     |       | |         |     |       | |     |     |   |   |   |   |   |     ` ref name_7
|     |       | |         |     |       | |     |     |   |   |   |   |   ` ref name_11
|     |       | |         |     |       | |     |     |   |   |   |   ` ref name_27
|     |       | |         |     |       | |     |     |   |   |   ` <*>
|     |       | |         |     |       | |     |     |   |   |     + <*>
|     |       | |         |     |       | |     |     |   |   |     | + <*>
|     |       | |         |     |       | |     |     |   |   |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |   |     | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |   |   |     | ` ref name_30
|     |       | |         |     |       | |     |     |   |   |     ` <*>
|     |       | |         |     |       | |     |     |   |   |       + <*>
|     |       | |         |     |       | |     |     |   |   |       | + <*>
|     |       | |         |     |       | |     |     |   |   |       | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |   |       | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |   |   |       | ` <*>
|     |       | |         |     |       | |     |     |   |   |       |   + <*>
|     |       | |         |     |       | |     |     |   |   |       |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|     |       | |         |     |       | |     |     |   |   |       |   | ` ref name_27
|     |       | |         |     |       | |     |     |   |   |       |   ` def name_3
|     |       | |         |     |       | |     |     |   |   |       |     ` <|>
|     |       | |         |     |       | |     |     |   |   |       |       + <*>
|     |       | |         |     |       | |     |     |   |   |       |       | + <*>
|     |       | |         |     |       | |     |     |   |   |       |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|     |       | |         |     |       | |     |     |   |   |       |       | | ` <*>
|     |       | |         |     |       | |     |     |   |   |       |       | |   + ref name_6
|     |       | |         |     |       | |     |     |   |   |       |       | |   ` <*>
|     |       | |         |     |       | |     |     |   |   |       |       | |     + <*>
|     |       | |         |     |       | |     |     |   |   |       |       | |     | + <*>
|     |       | |         |     |       | |     |     |   |   |       |       | |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |   |       |       | |     | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |   |   |       |       | |     | ` ref name_23
|     |       | |         |     |       | |     |     |   |   |       |       | |     ` ref name_30
|     |       | |         |     |       | |     |     |   |   |       |       | ` rec name_3
|     |       | |         |     |       | |     |     |   |   |       |       ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |   |   |       ` ref name_27
|     |       | |         |     |       | |     |     |   |   ` <*>
|     |       | |         |     |       | |     |     |   |     + <*>
|     |       | |         |     |       | |     |     |   |     | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |     | ` <*>
|     |       | |         |     |       | |     |     |   |     |   + <*>
|     |       | |         |     |       | |     |     |   |     |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |   |     |   | ` pure '='
|     |       | |         |     |       | |     |     |   |     |   ` ref name_2
|     |       | |         |     |       | |     |     |   |     ` ref name_11
|     |       | |         |     |       | |     |     |   ` <*>
|     |       | |         |     |       | |     |     |     + <*>
|     |       | |         |     |       | |     |     |     | + <*>
|     |       | |         |     |       | |     |     |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |     | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |     | ` ref name_14
|     |       | |         |     |       | |     |     |     ` <*>
|     |       | |         |     |       | |     |     |       + <*>
|     |       | |         |     |       | |     |     |       | + <*>
|     |       | |         |     |       | |     |     |       | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |       | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |       | ` <*>
|     |       | |         |     |       | |     |     |       |   + <*>
|     |       | |         |     |       | |     |     |       |   | + pure ((\u1 -> (\u2 -> (\u3 -> (u1 u3) u2))) (\u1 -> (\u2 -> u1 u2)))
|     |       | |         |     |       | |     |     |       |   | ` ref name_27
|     |       | |         |     |       | |     |     |       |   ` def name_1
|     |       | |         |     |       | |     |     |       |     ` <|>
|     |       | |         |     |       | |     |     |       |       + <*>
|     |       | |         |     |       | |     |     |       |       | + <*>
|     |       | |         |     |       | |     |     |       |       | | + pure (\u1 -> (\u2 -> (\u3 -> u1 (u2 u3))))
|     |       | |         |     |       | |     |     |       |       | | ` <*>
|     |       | |         |     |       | |     |     |       |       | |   + ref name_6
|     |       | |         |     |       | |     |     |       |       | |   ` <*>
|     |       | |         |     |       | |     |     |       |       | |     + <*>
|     |       | |         |     |       | |     |     |       |       | |     | + <*>
|     |       | |         |     |       | |     |     |       |       | |     | | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |     |       |       | |     | | ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |       |       | |     | ` ref name_23
|     |       | |         |     |       | |     |     |       |       | |     ` ref name_14
|     |       | |         |     |       | |     |     |       |       | ` rec name_1
|     |       | |         |     |       | |     |     |       |       ` pure (\u1 -> u1)
|     |       | |         |     |       | |     |     |       ` ref name_27
|     |       | |         |     |       | |     |     ` def name_21
|     |       | |         |     |       | |     |       ` <*>
|     |       | |         |     |       | |     |         + <*>
|     |       | |         |     |       | |     |         | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |         | ` <*>
|     |       | |         |     |       | |     |         |   + <*>
|     |       | |         |     |       | |     |         |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |     |         |   | ` pure ';'
|     |       | |         |     |       | |     |         |   ` ref name_2
|     |       | |         |     |       | |     |         ` ref name_11
|     |       | |         |     |       | |     ` <*>
|     |       | |         |     |       | |       + <*>
|     |       | |         |     |       | |       | + pure (\u1 -> (\u2 -> u1))
|     |       | |         |     |       | |       | ` ref name_14
|     |       | |         |     |       | |       ` ref name_21
|     |       | |         |     |       | ` rec name_4
|     |       | |         |     |       ` pure (\u1 -> u1)
|     |       | |         |     ` ref name_27
|     |       | |         ` <*>
|     |       | |           + <*>
|     |       | |           | + pure (\u1 -> (\u2 -> u1))
|     |       | |           | ` <*>
|     |       | |           |   + <*>
|     |       | |           |   | + pure (\u1 -> (\u2 -> u1))
|     |       | |           |   | ` pure '}'
|     |       | |           |   ` ref name_2
|     |       | |           ` ref name_11
|     |       | ` rec name_15
|     |       ` pure (\u1 -> u1)
|     ` ref name_27
` eof