A Tough nut for Proof Procedures. AIM-016