* The metis method no longer fails because the theorem is too trivial (contains the empty clause). Larry