functor (F : Formula_intf.S) ->
  sig
    type formula = F.t
    type proof = F.proof
    type level
    val dummy : level
    val current_level : unit -> level
    val assume :
      (formula, proof) Theory_intf.slice -> (formula, proof) Theory_intf.res
    val if_sat :
      (formula, proof) Theory_intf.slice -> (formula, proof) Theory_intf.res
    val backtrack : level -> unit
  end