-
Michael Raskin authored
Implemented filtering; interestingly, with unused lemmas removed, Vampire fails to prove a lemma which is easy for E prover and SPASS. In another mode it can prove it, but in this mode it fails to prove with the original set of lemmas. If I remove all the unused assumptions, Vampire manages to prove it.
faff1ac8