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