A split tree provides a ledger recording intermediate terms
encountered during a derivation. Each term in the tree is derived
from a single parent using the split operator. A key property is
that we can determine whether or not a given term has been
encountered previously.
A derivation heuristic is responsible for deriving a given term in
the derivation tree. That means it must decide what aspect of the
term to derivation on (e.g. the number of occurences of a
particular variable) and then apply this to the derivation tree.