* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Inference;;
open Utils;;
let symbols_counter = ref 0;;
(* non-recursive Knuth-Bendix term ordering by default *)
-(* Utils.compare_terms := Utils.nonrec_kbo;; *)
-Utils.compare_terms := Utils.ao;;
+Utils.compare_terms := Utils.nonrec_kbo;;
+(* Utils.compare_terms := Utils.ao;; *)
(* statistics... *)
let derived_clauses = ref 0;;