first check for satisfiability without topo. if unsat, return core. if satisfiable, check incrementally until returned set of clauses changes. This is in response to observed cores for hallwayofdoom type specs