Nearly all of my time today consumed again by this project. Lots of good optimization hacking, but there's still a major and mysterious outstanding bug: when trying to prove
P(a) ⇒ ¬P(f(f(a))) &rArr ¬¬(∃x. P(x) ∧ ¬P(f(x)))
it generates crazy proofterms that involve variables applied to themselves, which is clearly not right.
Had a quick dinner at some restaurant in oakland whose name I forget with tom and the pitt biology kids. It was an ok burger, little on the burnt side. Had to turn down a trip to the waterfront with martinivixen and this vanessa character I still haven't met, since I really needed to buckle down tonight on the project. A shame, but I'll be able to make up for it soon since summer effectively begins friday for me.