val mk_passive : bag -> B.input * B.input -> bag * B.t Terms.unit_clause
val mk_goal : bag -> B.input * B.input -> bag * B.t Terms.unit_clause
val paramod :
val mk_passive : bag -> B.input * B.input -> bag * B.t Terms.unit_clause
val mk_goal : bag -> B.input * B.input -> bag * B.t Terms.unit_clause
val paramod :