- | Success (None, env) ->
- Printf.printf "Success, but no proof?!?\n\n"
+ | Success (None, env) ->
+ Printf.printf "Success, but no proof?!?\n\n"
+ in
+ Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+ "backward_simpl_time: %.9f\n")
+ !infer_time !forward_simpl_time !backward_simpl_time;
+ Printf.printf "successful unification/matching time: %.9f\n"
+ !Indexing.match_unif_time_ok;
+ Printf.printf "failed unification/matching time: %.9f\n"
+ !Indexing.match_unif_time_no;
+ Printf.printf "indexing retrieval time: %.9f\n"
+ !Indexing.indexing_retrieval_time;
+ Printf.printf "derived %d clauses, kept %d clauses.\n"
+ !derived_clauses !kept_clauses;