sig
  module type S = LogtkOrdering_intf.S
  module Make :
    functor
      (P : sig
             type symbol = LogtkSymbol.t
             type t
             type precedence = t
             val eq : t -> t -> bool
             val snapshot : t -> symbol list
             val compare : t -> symbol -> symbol -> int
             val mem : t -> symbol -> bool
             val status : t -> symbol -> LogtkPrecedence_intf.symbol_status
             val weight : t -> symbol -> int
             val add_list : t -> symbol list -> t
             val add_seq : t -> symbol Sequence.t -> t
             val declare_status :
               t -> symbol -> LogtkPrecedence_intf.symbol_status -> t
             module Seq : sig val symbols : t -> symbol Sequence.t end
             val pp_snapshot : Buffer.t -> symbol list -> unit
             val pp_debug : Buffer.t -> t -> unit
             val pp : Buffer.t -> t -> unit
             val fmt : Format.formatter -> t -> unit
             val to_string : t -> string
             module Constr :
               sig
                 type t = symbol -> symbol -> LogtkComparison.t
                 val cluster : symbol list list -> t
                 val of_list : symbol list -> t
                 val of_precedence : precedence -> t
                 val arity : (symbol -> int) -> t
                 val invfreq : symbol Sequence.t -> t
                 val max : symbol list -> t
                 val min : symbol list -> t
                 val alpha : t
               end
             type weight_fun = symbol -> int
             val weight_modarity : arity:(symbol -> int) -> weight_fun
             val weight_constant : weight_fun
             val set_weight : t -> weight_fun -> t
             val create :
               ?weight:weight_fun -> Constr.t list -> symbol list -> t
             val create_sort :
               ?weight:weight_fun ->
               (int * Constr.t) list -> symbol list -> t
             val default : symbol list -> t
             val default_seq : symbol Sequence.t -> t
             val constr_list : t -> Constr.t list
             val with_constr_list : t -> Constr.t list -> t
           end->
      sig
        module Prec :
          sig
            type symbol = LogtkSymbol.t
            type t = P.t
            type precedence = t
            val eq : t -> t -> bool
            val snapshot : t -> symbol list
            val compare : t -> symbol -> symbol -> int
            val mem : t -> symbol -> bool
            val status : t -> symbol -> LogtkPrecedence_intf.symbol_status
            val weight : t -> symbol -> int
            val add_list : t -> symbol list -> t
            val add_seq : t -> symbol Sequence.t -> t
            val declare_status :
              t -> symbol -> LogtkPrecedence_intf.symbol_status -> t
            module Seq : sig val symbols : t -> symbol Sequence.t end
            val pp_snapshot : Buffer.t -> symbol list -> unit
            val pp_debug : Buffer.t -> t -> unit
            val pp : Buffer.t -> t -> unit
            val fmt : Format.formatter -> t -> unit
            val to_string : t -> string
            module Constr :
              sig
                type t = symbol -> symbol -> LogtkComparison.t
                val cluster : symbol list list -> t
                val of_list : symbol list -> t
                val of_precedence : precedence -> t
                val arity : (symbol -> int) -> t
                val invfreq : symbol Sequence.t -> t
                val max : symbol list -> t
                val min : symbol list -> t
                val alpha : t
              end
            type weight_fun = symbol -> int
            val weight_modarity : arity:(symbol -> int) -> weight_fun
            val weight_constant : weight_fun
            val set_weight : t -> weight_fun -> t
            val create :
              ?weight:weight_fun -> Constr.t list -> symbol list -> t
            val create_sort :
              ?weight:weight_fun -> (int * Constr.t) list -> symbol list -> t
            val default : symbol list -> t
            val default_seq : symbol Sequence.t -> t
            val constr_list : t -> Constr.t list
            val with_constr_list : t -> Constr.t list -> t
          end
        type term = LogtkFOTerm.t
        type symbol = Prec.symbol
        type t
        type ordering = t
        val compare : t -> term -> term -> LogtkComparison.t
        val precedence : t -> Prec.t
        val set_precedence : t -> Prec.t -> t
        val update_precedence : t -> (Prec.t -> Prec.t) -> t
        val add_list : t -> symbol list -> t
        val add_seq : t -> symbol Sequence.t -> t
        val name : t -> string
        val clear_cache : t -> unit
        val pp : Buffer.t -> t -> unit
        val fmt : Format.formatter -> t -> unit
        val to_string : t -> string
        val kbo : Prec.t -> t
        val rpo6 : Prec.t -> t
        val none : t
        val subterm : t
        val default_of_list : symbol list -> t
        val default_of_prec : Prec.t -> t
        val by_name : string -> Prec.t -> t
        val register : string -> (Prec.t -> t) -> unit
      end
  module Default :
    sig
      module Prec :
        sig
          type symbol = LogtkSymbol.t
          type t = LogtkPrecedence.Default.t
          type precedence = t
          val eq : t -> t -> bool
          val snapshot : t -> symbol list
          val compare : t -> symbol -> symbol -> int
          val mem : t -> symbol -> bool
          val status : t -> symbol -> LogtkPrecedence_intf.symbol_status
          val weight : t -> symbol -> int
          val add_list : t -> symbol list -> t
          val add_seq : t -> symbol Sequence.t -> t
          val declare_status :
            t -> symbol -> LogtkPrecedence_intf.symbol_status -> t
          module Seq : sig val symbols : t -> symbol Sequence.t end
          val pp_snapshot : Buffer.t -> symbol list -> unit
          val pp_debug : Buffer.t -> t -> unit
          val pp : Buffer.t -> t -> unit
          val fmt : Format.formatter -> t -> unit
          val to_string : t -> string
          module Constr :
            sig
              type t = symbol -> symbol -> LogtkComparison.t
              val cluster : symbol list list -> t
              val of_list : symbol list -> t
              val of_precedence : precedence -> t
              val arity : (symbol -> int) -> t
              val invfreq : symbol Sequence.t -> t
              val max : symbol list -> t
              val min : symbol list -> t
              val alpha : t
            end
          type weight_fun = symbol -> int
          val weight_modarity : arity:(symbol -> int) -> weight_fun
          val weight_constant : weight_fun
          val set_weight : t -> weight_fun -> t
          val create :
            ?weight:weight_fun -> Constr.t list -> symbol list -> t
          val create_sort :
            ?weight:weight_fun -> (int * Constr.t) list -> symbol list -> t
          val default : symbol list -> t
          val default_seq : symbol Sequence.t -> t
          val constr_list : t -> Constr.t list
          val with_constr_list : t -> Constr.t list -> t
        end
      type term = LogtkFOTerm.t
      type symbol = Prec.symbol
      type t
      type ordering = t
      val compare : t -> term -> term -> LogtkComparison.t
      val precedence : t -> Prec.t
      val set_precedence : t -> Prec.t -> t
      val update_precedence : t -> (Prec.t -> Prec.t) -> t
      val add_list : t -> symbol list -> t
      val add_seq : t -> symbol Sequence.t -> t
      val name : t -> string
      val clear_cache : t -> unit
      val pp : Buffer.t -> t -> unit
      val fmt : Format.formatter -> t -> unit
      val to_string : t -> string
      val kbo : Prec.t -> t
      val rpo6 : Prec.t -> t
      val none : t
      val subterm : t
      val default_of_list : symbol list -> t
      val default_of_prec : Prec.t -> t
      val by_name : string -> Prec.t -> t
      val register : string -> (Prec.t -> t) -> unit
    end
  module Prec :
    sig
      type symbol = LogtkSymbol.t
      type t = LogtkPrecedence.Default.t
      type precedence = t
      val eq : t -> t -> bool
      val snapshot : t -> symbol list
      val compare : t -> symbol -> symbol -> int
      val mem : t -> symbol -> bool
      val status : t -> symbol -> LogtkPrecedence_intf.symbol_status
      val weight : t -> symbol -> int
      val add_list : t -> symbol list -> t
      val add_seq : t -> symbol Sequence.t -> t
      val declare_status :
        t -> symbol -> LogtkPrecedence_intf.symbol_status -> t
      module Seq : sig val symbols : t -> symbol Sequence.t end
      val pp_snapshot : Buffer.t -> symbol list -> unit
      val pp_debug : Buffer.t -> t -> unit
      val pp : Buffer.t -> t -> unit
      val fmt : Format.formatter -> t -> unit
      val to_string : t -> string
      module Constr :
        sig
          type t = symbol -> symbol -> LogtkComparison.t
          val cluster : symbol list list -> t
          val of_list : symbol list -> t
          val of_precedence : precedence -> t
          val arity : (symbol -> int) -> t
          val invfreq : symbol Sequence.t -> t
          val max : symbol list -> t
          val min : symbol list -> t
          val alpha : t
        end
      type weight_fun = symbol -> int
      val weight_modarity : arity:(symbol -> int) -> weight_fun
      val weight_constant : weight_fun
      val set_weight : t -> weight_fun -> t
      val create : ?weight:weight_fun -> Constr.t list -> symbol list -> t
      val create_sort :
        ?weight:weight_fun -> (int * Constr.t) list -> symbol list -> t
      val default : symbol list -> t
      val default_seq : symbol Sequence.t -> t
      val constr_list : t -> Constr.t list
      val with_constr_list : t -> Constr.t list -> t
    end
  type term = LogtkFOTerm.t
  type symbol = Prec.symbol
  type t
  type ordering = t
  val compare : t -> term -> term -> LogtkComparison.t
  val precedence : t -> Prec.t
  val set_precedence : t -> Prec.t -> t
  val update_precedence : t -> (Prec.t -> Prec.t) -> t
  val add_list : t -> symbol list -> t
  val add_seq : t -> symbol Sequence.t -> t
  val name : t -> string
  val clear_cache : t -> unit
  val pp : Buffer.t -> t -> unit
  val fmt : Format.formatter -> t -> unit
  val to_string : t -> string
  val kbo : Prec.t -> t
  val rpo6 : Prec.t -> t
  val none : t
  val subterm : t
  val default_of_list : symbol list -> t
  val default_of_prec : Prec.t -> t
  val by_name : string -> Prec.t -> t
  val register : string -> (Prec.t -> t) -> unit
end