Skip to content
  • Michael Raskin's avatar
    Refactorings went to produce something usable · faff1ac8
    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