renaming

fiddle with relevance filter

update docs

reorganize options regarding to the relevance threshold and decay

make relevance filter work in term of a "max_relevant" option + use Vampire SOS; "max_relevant" is more reliable than "max_relevant_per_iter"; also made sure that the option is monotone -- larger values should lead to more axioms -- which wasn't always the case before; SOS for Vampire makes a difference of about 3% (i.e. 3% more proofs are found)

simplify more code

cosmetics

get rid of "defs_relevant" feature; nobody uses it and it works poorly

make SML/NJ happy

renamed "relevance_convergence" to "relevance_decay"