looks for guilty conjuncts whose cnf elements are subsumed by other conjuncts and removes them from the returned core