@type failure() ::
  {atom(), atom(), term(), term()}
  | Theoria.Kernel.Reference.Replay.Report.failure()

@type t() :: %Theoria.Kernel.Differential.Report{
  artifact_replay: Theoria.Kernel.ArtifactReplay.t(),
  artifact_replay_count: non_neg_integer(),
  artifact_replay_skipped: non_neg_integer(),
  artifact_replay_skips: [Theoria.Kernel.ArtifactReplay.skip()],
  check_count: non_neg_integer(),
  defeq_count: non_neg_integer(),
  failures: [failure()],
  generated_artifact_count: non_neg_integer(),
  generated_artifact_replay_count: non_neg_integer(),
  generated_term_count: non_neg_integer(),
  generated_term_families: %{required(atom()) => non_neg_integer()},
  generated_terms: Theoria.Kernel.GeneratedTerm.Report.t(),
  indexed_artifact_count: non_neg_integer(),
  indexed_artifact_replay_count: non_neg_integer(),
  infer_count: non_neg_integer(),
  normalize_count: non_neg_integer(),
  proof_strategies: Theoria.Kernel.ProofStrategyReport.t(),
  proof_strategy_counts: %{required(atom()) => non_neg_integer()},
  rejection_count: non_neg_integer(),
  replay_count: non_neg_integer(),
  replay_skipped: non_neg_integer(),
  theorem_count: non_neg_integer(),
  theorem_modules: [Theoria.Kernel.TheoremModuleReport.t()],
  theorem_replay_count: non_neg_integer(),
  theorem_replay_skipped: non_neg_integer(),
  timings: Theoria.Kernel.Differential.Timings.t()
}