let (proof,ty) = B.saturate t ty in
let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
let bag, c = Utils.add_to_bag bag c in
let (proof,ty) = B.saturate t ty in
let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
let bag, c = Utils.add_to_bag bag c in
passive_singleton (0,goal)
in
let passives, bag, maxvar =
List.fold_left
(fun (cl, bag, maxvar) t ->
let bag, maxvar, c = mk_clause bag maxvar t in
passive_singleton (0,goal)
in
let passives, bag, maxvar =
List.fold_left
(fun (cl, bag, maxvar) t ->
let bag, maxvar, c = mk_clause bag maxvar t in
(passive_empty_set, bag, maxvar) table
in
let actives = [], IDX.DT.empty in
(passive_empty_set, bag, maxvar) table
in
let actives = [], IDX.DT.empty in