Removing gates
Moving subsumption and strengthening to another file
Extended Resolution has long been removed -- clean it up
Forgot to initialize SubsumeStrengthen in Simplifier. Fixed.
Bin&Tri clauses' literals no longer counted into binTri.redLits/irredLits
Renaming 'learnt' to redundant and 'non-learnt' to irredundant

Much cleaner and better, but a lot of code had to be changed
Renaming learnt_clause2 to tmp_learnt_clause

And cleaning up related implementation. Should be cleaned up more,
though
Cleaning up component finding
OOps, forgot to indicate M for millions
Removing unused, commented out code
Adding an iterator to Watched so foreach() works with it
Add helper function to varreplacer to check for assignement sanity

Something seems to be wrong, this helps to debug it. If variables are
set, their replacement should also be set. Apparently, this is violated.
Adding [prober] prefix to stuff printed by prober
Allow for boost array in findSubsume0 in SubsumeStrengthen

This will be useful for gate-finding
Gatefinder must be a friend of SubsumeStrengthen to use it

Probably this should be changed, it should be less private and more
public
More asserts and comments in implication cache cleaning
When something is set during cache-cleaning, it must be re-done

Because re-numbering will take effects after propagation, which may set
new variables, etc. So that must be recursive, unfortunately
Irredundant binary clauses must always be added for every variable replacement

OR the variable replacement MUST be done immediately after. Otherwise,
redundant binary clauses might get removed (by var-elim for example) and
then all hell gets loose
Re-enabling gate-finding
Limits must be set before blocked clause elimination