Theorem proving via general matings