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