Wonderful links, thank you so much. Vampire uses a portfolio of strategies, including the application of an SMT solver (Z3). This link goes into some detail: h

Wonderful links, thank you so much. Vampire uses a portfolio of strategies, including the application of an SMT solver (Z3). This link goes into some detail: http://smt2019.galois.com/papers/tool_paper_20.pdf http://smt2019.galois.com/papers/tool_paper_20.pdf This is the most relevant bit for our conversation: > There are only two cases where Vampire can return sat: Firstly in UF and secondly, if Vampire produces a ground problem after preprocessing it may pass this problem to Z3 and report its result (possibly sat) directly. Essentially this refers to model building, i.e. solving existential problems. That's where SAT solvers excel. This includes producing counter-examples which are extremely useful in industry.