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)
+ Sup.infer_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 "Proofs: ";
+ prerr_endline (Pp.pp_bag bag);
prerr_endline "========================================";
;;