I love twelf! I verified my first metatheorem today. I struggled with my code for several hours last night, before taking my question to the top. It turned out to be a naive lack of parentheses introducing unwanted dependencies. But that is fixed and now I am a theorem proving maniac.
Man, if only one could do a thesis on admissibility of cut for various logics, because I am really good at that now.
Oh yeah, I beat my brother Mike to 1,000 songs on Audioscrobbler. (Audioscrobbler is a neat plugin for winamp and other players that keeps on-line stats on what you play, and helps you see what music is related to it. The data are all supposedly free for everyone, which helps me believe it's not just some nefarious marketing data collection plot.) Want to attach "experience points" to something you do anyway? This is it!
I was cheated out of about 300 songs a few weeks ago when their server went down, but I still win: brighterorange vs. oatmeal2000!