That's a lot of fun :). It's a bit frustrating though that once you've grabbed a logic operator from the panel left, it loses the annotations. For example, for function application, i'd forgotten if the top or the bottom hole was for the function... Maybe i should just work on my short-term memory...<p>EDIT: I'm not really sure what the point is of all the propositions they want you to prove using bottom? Yeah so your logic is inconsistent if you introduce bottom as a true proposition, big deal :/