Revised discrimination tree implementation:

Revised discrimination tree implementation:

- code size reduced, looking for unifiables or generalizations is
  almost the same and do not internally work with the query term,
  but its path representation that is now decorated with arieties to
  recover the tree structure when needed (jump to the sibling...)

- works with partial instantiation (no more global ariety list, but
  local to application heads). Stupid example:

  query: fold plus [] 0 = 0
  ==?==
  tree: fold ? [] 0 = 0

  since the 2nd arg is ? we skip the query subterm rooted in plus,
  but if plus is considered of ariety 2, we fail unifiing the following
  terms (we skip [] and 0 reaching the second 0 that is unified with
  [] and fails).

- term -> path string function fixed to clen up the input term, no more
  "FIXME: the trie received invalid term". Here there is room for improvements
  especially on beta redexes and terms beginning with an abstraction, but we
  need the substitutions operation, we should move the file elsewhere

- Big change:
  - if the query term is a meta, then the whole content of the tree is returned
  - in paramodulation this is dangerous, thus we added a small check in
    the paramodulation code (eq_indexing) instead of making the discrimination
    tree behave in a nasty way
  - the new implementation returns the same set of candidates on all test
    TPTP/Veloci and library/ (except for the aforementioned corner case).