Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs