Efficient reasoning for inconsistent horn formulae