+*)
+ let mk_clause maxvar t =
+ let ty = B.embed t in
+ let proof = B.embed (NCic.Rel ~-1) in
+ Utils.mk_unit_clause maxvar ty proof
+ in
+ let clause, maxvar = mk_clause 0 t in
+ prerr_endline "Input clause :";
+ prerr_endline (Pp.pp_unit_clause clause);
+ let bag = Utils.empty_bag in
+ let active_clauses, maxvar =
+ List.fold_left
+ (fun (cl,maxvar) t ->
+ let c, m = mk_clause maxvar t in
+ c::cl, m)
+ ([],maxvar) table
+ in
+ let table =
+ List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
+ in
+ prerr_endline "Active table:";
+ List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
+ let bag, maxvar, _, newclauses =
+ Sup.superposition_right bag maxvar clause (active_clauses, table)
+ in
+ prerr_endline "Output clauses :";
+ List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
+ prerr_endline "========================================";