When adding clauses that conatins duplicates, the checking
of some proof would fail because there would sometime be multiple
littrals to resolve over. This fixes that problem.
Proofs require local assumptions to be recognisable.
Keeping the reason of local assumptions as Bcp simplfies
the code, since a proof is a clause, and allows to not have
to recreate the local unit clause that effectively propagates
the local assumptions.
With this fix, simplification of clauses is not required aymore for
levels between 0 (excluded) and base_level, so the partition function
can be simplified accordingly.
Apart from new assumptions, clause level can always
be computed from the histoy of the clause, so it is
better to do it in Solver_types when creating clauses.
Aditionally, it seems there was an error in the manual
computing of clause level somewhere, this fixes the bug.
