Adding Gondwana (linear join expansion) and fixing KifFormat on Dobs that only have one child.
Stratified provers now decide between expansion methods for each rule based on historical cost of using each method.