Predicate Pairing with Abstraction for Relational Verification