Function vampire_extract_proof 

pub unsafe extern "C" fn vampire_extract_proof(
    refutation: *mut vampire_unit_t,
    out_steps: *mut *mut vampire_proof_step_t,
    out_count: *mut usize,
) -> c_int

Extract the proof as a sequence of steps. Steps are returned in topological order (premises before conclusions). The last step is the empty clause (refutation).

@param refutation The refutation from vampire_get_refutation() @param out_steps Pointer to receive the array of proof steps @param out_count Pointer to receive the number of steps @return 0 on success, -1 on error

Note: The caller must free the returned array and each step’s premise_ids array.