add rudimentary simplification: subsumption, self-subsuming resolution, bounded variable elimination