The Model Verification Method

The Interpretation Formula must ...

... be syntactically correct, well-typed
... represent the model that was found
... be satisfiable
... be consistent with the problem formulae
... represent a model of the problem formulae

These things can be checked by ...

... standard parsing and type checking
... faith in the implementation
... a trusted model finder
... a trusted model finder
... proving that if ...
     TPTP axiom ⊨ Problem formulae
  then
     Domain & Mappings ⊢ Problem formulae
... and using a trusted theorem prover to show ...
     TPTP axiom ⊨ Problem formulae