Is the documentation of the file format here http://www.gilith.com/research/opentheory/article.html#eqMpCommand correct? My reader appears to be saying that the article file corresponding to bool-1.0 wants |- phi to be popped before |- phi' = psi