After some heroic bug-hunting and optimizing, our theorem prover passes all 81 tests - even the ones that we had formerly left out because they were too slow - in about 5 seconds when compiled with MLton. It even proves &exist x. 2 * 2 = x Amazing, I know! (x = 4)
So there's a lunch Frank organized for tomorrow for all of us in the class to discuss our projects. After that, at last, the semester's over for me.