What needs to be done:
 Finish refactoring of axiom_rules.py (issue453).
 Try different options for axiom_rules.py (within issue453):
 overapproximate negated axioms: 1) current way (negate = buggy),
2) trivially overapproximate; 3) trivially overapproximate for cycles,
negate when there are no cycles
 keep redundant positive axioms: yes/no (=> in the medium term, we would
like to always have the positive form as the "real" form)
 layers: use minimum number of layers (as currently) or maximum number of
layer (=> in the medium term, we probably only want to decide on one
of these two)
 overapproximate necessary literals: 1) full relevance analysis 2) consider
all nonderived literals as necessary 3) old implementation
(The old implementation considered all positive literals as necessary,
which is wrong but usually works well. Ideally we will decide between
1 and 3 or keep 1 and 3 as options)
 Do something about the combinatiorial explosion with the DNF conversion
(e.g. issue450).
Related issues and messages:
 issue165: partly or fully the same thing as issue450 (see below)
 issue450: negating axiom rules is implemented as a CNFtoDNF conversion,
which can explode exponentially
 issue453: axiom semantics when negated are wrong because the idea of just
negating the formula that encodes the triggering conditions is semantically wrong
 issue454: about getting rid of negated axiom rules in the translator
 msg8204: explains the axiom code and contains notes and what could be improved
 msg8235: lists which domains and search configurations are relevant when
dealing with the axioms
Issues that have test cases that are important and we should consolidate:
 issue165
 issue450
 issue453
 issue862
