sig
  type t =
      Axiom
    | Resolved of Reasoner.fact Reasoner.Proof.with_proof *
        Reasoner.clause Reasoner.Proof.with_proof
  and 'a with_proof = { conclusion : 'a; proof : Reasoner.Proof.t; }
  val facts : Reasoner.Proof.t -> Reasoner.fact Sequence.t
  val rules : Reasoner.Proof.t -> Reasoner.clause Sequence.t
end