Using First-Order Theorem Provers in the Jahob Data Structure Verification System