In automated theorem Poving different kinds of proof systems have been used. Traditional proof systems, such as Hilbert-style proofs or natural deduction we call non-analytic, while resolution or mating proof systems we call analytic. There are many good reasons to study the connections between analytic and non-analytic proofs. We would like a theorem prover to make efficient use of both analytic and non-analytic methods to get the best of both worlds.