In first order logic, we can prove satisfiability several ways: Finite model generation, truthful monadic abstractions, and also saturation. With finite model generation techniques, we can verify the model directly. With saturation we saturate the search space, running out of inferences, thus proving that a model exists.
How can we verify satisfiability demonstrated through saturation without rerunning the entire search, which might take quite a long time? Satisfiability demonstrated through saturation might be an infinite model, so model generation may not be sufficient.