Proving properties of sorting programs: A case study in horn clause verification