Generate tasks for the given formulas and add them to the goal
The constants that can be considered free (resp., that have to be considered non-free) in this proof tree.
The fully simplified closing constraint
All constants that occur in formulas in this goal
Constants that can be eliminated in this goal because they are universal, and they do not occur in any tasks or compound formulas (but they might occur in the facts)
t is a constant that is eliminated in this goal
Eliminate all prioritised tasks for which the given predicate is false.
true if the sets of free constants have reached a fixed point
Create the tasks to store and handle an arbitrary given formula.
Function to be called after split rules, to generate new inference collections for the subgoals.
true if there are chances that the
closingConstraint of this tree changes by applying rules
to any goal
true if it is possible to apply rules to any goal in this
the vocabulary available at a certain node in the proof