YiBS

Principle

• There are often unnecessary axioms in problems in rich theories
• Estimate relevance of axioms and remove less relevant ones

Architecture

• Divide formulae into more and less relevant parts
• Submit more relevant part to ATP
• On failure, add or remove formulae

Performance

• TBA