- Provide axioms with relevance measure
- Divide formulae into top and bottom parts
- Call ATP system using the top part
- If proof found, hoorah
- If proof impossible, add top of bottom
- If timeout
- Optimistic mode, try top of top
- Pessimistic mode, add top of bottom
- At the median - get half the formulae
- At 0.5 - get formulae "more than half relevant"
- At the (geometric) average - get formulae "above average relevance"
- Σtop-relevancies = Σbottom-relevancies
- get "half the relevance"
- Σtop-relevancies = Σ(1 - bottom-relevancies)
- balances relevance against irrelevance
- Σ(1 - top-relevance) = Σbottom-relevancies
- balances irrelevance against relevance.