We construct a correspondence between Horn clauses and finite tree automata (FTA). We construct a refined clauses from an FTA of the clauses and an infeasible trace. We propose a splitting operator on FTAs and describe its role in verification. We demonstrate the feasibility of our approach in practice.