Pass the correct prover parameter.

Use CSAS proof status.

Use ProofEvaluationStateUpdater.

Fix tptp proving by working around a hets problem Hets doesn't find a theorem when we pass it as an argument. For TPTP, we know that there can only be a single node and a single theorem, so we don't need to pass the theorems array. The same applies for parsing the output of the prove command.

Use original scope on theorems associations.

Let PAC have one proof_attempt and remove goals When the ProofAttemptCofiguration only has one proof_attempt, there can only be a single goal. This can be retrieved through the proof_attempt.

Use SZS status parser.

Adjust to new hets prover keys 'name' was renamed to 'identifier' and 'display_name' was renamed to 'name'

Fix first_or_create! not knowing the display_name.

Create tactic script during evaluation.

Create ProverOutput in evaluator.

Rename *_with_hash to *_from_hash.

Fix time taken being negative.

Move model filling methods into helper module.