On interpolation in automated theorem proving