SaturationAlgorithm::addInputSOSClause is currently skipping forwardSimplify

[quickbeam123]

Filling up the active container at the start under SOS is not doing full clause inter-reductions even if enabled.

We might want to do it for consistency, efficiency, and stronger invariants (e.g., "can't have two alpha-equivalent clauses in the forward subsumption index when FSub enabled, ...)

However, this is not a one-line fix, because forwardSimplify normally puts clause replacements into _newClauses from which travel to _unprocessed from which they normally go to _passive. So this long clause dispatch would need to be duplicated for the sake of addInputSOSClause or parametrized.