New parameter asym_eq

This controls the "asymmetric" optim of the equation rule, where at most
one of the two recipes can be a sum.
Tighten dynamic constraint generation

Fix in the rigid case: Only check for occurrence at toplevel underneath
sums, not arbitrarily deep in the term. Also make sure to only mark
recipes associated to sums, to maintain the invariants used in the theory.

Change the flexible case: Mark any recipe associated to a sum, but consider
all options (making the rule more non-deterministic). Also do not mark in
the only (!) case where the theory cannot justify this strategy.

The dynamic marking seems pretty solid now. However, the marking in the
flexible case is unnecessary for termination (and useless for performance)
when asym_eq is activated, and we loose several examples when asym_eq is
disabled regardless of the amount of flexible marking that is performed.
Restrict conseq to be able to justify asym_eq

In order to have completeness for identical atoms, we need to be able to
decompose all equalities of recipes into equalities with one side not being a
sum. This can be guaranteed after a slight restriction of conseq, which does
not affect our examples.
Produce a RESULTS file when running tests
Merge branch 'ac' of github.com:dbaelde/akiss into ac