sig
  type id = Ast_tptp.name
  type term = Libzipperposition.STerm.t
  type form = Libzipperposition.STerm.t
  type clause = Trace_tstp.term Libzipperposition.SLiteral.t list
  type t =
      Axiom of string * string
    | Theory of string
    | InferForm of Trace_tstp.form * Trace_tstp.step lazy_t
    | InferClause of Trace_tstp.clause * Trace_tstp.step lazy_t
  and step = {
    id : Trace_tstp.id;
    rule : string;
    parents : Trace_tstp.t array;
    esa : bool;
  }
  val equal : Trace_tstp.t -> Trace_tstp.t -> bool
  val compare : Trace_tstp.t -> Trace_tstp.t -> int
  val mk_f_axiom :
    id:Trace_tstp.id ->
    Trace_tstp.form -> file:string -> name:string -> Trace_tstp.t
  val mk_c_axiom :
    id:Trace_tstp.id ->
    Trace_tstp.clause -> file:string -> name:string -> Trace_tstp.t
  val mk_f_step :
    ?esa:bool ->
    id:Trace_tstp.id ->
    Trace_tstp.form -> rule:string -> Trace_tstp.t list -> Trace_tstp.t
  val mk_c_step :
    ?esa:bool ->
    id:Trace_tstp.id ->
    Trace_tstp.clause -> rule:string -> Trace_tstp.t list -> Trace_tstp.t
  val is_axiom : Trace_tstp.t -> bool
  val is_theory : Trace_tstp.t -> bool
  val is_step : Trace_tstp.t -> bool
  val is_proof_of_false : Trace_tstp.t -> bool
  val get_id : Trace_tstp.t -> Trace_tstp.id
  val force : Trace_tstp.t -> unit
  module StepTbl :
    sig
      type key = t
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
    end
  type proof_set = unit Trace_tstp.StepTbl.t
  val is_dag : Trace_tstp.t -> bool
  val traverse :
    ?traversed:Trace_tstp.proof_set ->
    Trace_tstp.t -> (Trace_tstp.t -> unit) -> unit
  val to_seq : Trace_tstp.t -> Trace_tstp.t Sequence.t
  val depth : Trace_tstp.t -> int
  val size : Trace_tstp.t -> int
  type 'a or_error = [ `Error of string | `Ok of 'a ]
  val of_decls :
    Trace_tstp.form Ast_tptp.t Sequence.t -> Trace_tstp.t Trace_tstp.or_error
  val parse : ?recursive:bool -> string -> Trace_tstp.t Trace_tstp.or_error
  val pp : t CCFormat.printer
  val to_string : t -> string
  val pp1 : Trace_tstp.t CCFormat.printer
  val pp_tstp : Trace_tstp.t CCFormat.printer
end