+module type Paramod =
+ sig
+ type t
+ type input
+ type szsontology =
+ | Unsatisfiable of (t Terms.bag * int * int list) list
+ | GaveUp
+ | Error of string
+ | Timeout of int * t Terms.bag
+ type bag = t Terms.bag * int
+ val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
+ val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
+ val paramod :
+ useage:bool ->
+ max_steps:int ->
+ ?timeout:float ->
+ bag ->
+ g_passives:t Terms.unit_clause list ->
+ passives:t Terms.unit_clause list -> szsontology
+ end
+
+module Paramod (B : Orderings.Blob) = struct
+ type t = B.t
+ type input = B.input