Fixed: Solver::Assign() should check subsumption in original setup.

When adding all isomorphic literals, the order of these literals should
be irrelevant.