Solving Horn Clauses on Inductive Data Types Without Induction