Applying machine learning to saturation-based automated theorem proving. Member of Automated Reasoning Group. Supervised by Josef Urban and Martin Suda.