Interval-based Resource Usage Verification by Translation into Horn Clauses and an Application to Energy Consumption