Add an explicit theory axiom.
Add a formula to the handled proof goal.
Record that values of the given constants can be reconstructed from the provided facts.
Split a proof goal into multiple sub-goals, and justify the split through an explicit theory axiom.
Close the goal by invoking an explicit theory axiom.
Remove some facts from the handled proof goal.
Schedule a task to be applied later on the goal.
Split a disequality fact into two inequalities.
Split a proof goal into multiple sub-goals.
A simple relevance filter to get rid of axioms that follow trivially from built-in arithmetic rules.